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