#!/bin/sh # This is a shell archive, meaning: # 1. Remove everything above the #!/bin/sh line. # 2. Save the resulting text in a file. # 3. Execute the file with /bin/sh (not csh) to create the files: # README # design_or.desc # design_or.ver1 # design_or.ver1.clauses # design_or.ver1.out # intchg_val.desc # intchg_val.ver1 # intchg_val.ver1.clauses # intchg_val.ver1.out # interchange.desc # interchange.ver1.clauses # interchange.ver1.in # interchange.ver1.out # two.inverter.desc # two.inverter.val.desc # two.inverter.val.ver1.clauses # two.inverter.val.ver1.in # two.inverter.val.ver1.out # two.inverter.ver1.clauses # two.inverter.ver1.in # two.inverter.ver1.out # two.inverter.ver2.clauses # two.inverter.ver2.in # two.inverter.ver2.out # This archive created: Tue Aug 16 11:14:10 1988 export PATH; PATH=/bin:$PATH if test -f 'README' then echo shar: over-writing existing file "'README'" fi cat << \SHAR_EOF > 'README' problem-set/circuits/README created: 09/02/86 revised: 07/15/88 Contents of 'circuits': ---------------------- Main File Headings ------------------------------------------------------------------------ README : You are currently in this file. design_or : To design an OR-gate from NAND-gates. interchange : To design a circuit which interchanges the given inputs. intchg_val : The ciruit validation of circuit which interchanges the inputs. two_inverter : To design a specific ciruit using only two NOT-gates, and any number of AND-gates and OR-gates. two_inverter_val : The circuit validation of the circuit described by the two_inverter problem. ------------------------------------------------------------------------ For each problem, there are several standard files, which include one probname.desc file and at least one of each of probname.ver#.in, probname.ver#.clauses, and probname.ver#.out. These contain the following: probname.desc : contains the Natural Language Description of the problem, where available, credits for problem formulation, and complete details on each formulation and each version. probname.ver#.in : contains the problem specification, input clauses, and strategy for OTTER; this file is ready to run. probname.ver#.clauses : contains the description, commentary, and the actual clauses (including the denial of the conclusion) used for probname.ver#.in, without any strategy; note that comments always are on lines beginning with a %, preceding the clauses to which they refer, and that clauses terminate with periods. probname.ver#.out : contains the output from running probname.ver#.in with OTTER, with proof if one is found, and with statistics on the clauses generated and CPU time used. HOW TO RUN : ---------------------------------------------------------------------- Invoke OTTER by using the following command : otter < probname.ver#.in [ > outfile ] [ & ] NOTE : '> outfile' may be used to send all output to a file named outfile; '&' may be used to run the program in the background. SHAR_EOF if test -f 'design_or.desc' then echo shar: over-writing existing file "'design_or.desc'" fi cat << \SHAR_EOF > 'design_or.desc' problem-set/circuits/design_or.desc created: 08/28/86 revised: 07/11/88 Natural Language Description: The files beginning with design_or concern the designing of an OR gate using NAND gates. Versions: design_or.ver1 - Nonequality bases axioms are used, hyper resolution is the inference rule, and demodulators are included. created by: E. Lusk verified for ITP: 09/03/86 translated for OTTER: SLM verified for OTTER: 07/11/88 SHAR_EOF if test -f 'design_or.ver1' then echo shar: over-writing existing file "'design_or.ver1'" fi cat << \SHAR_EOF > 'design_or.ver1' % problem-set/circuits/design_or.ver1 % created : 08/28/86 % revised : 07/11/88 % description: % % This run designs an OR gate, using NAND gates. % representation: % % This input file came with no explanation of % the representation. set(hyper_res). list(axioms). -Tab(x1,x2,x3,x4) | -Tab(y1,y2,y3,y4) | Tab(nand(x1,y1),nand(x2,y2),nand(x3,y3),nand(x4,y4)). -Tab(0,1,1,1). end_of_list. list(sos). Tab(0,0,1,1). Tab(0,1,0,1). end_of_list. list(demodulators). Equal(nand(x,y),not(and(x,y))). Equal(and(x,0),0). Equal(and(x,1),x). Equal(not(0),1). Equal(not(1),0). end_of_list. SHAR_EOF if test -f 'design_or.ver1.clauses' then echo shar: over-writing existing file "'design_or.ver1.clauses'" fi cat << \SHAR_EOF > 'design_or.ver1.clauses' % problem-set/circuits/design_or.ver1.clauses % created : 08/28/86 % revised : 07/11/88 % description: % % This run designs an OR gate, using NAND gates. % representation: % % This input file came with no explanation of % the representation. -Tab(x1,x2,x3,x4) | -Tab(y1,y2,y3,y4) | Tab(nand(x1,y1),nand(x2,y2),nand(x3,y3),nand(x4,y4)). -Tab(0,1,1,1). Tab(0,0,1,1). Tab(0,1,0,1). Equal(nand(x,y),not(and(x,y))). Equal(and(x,0),0). Equal(and(x,1),x). Equal(not(0),1). Equal(not(1),0). SHAR_EOF if test -f 'design_or.ver1.out' then echo shar: over-writing existing file "'design_or.ver1.out'" fi cat << \SHAR_EOF > 'design_or.ver1.out' problem-set/circuits/design_or.ver1.out created: 08/28/86 revised: 07/11/88 OTTER release 0.9, 19 May 1988 set(hyper_res). list(axioms). 1 -Tab(x1,x2,x3,x4) | -Tab(y1,y2,y3,y4) | Tab(nand(x1,y1),nand(x2,y2),nand(x3,y3),nand(x4,y4)). 2 -Tab(0,1,1,1). end_of_list. list(sos). 3 Tab(0,0,1,1). 4 Tab(0,1,0,1). end_of_list. list(demodulators). 5 Equal(nand(x,y),not(and(x,y))). 6 Equal(and(x,0),0). 7 Equal(and(x,1),x). 8 Equal(not(0),1). 9 Equal(not(1),0). end_of_list. ----> UNIT CONFLICT at 0.35 sec ----> 17 (15,2) . ------------ END OF SEARCH ------------ ---------------- PROOF ---------------- 1 -Tab(x1,x2,x3,x4) | -Tab(y1,y2,y3,y4) | Tab(nand(x1,y1),nand(x2,y2),nand(x3,y3),nand(x4,y4)). 2 -Tab(0,1,1,1). 3 Tab(0,0,1,1). 4 Tab(0,1,0,1). 5 Equal(nand(x,y),not(and(x,y))). 6 Equal(and(x,0),0). 7 Equal(and(x,1),x). 8 Equal(not(0),1). 9 Equal(not(1),0). 10 (3,1,3,5,6,8,5,6,8,5,7,9,5,7,9) Tab(1,1,0,0). 11 (4,1,4,5,6,8,5,7,9,5,6,8,5,7,9) Tab(1,0,1,0). 15 (11,1,10,5,7,9,5,6,8,5,7,8,5,6,8) Tab(0,1,1,1). 17 (15,2) . --------------- options --------------- set(hyper_res). set(demod_hist). set(for_sub). set(print_kept). set(back_sub). set(print_back_sub). set(print_given). set(check_arity). clear(binary_res). clear(UR_res). clear(para_from). clear(para_into). clear(demod_inf). clear(para_from_left). clear(para_from_right). clear(para_into_vars). clear(para_from_vars). clear(para_all). clear(para_ones_rule). clear(no_para_into_left). clear(no_para_into_right). clear(demod_linear). clear(print_gen). clear(sort_literals). clear(Unit_deletion). clear(factor). clear(print_weight). clear(sos_fifo). clear(bird_print). clear(atom_wt_max_args). clear(print_lists_at_end). clear(free_all_mem). clear(for_sub_fpa). clear(no_fapl). clear(no_fanl). assign(report, 0). assign(max_seconds, 0). assign(max_given, 0). assign(max_kept, 0). assign(max_gen, 0). assign(max_mem, 0). assign(max_weight, 0). assign(max_literals, 0). assign(fpa_literals, 4). assign(fpa_terms, 4). assign(demod_limit, 100). assign(max_proofs, 1). assign(neg_weight, 0). -------------- statistics ------------- clauses input 9 clauses given 4 clauses generated 21 demodulation rewrites 240 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 13 (clauses subsumed by sos) 9 unit deletions 0 clauses kept 8 empty clauses 1 factors generated 0 clauses back subsumed 0 clauses not processed 3 ----------- times (seconds) ----------- run time 0.46 input time 0.10 binary_res time 0.00 hyper_res time 0.05 UR_res time 0.00 para_into time 0.00 para_from time 0.00 pre_process time 0.16 demod time 0.10 weigh time 0.00 for_sub time 0.01 unit_del time 0.00 post_process time 0.02 back_sub time 0.01 conflict time 0.01 factor time 0.00 FPA build time 0.02 IS build time 0.01 print_cl time 0.08 cl integrate time 0.01 window time 0.00 SHAR_EOF if test -f 'intchg_val.desc' then echo shar: over-writing existing file "'intchg_val.desc'" fi cat << \SHAR_EOF > 'intchg_val.desc' problem-set/circuits/intchg_val.desc Natural Language Description: The files beginning with intchg_val concern the validation of a circuit which takes as input x and y and outputs y and x without crossing any wires. Versions: intchg_val.ver1 - The clauses include the 1nput to the circuit and the demodulators required to retrace the flow to validate the circuit. Demodultion is the inference rule. created by: E. Lusk verified for ITP: not yet translated for OTTER: SLM verified for OTTER: not yet SHAR_EOF if test -f 'intchg_val.ver1' then echo shar: over-writing existing file "'intchg_val.ver1'" fi cat << \SHAR_EOF > 'intchg_val.ver1' % problem-set/circuits/intchg_val.ver1 % created : 09/02/86 % revised : 07/11/88 % description: % % This run validates one of the circuit designs that will take % x and y as input and output y and x without crossing any wires. % representation: % % This input file came with no explanation of % the representation. set(demod_inf). assign(max_given, 1). assign(demod_limit, 5000). clear(demod_hist). lex(And(x,x), Or(x,x) ,i2,i1,f3,f2,f1,e2,e1,d3,d2,d1,c2,c1,b3,b2,b1,a2,a1,Not(x)). list(sos). ckt(Input(i1,i2),Output(a1,a2)). end_of_list. list(demodulators). Equal(a1,And(b1,b3)). Equal(a2,And(b2,b3)). Equal(b1,Not(d1)). Equal(b2,Not(d2)). Equal(b3,Or(c1,c2)). Equal(c1,Or(d1,d3)). Equal(c2,Or(d2,d3)). Equal(d3,f3). Equal(d1,Not(e1)). Equal(d2,Not(e2)). Equal(e1,Or(f1,f3)). Equal(e2,Or(f2,f3)). Equal(f1,Not(i1)). Equal(f2,Not(i2)). Equal(f3,And(i1,i2)). % commutativity and associativity Equal(And(x,y),And(y,x)). Equal(Or(x,y),Or(y,x)). Equal(And(x,And(y,z)),And(And(x,y),z)). Equal(Or(x,Or(y,z)),Or(Or(x,y),z)). % sorting Equal(Or(Or(x,y),z),Or(Or(x,z),y)). Equal(And(And(x,y),z),And(And(x,z),y)). % canonicalization to move Not to inside Equal(Not(And(x,y)),Or(Not(x),Not(y))). Equal(Not(Or(x,y)),And(Not(x),Not(y))). % canonicalization to sum-of-products Equal(And(Or(x,y),z),Or(And(x,z),And(y,z))). % simplifiers Equal(And(x,x),x). Equal(And(And(x,y),y),And(x,y)). Equal(And(And(x,y),x),And(x,y)). Equal(Or(x,x),x). Equal(Or(Or(x,y),y),Or(x,y)). Equal(Or(Or(x,y),x),Or(x,y)). Equal(And(x,Not(x)),0). Equal(And(And(x,y),Not(y)),0). Equal(And(And(x,y),Not(x)),0). Equal(Or(x,Not(x)),1). Equal(Or(Or(x,y),Not(y)),1). Equal(Or(Or(x,y),Not(x)),1). Equal(Not(Not(x)),x). Equal(Or(And(x,y),And(x,Not(y))),x). Equal(Or(And(x,y),And(y,Not(x))),y). % evaluators Equal(And(x,0),0). Equal(And(x,1),x). Equal(Or(x,0),x). Equal(Or(x,1),1). Equal(Not(0),1). Equal(Not(1),0). end_of_list. SHAR_EOF if test -f 'intchg_val.ver1.clauses' then echo shar: over-writing existing file "'intchg_val.ver1.clauses'" fi cat << \SHAR_EOF > 'intchg_val.ver1.clauses' % problem-set/circuits/intchg_val.ver1.clauses % created : 09/02/86 % revised : 07/11/88 % description: % % This run validates one of the circuit designs that will take % x and y as input and output y and x without crossing any wires. % representation: % % This input file came with no explanation of % the representation. lex(And(x,x), Or(x,x) ,i2,i1,f3,f2,f1,e2,e1,d3,d2,d1,c2,c1,b3,b2,b1,a2,a1,Not(x)). ckt(Input(i1,i2),Output(a1,a2)). Equal(a1,And(b1,b3)). Equal(a2,And(b2,b3)). Equal(b1,Not(d1)). Equal(b2,Not(d2)). Equal(b3,Or(c1,c2)). Equal(c1,Or(d1,d3)). Equal(c2,Or(d2,d3)). Equal(d3,f3). Equal(d1,Not(e1)). Equal(d2,Not(e2)). Equal(e1,Or(f1,f3)). Equal(e2,Or(f2,f3)). Equal(f1,Not(i1)). Equal(f2,Not(i2)). Equal(f3,And(i1,i2)). % commutativity and associativity Equal(And(x,y),And(y,x)). Equal(Or(x,y),Or(y,x)). Equal(And(x,And(y,z)),And(And(x,y),z)). Equal(Or(x,Or(y,z)),Or(Or(x,y),z)). % sorting Equal(Or(Or(x,y),z),Or(Or(x,z),y)). Equal(And(And(x,y),z),And(And(x,z),y)). % canonicalization to move Not to inside Equal(Not(And(x,y)),Or(Not(x),Not(y))). Equal(Not(Or(x,y)),And(Not(x),Not(y))). % canonicalization to sum-of-products Equal(And(Or(x,y),z),Or(And(x,z),And(y,z))). % simplifiers Equal(And(x,x),x). Equal(And(And(x,y),y),And(x,y)). Equal(And(And(x,y),x),And(x,y)). Equal(Or(x,x),x). Equal(Or(Or(x,y),y),Or(x,y)). Equal(Or(Or(x,y),x),Or(x,y)). Equal(And(x,Not(x)),0). Equal(And(And(x,y),Not(y)),0). Equal(And(And(x,y),Not(x)),0). Equal(Or(x,Not(x)),1). Equal(Or(Or(x,y),Not(y)),1). Equal(Or(Or(x,y),Not(x)),1). Equal(Not(Not(x)),x). Equal(Or(And(x,y),And(x,Not(y))),x). Equal(Or(And(x,y),And(y,Not(x))),y). % evaluators Equal(And(x,0),0). Equal(And(x,1),x). Equal(Or(x,0),x). Equal(Or(x,1),1). Equal(Not(0),1). Equal(Not(1),0). SHAR_EOF if test -f 'intchg_val.ver1.out' then echo shar: over-writing existing file "'intchg_val.ver1.out'" fi cat << \SHAR_EOF > 'intchg_val.ver1.out' problem-set/circuits/intchg_val.ver1.out created: 09/02/86 revised: 07/14/88 OTTER version 0.9, 19 May 1988. set(demod_inf). assign(max_given,1). assign(demod_limit,5000). clear(demod_hist). lex(And(x,x),Or(x,x),i2,i1,f3,f2,f1,e2,e1,d3,d2,d1,c2,c1,b3,b2,b1,a2,a1,Not(x)). list(sos). 1 ckt(Input(i1,i2),Output(a1,a2)). end_of_list. list(demodulators). lex-dependent demodulator: Equal(And(x,y),And(y,x)) lex-dependent demodulator: Equal(Or(x,y),Or(y,x)) lex-dependent demodulator: Equal(Or(Or(x,y),z),Or(Or(x,z),y)) lex-dependent demodulator: Equal(And(And(x,y),z),And(And(x,z),y)) 2 Equal(a1,And(b1,b3)). 3 Equal(a2,And(b2,b3)). 4 Equal(b1,Not(d1)). 5 Equal(b2,Not(d2)). 6 Equal(b3,Or(c1,c2)). 7 Equal(c1,Or(d1,d3)). 8 Equal(c2,Or(d2,d3)). 9 Equal(d3,f3). 10 Equal(d1,Not(e1)). 11 Equal(d2,Not(e2)). 12 Equal(e1,Or(f1,f3)). 13 Equal(e2,Or(f2,f3)). 14 Equal(f1,Not(i1)). 15 Equal(f2,Not(i2)). 16 Equal(f3,And(i1,i2)). 17 Equal(And(x,y),And(y,x)). 18 Equal(Or(x,y),Or(y,x)). 19 Equal(And(x,And(y,z)),And(And(x,y),z)). 20 Equal(Or(x,Or(y,z)),Or(Or(x,y),z)). 21 Equal(Or(Or(x,y),z),Or(Or(x,z),y)). 22 Equal(And(And(x,y),z),And(And(x,z),y)). 23 Equal(Not(And(x,y)),Or(Not(x),Not(y))). 24 Equal(Not(Or(x,y)),And(Not(x),Not(y))). 25 Equal(And(Or(x,y),z),Or(And(x,z),And(y,z))). 26 Equal(And(x,x),x). 27 Equal(And(And(x,y),y),And(x,y)). 28 Equal(And(And(x,y),x),And(x,y)). 29 Equal(Or(x,x),x). 30 Equal(Or(Or(x,y),y),Or(x,y)). 31 Equal(Or(Or(x,y),x),Or(x,y)). 32 Equal(And(x,Not(x)),0). 33 Equal(And(And(x,y),Not(y)),0). 34 Equal(And(And(x,y),Not(x)),0). 35 Equal(Or(x,Not(x)),1). 36 Equal(Or(Or(x,y),Not(y)),1). 37 Equal(Or(Or(x,y),Not(x)),1). 38 Equal(Not(Not(x)),x). 39 Equal(Or(And(x,y),And(x,Not(y))),x). 40 Equal(Or(And(x,y),And(y,Not(x))),y). 41 Equal(And(x,0),0). 42 Equal(And(x,1),x). 43 Equal(Or(x,0),x). 44 Equal(Or(x,1),1). 45 Equal(Not(0),1). 46 Equal(Not(1),0). end_of_list. new given clause: 1 ckt(Input(i1,i2),Output(a1,a2)). ** KEPT: 47 (1) ckt(Input(i1,i2),Output(i2,i1)). ------------ END OF SEARCH ------------ search stopped by max_given option. --------------- options --------------- set(demod_inf). set(for_sub). set(print_kept). set(back_sub). set(print_back_sub). set(print_given). set(check_arity). clear(binary_res). clear(hyper_res). clear(UR_res). clear(para_from). clear(para_into). clear(para_from_left). clear(para_from_right). clear(para_into_vars). clear(para_from_vars). clear(para_all). clear(para_ones_rule). clear(no_para_into_left). clear(no_para_into_right). clear(demod_linear). clear(demod_hist). clear(print_gen). clear(sort_literals). clear(Unit_deletion). clear(factor). clear(print_weight). clear(sos_fifo). clear(bird_print). clear(atom_wt_max_args). clear(print_lists_at_end). clear(free_all_mem). clear(for_sub_fpa). clear(no_fapl). clear(no_fanl). assign(report, 0). assign(max_seconds, 0). assign(max_given, 1). assign(max_kept, 0). assign(max_gen, 0). assign(max_mem, 0). assign(max_weight, 0). assign(max_literals, 0). assign(fpa_literals, 4). assign(fpa_terms, 4). assign(demod_limit, 5000). assign(max_proofs, 1). assign(neg_weight, 0). -------------- statistics ------------- clauses input 46 clauses given 1 clauses generated 1 demodulation rewrites 157 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 0 (clauses subsumed by sos) 0 unit deletions 0 clauses kept 1 empty clauses 0 factors generated 0 clauses back subsumed 0 clauses not processed 0 ----------- times (seconds) ----------- run time 1.61 input time 1.21 binary_res time 0.00 hyper_res time 0.00 UR_res time 0.00 para_into time 0.00 para_from time 0.00 pre_process time 0.27 demod time 0.27 weigh time 0.00 for_sub time 0.00 unit_del time 0.00 post_process time 0.00 back_sub time 0.00 conflict time 0.00 factor time 0.00 FPA build time 0.00 IS build time 0.01 print_cl time 0.18 cl integrate time 0.03 window time 0.00 SHAR_EOF if test -f 'interchange.desc' then echo shar: over-writing existing file "'interchange.desc'" fi cat << \SHAR_EOF > 'interchange.desc' problem-set/circuits/interchange.desc created : 08/28/86 revised : 07/11/88 Natural Language Description: The files beginning with interchange concern the designing of a circuit with inputs x and y and outputs y and x containing no crossing of wires (interchanging of inputs). Versions: interchange.ver1 - Nonequality based axioms are used, hyper resolution is the inference rule, and demodulators are included. created by: E. Lusk verified for ITP: 09/03/86 translated for OTTER by: SLM verified for OTTER: 07/11/88 SHAR_EOF if test -f 'interchange.ver1.clauses' then echo shar: over-writing existing file "'interchange.ver1.clauses'" fi cat << \SHAR_EOF > 'interchange.ver1.clauses' % problem-set/circuits/interchange.ver1.clauses % created : 08/28/86 % revised : 07/11/88 % description: % % Design a circuit with inputs x and y whose outputs are % y and x, and contains no crossings of wires. % representation: % % We represent the circuit built up so far by % ckt(Top(x),Middle(y),Bottom(z)), where Top and Bottom are lists % of outputs, counting outward from the middle. % split the middle, keeping the middle -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(and(y,x1),x2)),Middle(y),Bot(C(and(y,z1),z2))). -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(or(y,x1),x2)),Middle(y),Bot(C(or(y,z1),z2))). % split the middle, omitting the middle -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(and(y,x1),x2)),NIL,Bot(C(and(y,z1),z2))). -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(or(y,x1),x2)),NIL,Bot(C(or(y,z1),z2))). % join across the middle if it is empty, not keeping the sides -ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) | ckt(Top(x2),Middle(and(x1,y1)),Bot(y2)). -ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) | ckt(Top(x2),Middle(or(x1,y1)),Bot(y2)). % join across the middle, keeping the sides -ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) | ckt(Top(C(x1,x2)),Middle(and(x1,y1)),Bot(C(y1,y2))). -ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) | ckt(Top(C(x1,x2)),Middle(or(x1,y1)),Bot(C(y1,y2))). % join to middle, keeping the sides -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(and(y,x1),C(x1,x2))),NIL,Bot(C(and(y,z1),C(z1,z2)))). -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(or(y,x1),C(x1,x2))),NIL,Bot(C(or(y,z1),C(z1,z2)))). % split the wire nearest the middle % this clause is superseded by the previous four % -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | % ckt(Top(C(x1,C(x1,x2))),Middle(y),Bot(C(z1,C(z1,z2)))). % join the two wires nearest the middle -ckt(Top(C(x1,C(x2,x3))),Middle(y),Bot(C(z1,C(z2,z3)))) | ckt(Top(C(and(x1,x2),x3)),Middle(y),Bot(C(and(z1,z2),z3))). -ckt(Top(C(x1,C(x2,x3))),Middle(y),Bot(C(z1,C(z2,z3)))) | ckt(Top(C(or(x1,x2),x3)),Middle(y),Bot(C(or(z1,z2),z3))). % put inverter on the middle wire -ckt(Top(x),Middle(y),Bot(z)) | ckt(Top(x),Middle(not(y)),Bot(z)). % put inverter on the adjacent wires -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(not(x1),x2)),Middle(y),Bot(C(not(z1),z2))). -ckt(Top(C(x1,x2)),NIL,Bot(C(z1,z2))) | ckt(Top(C(not(x1),x2)),NIL,Bot(C(not(z1),z2))). % cannot construct the answer -ckt(Top(C(Tab(0,1,0,1),NIL)),NIL,Bot(C(Tab(0,0,1,1),NIL))). % subsumer to get rid of circuits which are the % same on top and bottom ckt(Top(x),y,Bot(x)). % input configuration ckt(Top(C(Tab(0,0,1,1),NIL)),NIL,Bot(C(Tab(0,1,0,1),NIL))). Equal(and(Tab(x1,x2,x3,x4),Tab(y1,y2,y3,y4)),Tab(and(x1,y1),and(x2,y2),and(x3,y3),and(x4,y4))). Equal(and(0,0),0). Equal(and(0,1),0). Equal(and(1,0),0). Equal(and(1,1),1). Equal(and(NIL,x),x). Equal(or(Tab(x1,x2,x3,x4),Tab(y1,y2,y3,y4)),Tab(or(x1,y1),or(x2,y2),or(x3,y3),or(x4,y4))). Equal(or(0,0),0). Equal(or(0,1),1). Equal(or(1,0),1). Equal(or(1,1),1). Equal(or(NIL,x),x). Equal(not(Tab(x1,x2,x3,x4)),Tab(not(x1),not(x2),not(x3),not(x4))). Equal(not(0),1). Equal(not(1),0). Equal(not(NIL),NIL). Equal(Tab(0,0,0,0),NIL). Equal(Tab(1,1,1,1),NIL). Equal(C(NIL,x),x). Equal(C(x,C(x,y)),C(x,y)). SHAR_EOF if test -f 'interchange.ver1.in' then echo shar: over-writing existing file "'interchange.ver1.in'" fi cat << \SHAR_EOF > 'interchange.ver1.in' % problem-set/circuits/interchange.ver1 % created : 08/28/86 % revised : 07/11/88 % description: % % Design a circuit with inputs x and y whose outputs are % y and x, and contains no crossings of wires. % representation: % % We represent the circuit built up so far by % ckt(Top(x),Middle(y),Bottom(z)), where Top and Bottom are lists % of outputs, counting outward from the middle. set(hyper_res). list(axioms). % split the middle, keeping the middle -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(and(y,x1),x2)),Middle(y),Bot(C(and(y,z1),z2))). -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(or(y,x1),x2)),Middle(y),Bot(C(or(y,z1),z2))). % split the middle, omitting the middle -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(and(y,x1),x2)),NIL,Bot(C(and(y,z1),z2))). -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(or(y,x1),x2)),NIL,Bot(C(or(y,z1),z2))). % join across the middle if it is empty, not keeping the sides -ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) | ckt(Top(x2),Middle(and(x1,y1)),Bot(y2)). -ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) | ckt(Top(x2),Middle(or(x1,y1)),Bot(y2)). % join across the middle, keeping the sides -ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) | ckt(Top(C(x1,x2)),Middle(and(x1,y1)),Bot(C(y1,y2))). -ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) | ckt(Top(C(x1,x2)),Middle(or(x1,y1)),Bot(C(y1,y2))). % join to middle, keeping the sides -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(and(y,x1),C(x1,x2))),NIL,Bot(C(and(y,z1),C(z1,z2)))). -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(or(y,x1),C(x1,x2))),NIL,Bot(C(or(y,z1),C(z1,z2)))). % split the wire nearest the middle % this clause is superseded by the previous four % -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | % ckt(Top(C(x1,C(x1,x2))),Middle(y),Bot(C(z1,C(z1,z2)))). % join the two wires nearest the middle -ckt(Top(C(x1,C(x2,x3))),Middle(y),Bot(C(z1,C(z2,z3)))) | ckt(Top(C(and(x1,x2),x3)),Middle(y),Bot(C(and(z1,z2),z3))). -ckt(Top(C(x1,C(x2,x3))),Middle(y),Bot(C(z1,C(z2,z3)))) | ckt(Top(C(or(x1,x2),x3)),Middle(y),Bot(C(or(z1,z2),z3))). % put inverter on the middle wire -ckt(Top(x),Middle(y),Bot(z)) | ckt(Top(x),Middle(not(y)),Bot(z)). % put inverter on the adjacent wires -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(not(x1),x2)),Middle(y),Bot(C(not(z1),z2))). -ckt(Top(C(x1,x2)),NIL,Bot(C(z1,z2))) | ckt(Top(C(not(x1),x2)),NIL,Bot(C(not(z1),z2))). % cannot construct the answer -ckt(Top(C(Tab(0,1,0,1),NIL)),NIL,Bot(C(Tab(0,0,1,1),NIL))). % subsumer to get rid of circuits which are the % same on top and bottom ckt(Top(x),y,Bot(x)). end_of_list. list(sos). % input configuration ckt(Top(C(Tab(0,0,1,1),NIL)),NIL,Bot(C(Tab(0,1,0,1),NIL))). end_of_list. list(demodulators). Equal(and(Tab(x1,x2,x3,x4),Tab(y1,y2,y3,y4)),Tab(and(x1,y1),and(x2,y2),and(x3,y3),and(x4,y4))). Equal(and(0,0),0). Equal(and(0,1),0). Equal(and(1,0),0). Equal(and(1,1),1). Equal(and(NIL,x),x). Equal(or(Tab(x1,x2,x3,x4),Tab(y1,y2,y3,y4)),Tab(or(x1,y1),or(x2,y2),or(x3,y3),or(x4,y4))). Equal(or(0,0),0). Equal(or(0,1),1). Equal(or(1,0),1). Equal(or(1,1),1). Equal(or(NIL,x),x). Equal(not(Tab(x1,x2,x3,x4)),Tab(not(x1),not(x2),not(x3),not(x4))). Equal(not(0),1). Equal(not(1),0). Equal(not(NIL),NIL). Equal(Tab(0,0,0,0),NIL). Equal(Tab(1,1,1,1),NIL). Equal(C(NIL,x),x). Equal(C(x,C(x,y)),C(x,y)). end_of_list. SHAR_EOF if test -f 'interchange.ver1.out' then echo shar: over-writing existing file "'interchange.ver1.out'" fi cat << \SHAR_EOF > 'interchange.ver1.out' problem-set/circuits/interchange.ver1.out created : 08/28/86 revised : 07/11/88 OTTER release 0.9, 19 May 1988 set(hyper_res). list(axioms). 1 -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(and(y,x1),x2)),Middle(y),Bot(C(and(y,z1),z2))). 2 -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(or(y,x1),x2)),Middle(y),Bot(C(or(y,z1),z2))). 3 -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(and(y,x1),x2)),NIL,Bot(C(and(y,z1),z2))). 4 -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(or(y,x1),x2)),NIL,Bot(C(or(y,z1),z2))). 5 -ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) | ckt(Top(x2),Middle(and(x1,y1)),Bot(y2)). 6 -ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) | ckt(Top(x2),Middle(or(x1,y1)),Bot(y2)). 7 -ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) | ckt(Top(C(x1,x2)),Middle(and(x1,y1)),Bot(C(y1,y2))). 8 -ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) | ckt(Top(C(x1,x2)),Middle(or(x1,y1)),Bot(C(y1,y2))). 9 -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(and(y,x1),C(x1,x2))),NIL,Bot(C(and(y,z1),C(z1,z2)))). 10 -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(or(y,x1),C(x1,x2))),NIL,Bot(C(or(y,z1),C(z1,z2)))). 11 -ckt(Top(C(x1,C(x2,x3))),Middle(y),Bot(C(z1,C(z2,z3)))) | ckt(Top(C(and(x1,x2),x3)),Middle(y),Bot(C(and(z1,z2),z3))). 12 -ckt(Top(C(x1,C(x2,x3))),Middle(y),Bot(C(z1,C(z2,z3)))) | ckt(Top(C(or(x1,x2),x3)),Middle(y),Bot(C(or(z1,z2),z3))). 13 -ckt(Top(x),Middle(y),Bot(z)) | ckt(Top(x),Middle(not(y)),Bot(z)). 14 -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(not(x1),x2)),Middle(y),Bot(C(not(z1),z2))). 15 -ckt(Top(C(x1,x2)),NIL,Bot(C(z1,z2))) | ckt(Top(C(not(x1),x2)),NIL,Bot(C(not(z1),z2))). 16 -ckt(Top(C(Tab(0,1,0,1),NIL)),NIL,Bot(C(Tab(0,0,1,1),NIL))). 17 ckt(Top(x),y,Bot(x)). end_of_list. list(sos). 18 ckt(Top(C(Tab(0,0,1,1),NIL)),NIL,Bot(C(Tab(0,1,0,1),NIL))). end_of_list. list(demodulators). 19 Equal(and(Tab(x1,x2,x3,x4),Tab(y1,y2,y3,y4)),Tab(and(x1,y1),and(x2,y2),and(x3,y3),and(x4,y4))). 20 Equal(and(0,0),0). 21 Equal(and(0,1),0). 22 Equal(and(1,0),0). 23 Equal(and(1,1),1). 24 Equal(and(NIL,x),x). 25 Equal(or(Tab(x1,x2,x3,x4),Tab(y1,y2,y3,y4)),Tab(or(x1,y1),or(x2,y2),or(x3,y3),or(x4,y4))). 26 Equal(or(0,0),0). 27 Equal(or(0,1),1). 28 Equal(or(1,0),1). 29 Equal(or(1,1),1). 30 Equal(or(NIL,x),x). 31 Equal(not(Tab(x1,x2,x3,x4)),Tab(not(x1),not(x2),not(x3),not(x4))). 32 Equal(not(0),1). 33 Equal(not(1),0). 34 Equal(not(NIL),NIL). 35 Equal(Tab(0,0,0,0),NIL). 36 Equal(Tab(1,1,1,1),NIL). 37 Equal(C(NIL,x),x). 38 Equal(C(x,C(x,y)),C(x,y)). end_of_list. ----> UNIT CONFLICT at 10.95 sec ----> 149 (147,16) . ------------ END OF SEARCH ------------ ---------------- PROOF ---------------- 1 -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(and(y,x1),x2)),Middle(y),Bot(C(and(y,z1),z2))). 4 -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(or(y,x1),x2)),NIL,Bot(C(or(y,z1),z2))). 5 -ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) | ckt(Top(x2),Middle(and(x1,y1)),Bot(y2)). 8 -ckt(Top(C(x1,x2)),NIL,Bot(C(y1,y2))) | ckt(Top(C(x1,x2)),Middle(or(x1,y1)),Bot(C(y1,y2))). 9 -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(and(y,x1),C(x1,x2))),NIL,Bot(C(and(y,z1),C(z1,z2)))). 14 -ckt(Top(C(x1,x2)),Middle(y),Bot(C(z1,z2))) | ckt(Top(C(not(x1),x2)),Middle(y),Bot(C(not(z1),z2))). 16 -ckt(Top(C(Tab(0,1,0,1),NIL)),NIL,Bot(C(Tab(0,0,1,1),NIL))). 18 ckt(Top(C(Tab(0,0,1,1),NIL)),NIL,Bot(C(Tab(0,1,0,1),NIL))). 19 Equal(and(Tab(x1,x2,x3,x4),Tab(y1,y2,y3,y4)),Tab(and(x1,y1),and(x2,y2),and(x3,y3),and(x4,y4))). 20 Equal(and(0,0),0). 21 Equal(and(0,1),0). 22 Equal(and(1,0),0). 23 Equal(and(1,1),1). 25 Equal(or(Tab(x1,x2,x3,x4),Tab(y1,y2,y3,y4)),Tab(or(x1,y1),or(x2,y2),or(x3,y3),or(x4,y4))). 26 Equal(or(0,0),0). 27 Equal(or(0,1),1). 28 Equal(or(1,0),1). 29 Equal(or(1,1),1). 31 Equal(not(Tab(x1,x2,x3,x4)),Tab(not(x1),not(x2),not(x3),not(x4))). 32 Equal(not(0),1). 33 Equal(not(1),0). 40 (18,8,25,26,27,28,29) ckt(Top(C(Tab(0,0,1,1),NIL)),Middle(Tab(0,1,1,1)),Bot(C(Tab(0,1,0,1),NIL))). 44 (40,14,31,32,32,33,33,31,32,33,32,33) ckt(Top(C(Tab(1,1,0,0),NIL)),Middle(Tab(0,1,1,1)),Bot(C(Tab(1,0,1,0),NIL))). 54 (44,1,19,21,23,22,22,19,21,22,23,22) ckt(Top(C(Tab(0,1,0,0),NIL)),Middle(Tab(0,1,1,1)),Bot(C(Tab(0,0,1,0),NIL))). 72 (54,14,31,32,33,32,32,31,32,32,33,32) ckt(Top(C(Tab(1,0,1,1),NIL)),Middle(Tab(0,1,1,1)),Bot(C(Tab(1,1,0,1),NIL))). 88 (72,9,19,21,22,23,23,19,21,23,22,23) ckt(Top(C(Tab(0,0,1,1),C(Tab(1,0,1,1),NIL))),NIL,Bot(C(Tab(0,1,0,1),C(Tab(1,1,0,1),NIL)))). 141 (88,5,19,20,21,22,23) ckt(Top(C(Tab(1,0,1,1),NIL)),Middle(Tab(0,0,0,1)),Bot(C(Tab(1,1,0,1),NIL))). 142 (141,14,31,33,32,33,33,31,33,33,32,33) ckt(Top(C(Tab(0,1,0,0),NIL)),Middle(Tab(0,0,0,1)),Bot(C(Tab(0,0,1,0),NIL))). 147 (142,4,25,26,27,26,28,25,26,26,27,28) ckt(Top(C(Tab(0,1,0,1),NIL)),NIL,Bot(C(Tab(0,0,1,1),NIL))). 149 (147,16) . --------------- options --------------- set(hyper_res). set(demod_hist). set(for_sub). set(print_kept). set(back_sub). set(print_back_sub). set(print_given). set(check_arity). clear(binary_res). clear(UR_res). clear(para_from). clear(para_into). clear(demod_inf). clear(para_from_left). clear(para_from_right). clear(para_into_vars). clear(para_from_vars). clear(para_all). clear(para_ones_rule). clear(no_para_into_left). clear(no_para_into_right). clear(demod_linear). clear(print_gen). clear(sort_literals). clear(Unit_deletion). clear(factor). clear(print_weight). clear(sos_fifo). clear(bird_print). clear(atom_wt_max_args). clear(print_lists_at_end). clear(free_all_mem). clear(for_sub_fpa). clear(no_fapl). clear(no_fanl). assign(report, 0). assign(max_seconds, 0). assign(max_given, 0). assign(max_kept, 0). assign(max_gen, 0). assign(max_mem, 0). assign(max_weight, 0). assign(max_literals, 0). assign(fpa_literals, 4). assign(fpa_terms, 4). assign(demod_limit, 100). assign(max_proofs, 1). assign(neg_weight, 0). -------------- statistics ------------- clauses input 38 clauses given 59 clauses generated 404 demodulation rewrites 3300 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 293 (clauses subsumed by sos) 30 unit deletions 0 clauses kept 111 empty clauses 1 factors generated 0 clauses back subsumed 0 clauses not processed 5 ----------- times (seconds) ----------- run time 11.19 input time 0.73 binary_res time 0.00 hyper_res time 1.64 UR_res time 0.00 para_into time 0.00 para_from time 0.00 pre_process time 5.81 demod time 3.11 weigh time 0.08 for_sub time 0.54 unit_del time 0.00 post_process time 2.03 back_sub time 1.11 conflict time 0.90 factor time 0.00 FPA build time 0.54 IS build time 0.19 print_cl time 1.63 cl integrate time 0.35 window time 0.00 SHAR_EOF if test -f 'two.inverter.desc' then echo shar: over-writing existing file "'two.inverter.desc'" fi cat << \SHAR_EOF > 'two.inverter.desc' problem-set/circuits/two.inverter.desc created : 09/02/86 revised : 07/14/88 Natural Language Description: The files beginning with two_inverter concern the two inverter puzzle given in the text, "Automated Reasoning" by Larry Wos et al. (page 186 - 219). It involves using as many AND and OR gates as you like, but using only two NOT gates. The circuit should be designed according to the following specifications: o1 = not(i1) o2 = not(i2) o3 = not(i3) where, o1, o2, o3 are the outputs and i1, i2, i3 are the related inputs. Versions: two_inverter.ver1 - Nonequality based axioms are used, hyper resolution is the inference rule, and demodulators are included. created by: E. Lusk verified for ITP: no proof translated for OTTER by: SLM verified for OTTER: no proof two_inverter.ver2 - Nonequality based axioms are used, hyper resolution is the inference rule, and demodulators are included. created by: E. Lusk verified for ITP: 08/28/86 translated for OTTER by: SLM verified for OTTER: no proof SHAR_EOF if test -f 'two.inverter.val.desc' then echo shar: over-writing existing file "'two.inverter.val.desc'" fi cat << \SHAR_EOF > 'two.inverter.val.desc' problem-set/circuits/two.inverter.val.desc created : 09/03/86 revised : 07/15/88 Natural Language Description: The files beginning with two_inverter_val concern the validation of a solution to the two_inverter_val given in the text, "Automated Reasoning" by Larry Wos et al. (chapter 7). The puzzle involves using as many AND and OR gates as you like, but using only two NOT gates. The circuit should be designed according to the following specifications: o1 = not(i1) o2 = not(i2) o3 = not(i3) where, o1, o2, o3 are the outputs and i1, i2, i3 are the related inputs. Versions: two_inverter_val.ver1 - Nonequality based axioms are used, forward demodulation is the inference rule, and demodulators are included. created by: E. Lusk verified for ITP: no proof translated for OTTER by: SLM verified for OTTER: 07/15/88 SHAR_EOF if test -f 'two.inverter.val.ver1.clauses' then echo shar: over-writing existing file "'two.inverter.val.ver1.clauses'" fi cat << \SHAR_EOF > 'two.inverter.val.ver1.clauses' % problem-set/circuits/two.inverter.val.ver1.clauses % created : 08/28/86 % revised : 07/14/88 % description: % % This is made to validate the circuit described in the text, "Automated % Reasoning" by Larry Wos et al. (chapter 7): % % A circuit using as many AND and OR gates as you like, but % using only two NOT gates. The circuit should be designed according to % the following specification: % % o1 = not(i1) % o2 = not(i2) % o3 = not(i3) % % where, o1, o2, o3 are the outputs and i1, i2, i3 are the % related inputs. % representation: % % See the above mentioned text. lex(0,1,21,20,19,18,17,16,15,14,13,12,10,9,8,7,6,5,4,3,2,a1,inv2,inv1,i3,i2,i1,not(x),and(x,x),or(x,x)). % original state CKT(o1). CKT(o2). CKT(o3). % demodulators defining the structure Equal(o1,13). Equal(o2,17). Equal(o3,5). Equal(a1,and(inv1,i2)). Equal(2,and(inv1,i3)). Equal(3,or(a1,24)). Equal(4,or(15,3)). Equal(5,or(4,21)). Equal(6,and(i1,i2)). Equal(7,and(6,i3)). Equal(8,or(a1,10)). Equal(9,or(8,2)). Equal(10,or(24,7)). Equal(11,or(a1,2)). Equal(12,or(11,16)). Equal(13,or(12,21)). Equal(14,and(i2,i3)). Equal(15,and(inv2,6)). Equal(16,and(14,inv2)). Equal(17,or(18,21)). Equal(18,or(19,25)). Equal(19,and(23,inv2)). Equal(20,or(22,14)). Equal(21,and(inv1,inv2)). Equal(22,or(23,6)). Equal(23,and(i1,i3)). Equal(24,and(i1,inv1)). Equal(25,or(2,24)). Equal(inv1,not(20)). Equal(inv2,not(9)). % Canonicalizing an exclusive-or/and expression with lex-dependent demodulation Equal(eor(0,x), x). Equal(eor(x,0), x). Equal(eor(x,x), 0). Equal(eor(x,eor(x,y)), y). Equal(eor(x,y), eor(y,x)). Equal(eor(y,eor(x,z)), eor(x,eor(y,z))). Equal(and(0,x), 0). Equal(and(x,0), 0). Equal(and(1,x), x). Equal(and(x,1), x). Equal(and(x,x), x). Equal(and(x,and(x,y)), and(x,y)). Equal(and(x,y), and(y,x)). Equal(and(y,and(x,z)), and(x,and(y,z))). Equal(and(x,eor(y,z)),eor(and(x,y),and(x,z))). Equal(not(x), eor(1,x)). Equal(or(x,y), eor(and(x,y),eor(x,y))). SHAR_EOF if test -f 'two.inverter.val.ver1.in' then echo shar: over-writing existing file "'two.inverter.val.ver1.in'" fi cat << \SHAR_EOF > 'two.inverter.val.ver1.in' % problem-set/circuits/two.inverter.val.ver1 % created : 08/28/86 % revised : 07/14/88 % description: % % This is made to validate the circuit described in the text, "Automated % Reasoning" by Larry Wos et al. (chapter 7): % % A circuit using as many AND and OR gates as you like, but % using only two NOT gates. The circuit should be designed according to % the following specification: % % o1 = not(i1) % o2 = not(i2) % o3 = not(i3) % % where, o1, o2, o3 are the outputs and i1, i2, i3 are the % related inputs. % representation: % % See the above mentioned text. lex(0,1,21,20,19,18,17,16,15,14,13,12,10,9,8,7,6,5,4,3,2,a1,inv2,inv1,i3,i2,i1,not(x),and(x,x),or(x,x)). set(demod_inf). set(sos_fifo). assign(max_given,3). assign(demod_limit,3000). clear(demod_hist). list(sos). CKT(o1). CKT(o2). CKT(o3). end_of_list. list(demodulators). Equal(o1,13). Equal(o2,17). Equal(o3,5). Equal(a1,and(inv1,i2)). Equal(2,and(inv1,i3)). Equal(3,or(a1,24)). Equal(4,or(15,3)). Equal(5,or(4,21)). Equal(6,and(i1,i2)). Equal(7,and(6,i3)). Equal(8,or(a1,10)). Equal(9,or(8,2)). Equal(10,or(24,7)). Equal(11,or(a1,2)). Equal(12,or(11,16)). Equal(13,or(12,21)). Equal(14,and(i2,i3)). Equal(15,and(inv2,6)). Equal(16,and(14,inv2)). Equal(17,or(18,21)). Equal(18,or(19,25)). Equal(19,and(23,inv2)). Equal(20,or(22,14)). Equal(21,and(inv1,inv2)). Equal(22,or(23,6)). Equal(23,and(i1,i3)). Equal(24,and(i1,inv1)). Equal(25,or(2,24)). Equal(inv1,not(20)). Equal(inv2,not(9)). % Canonicalizing an exclusive-or/and expression with lex-dependent demodulation Equal(eor(0,x), x). Equal(eor(x,0), x). Equal(eor(x,x), 0). Equal(eor(x,eor(x,y)), y). Equal(eor(x,y), eor(y,x)). Equal(eor(y,eor(x,z)), eor(x,eor(y,z))). Equal(and(0,x), 0). Equal(and(x,0), 0). Equal(and(1,x), x). Equal(and(x,1), x). Equal(and(x,x), x). Equal(and(x,and(x,y)), and(x,y)). Equal(and(x,y), and(y,x)). Equal(and(y,and(x,z)), and(x,and(y,z))). Equal(and(x,eor(y,z)),eor(and(x,y),and(x,z))). Equal(not(x), eor(1,x)). Equal(or(x,y), eor(and(x,y),eor(x,y))). end_of_list. SHAR_EOF if test -f 'two.inverter.val.ver1.out' then echo shar: over-writing existing file "'two.inverter.val.ver1.out'" fi cat << \SHAR_EOF > 'two.inverter.val.ver1.out' problem-set/circuits/two.inverter.val.ver1.out created : 09/03/86 revised : 07/15/88 OTTER version 0.9, 19 May 1988. lex(0,1,21,20,19,18,17,16,15,14,13,12,10,9,8,7,6,5,4,3,2,a1,inv2,inv1,i3,i2,i1,not(x),and(x,x),or(x,x)). set(demod_inf). set(sos_fifo). assign(max_given,3). assign(demod_limit,3000). clear(demod_hist). list(sos). 1 CKT(o1). 2 CKT(o2). 3 CKT(o3). end_of_list. list(demodulators). lex-dependent demodulator: Equal(eor(x,y),eor(y,x)) lex-dependent demodulator: Equal(eor(y,eor(x,z)),eor(x,eor(y,z))) lex-dependent demodulator: Equal(and(x,y),and(y,x)) lex-dependent demodulator: Equal(and(y,and(x,z)),and(x,and(y,z))) 4 Equal(o1,13). 5 Equal(o2,17). 6 Equal(o3,5). 7 Equal(a1,and(inv1,i2)). 8 Equal(2,and(inv1,i3)). 9 Equal(3,or(a1,24)). 10 Equal(4,or(15,3)). 11 Equal(5,or(4,21)). 12 Equal(6,and(i1,i2)). 13 Equal(7,and(6,i3)). 14 Equal(8,or(a1,10)). 15 Equal(9,or(8,2)). 16 Equal(10,or(24,7)). 17 Equal(11,or(a1,2)). 18 Equal(12,or(11,16)). 19 Equal(13,or(12,21)). 20 Equal(14,and(i2,i3)). 21 Equal(15,and(inv2,6)). 22 Equal(16,and(14,inv2)). 23 Equal(17,or(18,21)). 24 Equal(18,or(19,25)). 25 Equal(19,and(23,inv2)). 26 Equal(20,or(22,14)). 27 Equal(21,and(inv1,inv2)). 28 Equal(22,or(23,6)). 29 Equal(23,and(i1,i3)). 30 Equal(24,and(i1,inv1)). 31 Equal(25,or(2,24)). 32 Equal(inv1,not(20)). 33 Equal(inv2,not(9)). 34 Equal(eor(0,x),x). 35 Equal(eor(x,0),x). 36 Equal(eor(x,x),0). 37 Equal(eor(x,eor(x,y)),y). 38 Equal(eor(x,y),eor(y,x)). 39 Equal(eor(y,eor(x,z)),eor(x,eor(y,z))). 40 Equal(and(0,x),0). 41 Equal(and(x,0),0). 42 Equal(and(1,x),x). 43 Equal(and(x,1),x). 44 Equal(and(x,x),x). 45 Equal(and(x,and(x,y)),and(x,y)). 46 Equal(and(x,y),and(y,x)). 47 Equal(and(y,and(x,z)),and(x,and(y,z))). 48 Equal(and(x,eor(y,z)),eor(and(x,y),and(x,z))). 49 Equal(not(x),eor(1,x)). 50 Equal(or(x,y),eor(and(x,y),eor(x,y))). end_of_list. new given clause: 1 CKT(o1). ** KEPT: 51 (1) CKT(eor(1,i1)). new given clause: 2 CKT(o2). ** KEPT: 52 (2) CKT(eor(1,i2)). new given clause: 3 CKT(o3). ** KEPT: 53 (3) CKT(eor(1,i3)). ------------ END OF SEARCH ------------ search stopped by max_given option. --------------- options --------------- set(demod_inf). set(for_sub). set(print_kept). set(back_sub). set(print_back_sub). set(print_given). set(check_arity). set(sos_fifo). clear(binary_res). clear(hyper_res). clear(UR_res). clear(para_from). clear(para_into). clear(para_from_left). clear(para_from_right). clear(para_into_vars). clear(para_from_vars). clear(para_all). clear(para_ones_rule). clear(no_para_into_left). clear(no_para_into_right). clear(demod_linear). clear(demod_hist). clear(print_gen). clear(sort_literals). clear(Unit_deletion). clear(factor). clear(print_weight). clear(bird_print). clear(atom_wt_max_args). clear(print_lists_at_end). clear(free_all_mem). clear(for_sub_fpa). clear(no_fapl). clear(no_fanl). assign(report, 0). assign(max_seconds, 0). assign(max_given, 3). assign(max_kept, 0). assign(max_gen, 0). assign(max_mem, 0). assign(max_weight, 0). assign(max_literals, 0). assign(fpa_literals, 4). assign(fpa_terms, 4). assign(demod_limit, 3000). assign(max_proofs, 1). assign(neg_weight, 0). -------------- statistics ------------- clauses input 50 clauses given 3 clauses generated 3 demodulation rewrites 4994 clauses wt or lit delete 0 tautologies deleted 0 clauses forward subsumed 0 (clauses subsumed by sos) 0 unit deletions 0 clauses kept 3 empty clauses 0 factors generated 0 clauses back subsumed 0 clauses not processed 0 ----------- times (seconds) ----------- run time 15.93 input time 1.08 binary_res time 0.00 hyper_res time 0.00 UR_res time 0.00 para_into time 0.00 para_from time 0.00 pre_process time 14.68 demod time 14.63 weigh time 0.02 for_sub time 0.00 unit_del time 0.00 post_process time 0.02 back_sub time 0.01 conflict time 0.00 factor time 0.00 FPA build time 0.00 IS build time 0.00 print_cl time 0.18 cl integrate time 0.03 window time 0.00 SHAR_EOF if test -f 'two.inverter.ver1.clauses' then echo shar: over-writing existing file "'two.inverter.ver1.clauses'" fi cat << \SHAR_EOF > 'two.inverter.ver1.clauses' % problem-set/circuits/two.inverter.ver1.clauses % created : 08/28/86 % revised : 07/14/88 % description: % % The two inverter puzzle given in the text, "Automated % Reasoning" by Larry Wos et al.(page 186 - 219). % % To design a circuit using as many AND and OR gates as you like, but % using only two NOT gates. The circuit should be designed according to % the following specification: % % o1 = not(i1) % o2 = not(i2) % o3 = not(i3) % % where, o1, o2, o3 are the outputs and i1, i2, i3 are the % related inputs. % representation: % % See pages 186 - 219 in the above mentioned text. -OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) | -OUTPUT(y1,y2,y3,y4,y5,y6,y7,y8,v) | OUTPUT(and(x1,y1),and(x2,y2),and(x3,y3),and(x4,y4), and(x5,y5),and(x6,y6),and(x7,y7),and(x8,y8),v). -OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) | -OUTPUT(y1,y2,y3,y4,y5,y6,y7,y8,v) | OUTPUT(or(x1,y1),or(x2,y2),or(x3,y3),or(x4,y4), or(x5,y5),or(x6,y6),or(x7,y7),or(x8,y8),v). -OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) | TEST(not(x1),not(x2),not(x3),not(x4),not(x5),not(x6), not(x7),not(x8),addinv(v,invtab(not(x1),not(x2),not(x3), not(x4),not(x5),not(x6),not(x7),not(x8))), makerevlist(l(invtab(not(x1),not(x2),not(x3),not(x4), not(x5),not(x6),not(x7),not(x8)),v))). -TEST(x1,x2,x3,x4,x5,x6,x7,x8,v,xrevlist) | OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v). -OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) | OUTPUT(not(x1),not(x2),not(x3),not(x4),not(x5),not(x6),not(x7),not(x8), addinv(v,invtab(not(x1),not(x2),not(x3),not(x4),not(x5),not(x6),not(x7), not(x8)))). OUTPUT(0,0,0,0,1,1,1,1,x). OUTPUT(0,0,1,1,0,0,1,1,x). OUTPUT(0,1,0,1,0,1,0,1,x). -OUTPUT(1,1,1,1,0,0,0,0,v) | -OUTPUT(1,1,0,0,1,1,0,0,v) | -OUTPUT(1,0,1,0,1,0,1,0,v). Equal(and(x,0),0). Equal(and(x,1),x). Equal(or(x,0),x). Equal(or(x,1),1). Equal(not(0),1). Equal(not(1),0). % list handling Equal(addinv(l(x,y),z),l(x,addinv(y,z))). Equal(addinv(x,y),l(y,x)). Equal(makerevlist(l(invtab(x000,x001,x010,x011,x100,x101,x110,x111),v)), lr(possrev(R00m,x000,x001), lr(possrev(R01m,x010,x011), lr(possrev(R10m,x100,x101), lr(possrev(R11m,x110,x111), lr(possrev(R0m0,x000,x010), lr(possrev(R0m1,x001,x011), lr(possrev(R1m0,x100,x110), lr(possrev(R1m1,x101,x111), lr(possrev(Rm00,x000,x100), lr(possrev(Rm01,x001,x101), lr(possrev(Rm10,x010,x110), lr(possrev(Rm11,x011,x111), makerevlist(v)))))))))))))). Equal(makerevlist(v),end). Equal(possrev(xname,1,0),xname). Equal(possrev(xname,0,1),notrev). Equal(possrev(xname,x,x),notrev). Equal(lr(notrev,x),x). Equal(lr(x,lr(y,z)),lr(y,lr(x,z))). Equal(lr(x,lr(x,y)),lr(x,y)). SHAR_EOF if test -f 'two.inverter.ver1.in' then echo shar: over-writing existing file "'two.inverter.ver1.in'" fi cat << \SHAR_EOF > 'two.inverter.ver1.in' % problem-set/circuits/two.inverter.ver1 % created : 08/28/86 % revised : 07/14/88 % description: % % The two inverter puzzle given in the text, "Automated % Reasoning" by Larry Wos et al.(page 186 - 219). % % To design a circuit using as many AND and OR gates as you like, but % using only two NOT gates. The circuit should be designed according to % the following specification: % % o1 = not(i1) % o2 = not(i2) % o3 = not(i3) % % where, o1, o2, o3 are the outputs and i1, i2, i3 are the % related inputs. % representation: % % See pages 186 - 219 in the above mentioned text. set(hyper_res). list(axioms). -OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) | -OUTPUT(y1,y2,y3,y4,y5,y6,y7,y8,v) | OUTPUT(and(x1,y1),and(x2,y2),and(x3,y3),and(x4,y4), and(x5,y5),and(x6,y6),and(x7,y7),and(x8,y8),v). -OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) | -OUTPUT(y1,y2,y3,y4,y5,y6,y7,y8,v) | OUTPUT(or(x1,y1),or(x2,y2),or(x3,y3),or(x4,y4), or(x5,y5),or(x6,y6),or(x7,y7),or(x8,y8),v). -OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) | TEST(not(x1),not(x2),not(x3),not(x4),not(x5),not(x6), not(x7),not(x8),addinv(v,invtab(not(x1),not(x2),not(x3), not(x4),not(x5),not(x6),not(x7),not(x8))), makerevlist(l(invtab(not(x1),not(x2),not(x3),not(x4), not(x5),not(x6),not(x7),not(x8)),v))). -TEST(x1,x2,x3,x4,x5,x6,x7,x8,v,xrevlist) | OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v). % -OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) | % OUTPUT(not(x1),not(x2),not(x3),not(x4),not(x5),not(x6),not(x7),not(x8), % addinv(v,invtab(not(x1),not(x2),not(x3),not(x4),not(x5),not(x6),not(x7), % not(x8)))). end_of_list. list(sos). OUTPUT(0,0,0,0,1,1,1,1,x). OUTPUT(0,0,1,1,0,0,1,1,x). OUTPUT(0,1,0,1,0,1,0,1,x). -OUTPUT(1,1,1,1,0,0,0,0,v) | -OUTPUT(1,1,0,0,1,1,0,0,v) | -OUTPUT(1,0,1,0,1,0,1,0,v). end_of_list. list(demodulators). Equal(and(x,0),0). Equal(and(x,1),x). Equal(or(x,0),x). Equal(or(x,1),1). Equal(not(0),1). Equal(not(1),0). % list handling Equal(addinv(l(x,y),z),l(x,addinv(y,z))). Equal(addinv(x,y),l(y,x)). Equal(makerevlist(l(invtab(x000,x001,x010,x011,x100,x101,x110,x111),v)), lr(possrev(R00m,x000,x001), lr(possrev(R01m,x010,x011), lr(possrev(R10m,x100,x101), lr(possrev(R11m,x110,x111), lr(possrev(R0m0,x000,x010), lr(possrev(R0m1,x001,x011), lr(possrev(R1m0,x100,x110), lr(possrev(R1m1,x101,x111), lr(possrev(Rm00,x000,x100), lr(possrev(Rm01,x001,x101), lr(possrev(Rm10,x010,x110), lr(possrev(Rm11,x011,x111), makerevlist(v)))))))))))))). Equal(makerevlist(v),end). Equal(possrev(xname,1,0),xname). Equal(possrev(xname,0,1),notrev). Equal(possrev(xname,x,x),notrev). Equal(lr(notrev,x),x). Equal(lr(x,lr(y,z)),lr(y,lr(x,z))). Equal(lr(x,lr(x,y)),lr(x,y)). end_of_list. SHAR_EOF if test -f 'two.inverter.ver1.out' then echo shar: over-writing existing file "'two.inverter.ver1.out'" fi cat << \SHAR_EOF > 'two.inverter.ver1.out' problem-set/circuits/two.inverter.ver1.out created : 08/28/86 revised : 07/14/88 This version has no output file, because no proof was found. SHAR_EOF if test -f 'two.inverter.ver2.clauses' then echo shar: over-writing existing file "'two.inverter.ver2.clauses'" fi cat << \SHAR_EOF > 'two.inverter.ver2.clauses' % problem-set/circuits/two.inverter.ver2.clauses % created : 08/28/86 % revised : 07/14/88 % description: % % The two inverter puzzle given in the text, "Automated % Reasoning" by Larry Wos et al.(page 186 - 219). % % To design a circuit using as many AND and OR gates as you like, but % using only two NOT gates. The circuit should be designed according to % the following specification: % % o1 = not(i1) % o2 = not(i2) % o3 = not(i3) % % where, o1, o2, o3 are the outputs and i1, i2, i3 are the % related inputs. % representation: % % See pages 186 - 219 in the above mentioned text. -BOUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) | -BOUTPUT(y1,y2,y3,y4,y5,y6,y7,y8,v) | BOUTPUT(and(x1,y1),and(x2,y2),and(x3,y3),and(x4,y4), and(x5,y5),and(x6,y6),and(x7,y7),and(x8,y8),v). -BOUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) | -OUTPUT(y1,y2,y3,y4,y5,y6,y7,y8,v) | OUTPUT(or(x1,y1),or(x2,y2),or(x3,y3),or(x4,y4), or(x5,y5),or(x6,y6),or(x7,y7),or(x8,y8),v). -OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) | TEST(not(x1),not(x2),not(x3),not(x4),not(x5),not(x6), not(x7),not(x8),addinv(v,invtab(not(x1),not(x2),not(x3), not(x4),not(x5),not(x6),not(x7),not(x8))), makerevlist(l(invtab(not(x1),not(x2),not(x3),not(x4), not(x5),not(x6),not(x7),not(x8)),v))). -BOUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) | OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v). -TEST(x1,x2,x3,x4,x5,x6,x7,x8,v,xrevlist) | BOUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v). BOUTPUT(0,0,0,0,1,1,1,1,x). BOUTPUT(0,0,1,1,0,0,1,1,x). BOUTPUT(0,1,0,1,0,1,0,1,x). -OUTPUT(1,1,1,1,0,0,0,0,v) | -OUTPUT(1,1,0,0,1,1,0,0,v) | -OUTPUT(1,0,1,0,1,0,1,0,v). Equal(and(x,0),0). Equal(and(x,1),x). Equal(or(x,0),x). Equal(or(x,1),1). Equal(not(0),1). Equal(not(1),0). % List handling. Equal(addinv(l(x,y),z),l(x,addinv(y,z))). Equal(addinv(x,y),l(y,x)). Equal(makerevlist(l(invtab(x000,x001,x010,x011,x100,x101,x110,x111),v)), lr(possrev(R00m,x000,x001), lr(possrev(R01m,x010,x011), lr(possrev(R10m,x100,x101), lr(possrev(R11m,x110,x111), lr(possrev(R0m0,x000,x010), lr(possrev(R0m1,x001,x011), lr(possrev(R1m0,x100,x110), lr(possrev(R1m1,x101,x111), lr(possrev(Rm00,x000,x100), lr(possrev(Rm01,x001,x101), lr(possrev(Rm10,x010,x110), lr(possrev(Rm11,x011,x111), makerevlist(v)))))))))))))). Equal(makerevlist(v),end). Equal(possrev(xname,1,0),xname). Equal(possrev(xname,0,1),notrev). Equal(possrev(xname,x,x),notrev). Equal(lr(notrev,x),x). Equal(lr(x,lr(y,z)),lr(y,lr(x,z))). Equal(lr(x,lr(x,y)),lr(x,y)). SHAR_EOF if test -f 'two.inverter.ver2.in' then echo shar: over-writing existing file "'two.inverter.ver2.in'" fi cat << \SHAR_EOF > 'two.inverter.ver2.in' % problem-set/circuits/two.inverter.ver2 % created : 08/28/86 % revised : 07/14/88 % description: % % The two inverter puzzle given in the text, "Automated % Reasoning" by Larry Wos et al.(page 186 - 219). % % To design a circuit using as many AND and OR gates as you like, but % using only two NOT gates. The circuit should be designed according to % the following specification: % % o1 = not(i1) % o2 = not(i2) % o3 = not(i3) % % where, o1, o2, o3 are the outputs and i1, i2, i3 are the % related inputs. % representation: % % See pages 186 - 219 in the above mentioned text. set(hyper_res). list(axioms). -BOUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) | -BOUTPUT(y1,y2,y3,y4,y5,y6,y7,y8,v) | BOUTPUT(and(x1,y1),and(x2,y2),and(x3,y3),and(x4,y4), and(x5,y5),and(x6,y6),and(x7,y7),and(x8,y8),v). -BOUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) | -OUTPUT(y1,y2,y3,y4,y5,y6,y7,y8,v) | OUTPUT(or(x1,y1),or(x2,y2),or(x3,y3),or(x4,y4), or(x5,y5),or(x6,y6),or(x7,y7),or(x8,y8),v). -OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) | TEST(not(x1),not(x2),not(x3),not(x4),not(x5),not(x6), not(x7),not(x8),addinv(v,invtab(not(x1),not(x2),not(x3), not(x4),not(x5),not(x6),not(x7),not(x8))), makerevlist(l(invtab(not(x1),not(x2),not(x3),not(x4), not(x5),not(x6),not(x7),not(x8)),v))). -BOUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v) | OUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v). -TEST(x1,x2,x3,x4,x5,x6,x7,x8,v,xrevlist) | BOUTPUT(x1,x2,x3,x4,x5,x6,x7,x8,v). end_of_list. list(sos). BOUTPUT(0,0,0,0,1,1,1,1,x). BOUTPUT(0,0,1,1,0,0,1,1,x). BOUTPUT(0,1,0,1,0,1,0,1,x). -OUTPUT(1,1,1,1,0,0,0,0,v) | -OUTPUT(1,1,0,0,1,1,0,0,v) | -OUTPUT(1,0,1,0,1,0,1,0,v). end_of_list. list(demodulators). Equal(and(x,0),0). Equal(and(x,1),x). Equal(or(x,0),x). Equal(or(x,1),1). Equal(not(0),1). Equal(not(1),0). % List handling. Equal(addinv(l(x,y),z),l(x,addinv(y,z))). Equal(addinv(x,y),l(y,x)). Equal(makerevlist(l(invtab(x000,x001,x010,x011,x100,x101,x110,x111),v)), lr(possrev(R00m,x000,x001), lr(possrev(R01m,x010,x011), lr(possrev(R10m,x100,x101), lr(possrev(R11m,x110,x111), lr(possrev(R0m0,x000,x010), lr(possrev(R0m1,x001,x011), lr(possrev(R1m0,x100,x110), lr(possrev(R1m1,x101,x111), lr(possrev(Rm00,x000,x100), lr(possrev(Rm01,x001,x101), lr(possrev(Rm10,x010,x110), lr(possrev(Rm11,x011,x111), makerevlist(v)))))))))))))). Equal(makerevlist(v),end). Equal(possrev(xname,1,0),xname). Equal(possrev(xname,0,1),notrev). Equal(possrev(xname,x,x),notrev). Equal(lr(notrev,x),x). Equal(lr(x,lr(y,z)),lr(y,lr(x,z))). Equal(lr(x,lr(x,y)),lr(x,y)). end_of_list. SHAR_EOF if test -f 'two.inverter.ver2.out' then echo shar: over-writing existing file "'two.inverter.ver2.out'" fi cat << \SHAR_EOF > 'two.inverter.ver2.out' problem-set/circuits/two.inverter.ver2.out created : 08/28/86 revised : 07/14/88 This version has no output file, because no proof was found. SHAR_EOF # End of shell archive exit 0