%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : HWV036-1 : TPTP v8.1.2. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n029.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:25:02 EDT 2024
% Result : Satisfiable 0.47s 0.68s
% Output : Saturation 0.47s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(or_1_11,axiom,
( ~ mode(X55,ok)
| ~ type(X55,or)
| ~ value(out(n1,X55),n1)
| value(in(n1,X55),n1)
| value(in(n2,X55),n1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',or_1_11) ).
cnf(not_1_0_bw,axiom,
( ~ mode(X54,ok)
| ~ type(X54,not)
| ~ value(out(n1,X54),n1)
| value(in(n1,X54),n0) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',not_1_0_bw) ).
cnf(not_0_1_bw,axiom,
( ~ mode(X53,ok)
| ~ type(X53,not)
| ~ value(out(n1,X53),n0)
| value(in(n1,X53),n1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',not_0_1_bw) ).
cnf(not_1_0_fw,axiom,
( ~ mode(X52,ok)
| ~ type(X52,not)
| ~ value(in(n1,X52),n1)
| value(out(n1,X52),n0) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',not_1_0_fw) ).
cnf(or_00_0,axiom,
( ~ mode(X51,ok)
| ~ type(X51,or)
| ~ value(in(n1,X51),n0)
| ~ value(in(n2,X51),n0)
| value(out(n1,X51),n0) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',or_00_0) ).
cnf(not_0_1_fw,axiom,
( ~ mode(X50,ok)
| ~ type(X50,not)
| ~ value(in(n1,X50),n0)
| value(out(n1,X50),n1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',not_0_1_fw) ).
cnf(or_0_01,axiom,
( ~ mode(X49,ok)
| ~ type(X49,or)
| ~ value(out(n1,X49),n0)
| value(in(n2,X49),n0) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',or_0_01) ).
cnf(or_0_0x,axiom,
( ~ mode(X48,ok)
| ~ type(X48,or)
| ~ value(out(n1,X48),n0)
| value(in(n1,X48),n0) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',or_0_0x) ).
cnf(and_1_x1,axiom,
( ~ mode(X47,ok)
| ~ type(X47,and)
| ~ value(out(n1,X47),n1)
| value(in(n2,X47),n1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',and_1_x1) ).
cnf(or_1x_1,axiom,
( ~ mode(X46,ok)
| ~ type(X46,or)
| ~ value(in(X45,X46),n1)
| value(out(n1,X46),n1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',or_1x_1) ).
cnf(and_1_1x,axiom,
( ~ mode(X44,ok)
| ~ type(X44,and)
| ~ value(out(n1,X44),n1)
| value(in(n1,X44),n1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',and_1_1x) ).
cnf(fulladder_connection_outch2_in1or1,axiom,
( ~ type(X43,fulladder)
| connection(out(c,h2(X43)),in(n1,or1(X43))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax',fulladder_connection_outch2_in1or1) ).
cnf(fulladder_connection_outch1_in2or1,axiom,
( ~ type(X42,fulladder)
| connection(out(c,h1(X42)),in(n2,or1(X42))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax',fulladder_connection_outch1_in2or1) ).
cnf(fulladder_connection_outsh1_in2h2,axiom,
( ~ type(X41,fulladder)
| connection(out(s,h1(X41)),in(n2,h2(X41))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax',fulladder_connection_outsh1_in2h2) ).
cnf(halfadder_connection_out1not1_in2and1,axiom,
( ~ type(X40,halfadder)
| connection(out(n1,not1(X40)),in(n2,and1(X40))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax',halfadder_connection_out1not1_in2and1) ).
cnf(halfadder_connection_out1and2_in1not1,axiom,
( ~ type(X39,halfadder)
| connection(out(n1,and2(X39)),in(n1,not1(X39))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax',halfadder_connection_out1and2_in1not1) ).
cnf(and_0_00,axiom,
( ~ mode(X38,ok)
| ~ type(X38,and)
| ~ value(out(n1,X38),n0)
| value(in(n1,X38),n0)
| value(in(n2,X38),n0) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',and_0_00) ).
cnf(halfadder_connection_out1or1_in1_and1,axiom,
( ~ type(X37,halfadder)
| connection(out(n1,or1(X37)),in(n1,and1(X37))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax',halfadder_connection_out1or1_in1_and1) ).
cnf(fulladder_connection_outc_out1or1,axiom,
( ~ type(X36,fulladder)
| connection(out(c,X36),out(n1,or1(X36))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax',fulladder_connection_outc_out1or1) ).
cnf(fulladder_connection_outs_outsh2,axiom,
( ~ type(X35,fulladder)
| connection(out(s,X35),out(s,h2(X35))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax',fulladder_connection_outs_outsh2) ).
cnf(fulladder_connection_inc_in2h1,axiom,
( ~ type(X34,fulladder)
| connection(in(c,X34),in(n2,h1(X34))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax',fulladder_connection_inc_in2h1) ).
cnf(fulladder_connection_in2_in1h1,axiom,
( ~ type(X33,fulladder)
| connection(in(n2,X33),in(n1,h1(X33))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax',fulladder_connection_in2_in1h1) ).
cnf(and_11_1,axiom,
( ~ mode(X32,ok)
| ~ type(X32,and)
| ~ value(in(n1,X32),n1)
| ~ value(in(n2,X32),n1)
| value(out(n1,X32),n1) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',and_11_1) ).
cnf(fulladder_connection_in1_in1h2,axiom,
( ~ type(X31,fulladder)
| connection(in(n1,X31),in(n1,h2(X31))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax',fulladder_connection_in1_in1h2) ).
cnf(halfadder_connection_outc_out1and2,axiom,
( ~ type(X30,halfadder)
| connection(out(c,X30),out(n1,and2(X30))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax',halfadder_connection_outc_out1and2) ).
cnf(halfadder_connection_outs_out1and1,axiom,
( ~ type(X29,halfadder)
| connection(out(s,X29),out(n1,and1(X29))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax',halfadder_connection_outs_out1and1) ).
cnf(halfadder_connection_in2_in2and2,axiom,
( ~ type(X28,halfadder)
| connection(in(n2,X28),in(n2,and2(X28))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax',halfadder_connection_in2_in2and2) ).
cnf(halfadder_connection_in1_in1and2,axiom,
( ~ type(X27,halfadder)
| connection(in(n1,X27),in(n1,and2(X27))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax',halfadder_connection_in1_in1and2) ).
cnf(and_0x_0,axiom,
( ~ mode(X26,ok)
| ~ type(X26,and)
| ~ value(in(X25,X26),n0)
| value(out(n1,X26),n0) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',and_0x_0) ).
cnf(halfadder_connection_in2_in2or1,axiom,
( ~ type(X24,halfadder)
| connection(in(n2,X24),in(n2,or1(X24))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax',halfadder_connection_in2_in2or1) ).
cnf(halfadder_connection_in1_in1or1,axiom,
( ~ type(X23,halfadder)
| connection(in(n1,X23),in(n1,or1(X23))) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax',halfadder_connection_in1_in1or1) ).
cnf(fulladder_or1,axiom,
( ~ type(X22,fulladder)
| type(or1(X22),or) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax',fulladder_or1) ).
cnf(fulladder_halfadder2,axiom,
( ~ type(X21,fulladder)
| type(h2(X21),halfadder) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax',fulladder_halfadder2) ).
cnf(fulladder_halfadder1,axiom,
( ~ type(X20,fulladder)
| type(h1(X20),halfadder) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-2.ax',fulladder_halfadder1) ).
cnf(ok_or_abnormal,axiom,
( ~ type(X19,X18)
| mode(X19,ok)
| mode(X19,abnormal) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',ok_or_abnormal) ).
cnf(halfadder_or1,axiom,
( ~ type(X17,halfadder)
| type(or1(X17),or) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax',halfadder_or1) ).
cnf(halfadder_not1,axiom,
( ~ type(X16,halfadder)
| type(not1(X16),not) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax',halfadder_not1) ).
cnf(halfadder_and2,axiom,
( ~ type(X15,halfadder)
| type(and2(X15),and) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax',halfadder_and2) ).
cnf(halfadder_and1,axiom,
( ~ type(X14,halfadder)
| type(and1(X14),and) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-1.ax',halfadder_and1) ).
cnf(unique_value,axiom,
( ~ value(X11,X9)
| ~ value(X11,X10)
| equal_value(X9,X10) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',unique_value) ).
cnf(c0,plain,
( ~ value(X13,X12)
| equal_value(X12,X12) ),
inference(factor,[status(thm)],[unique_value]) ).
cnf(value_propagation2,axiom,
( ~ connection(X8,X7)
| ~ value(X7,X6)
| value(X8,X6) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',value_propagation2) ).
cnf(value_propagation1,axiom,
( ~ connection(X5,X4)
| ~ value(X5,X3)
| value(X4,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',value_propagation1) ).
cnf(not_ok_and_abnormal,axiom,
( ~ mode(X2,ok)
| ~ mode(X2,abnormal) ),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',not_ok_and_abnormal) ).
cnf(equal_value2,axiom,
~ equal_value(n1,n0),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',equal_value2) ).
cnf(equal_value1,axiom,
~ equal_value(n0,n1),
file('/export/starexec/sandbox/benchmark/Axioms/HWV001-0.ax',equal_value1) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : HWV036-1 : TPTP v8.1.2. Released v2.5.0.
% 0.08/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n029.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Thu May 9 07:24:23 EDT 2024
% 0.15/0.37 % CPUTime :
% 0.47/0.68 % Version: 1.5
% 0.47/0.68 % SZS status Satisfiable
% 0.47/0.68 % SZS output start Saturation
% See solution above
% 0.47/0.68
% 0.47/0.68 % Initial clauses : 45
% 0.47/0.68 % Processed clauses : 46
% 0.47/0.68 % Factors computed : 1
% 0.47/0.68 % Resolvents computed: 0
% 0.47/0.68 % Tautologies deleted: 0
% 0.47/0.68 % Forward subsumed : 0
% 0.47/0.68 % Backward subsumed : 0
% 0.47/0.68 % -------- CPU Time ---------
% 0.47/0.68 % User time : 0.291 s
% 0.47/0.68 % System time : 0.014 s
% 0.47/0.68 % Total time : 0.305 s
%------------------------------------------------------------------------------