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
