%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : HWV035-1 : TPTP v8.1.2. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n027.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.34s 0.61s
% Output : Saturation 0.34s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(or_1_11,axiom,
( ~ mode(X44,ok)
| ~ type(X44,or)
| ~ value(out(n1,X44),n1)
| value(in(n1,X44),n1)
| value(in(n2,X44),n1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',or_1_11) ).
cnf(or_00_0,axiom,
( ~ mode(X43,ok)
| ~ type(X43,or)
| ~ value(in(n1,X43),n0)
| ~ value(in(n2,X43),n0)
| value(out(n1,X43),n0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',or_00_0) ).
cnf(not_1_0_bw,axiom,
( ~ mode(X42,ok)
| ~ type(X42,not)
| ~ value(out(n1,X42),n1)
| value(in(n1,X42),n0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',not_1_0_bw) ).
cnf(not_0_1_bw,axiom,
( ~ mode(X41,ok)
| ~ type(X41,not)
| ~ value(out(n1,X41),n0)
| value(in(n1,X41),n1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',not_0_1_bw) ).
cnf(not_1_0_fw,axiom,
( ~ mode(X40,ok)
| ~ type(X40,not)
| ~ value(in(n1,X40),n1)
| value(out(n1,X40),n0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',not_1_0_fw) ).
cnf(and_0_00,axiom,
( ~ mode(X39,ok)
| ~ type(X39,and)
| ~ value(out(n1,X39),n0)
| value(in(n1,X39),n0)
| value(in(n2,X39),n0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',and_0_00) ).
cnf(not_0_1_fw,axiom,
( ~ mode(X38,ok)
| ~ type(X38,not)
| ~ value(in(n1,X38),n0)
| value(out(n1,X38),n1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',not_0_1_fw) ).
cnf(or_0_01,axiom,
( ~ mode(X37,ok)
| ~ type(X37,or)
| ~ value(out(n1,X37),n0)
| value(in(n2,X37),n0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',or_0_01) ).
cnf(or_0_0x,axiom,
( ~ mode(X36,ok)
| ~ type(X36,or)
| ~ value(out(n1,X36),n0)
| value(in(n1,X36),n0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',or_0_0x) ).
cnf(and_1_x1,axiom,
( ~ mode(X35,ok)
| ~ type(X35,and)
| ~ value(out(n1,X35),n1)
| value(in(n2,X35),n1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',and_1_x1) ).
cnf(and_1_1x,axiom,
( ~ mode(X34,ok)
| ~ type(X34,and)
| ~ value(out(n1,X34),n1)
| value(in(n1,X34),n1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',and_1_1x) ).
cnf(and_11_1,axiom,
( ~ mode(X33,ok)
| ~ type(X33,and)
| ~ value(in(n1,X33),n1)
| ~ value(in(n2,X33),n1)
| value(out(n1,X33),n1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',and_11_1) ).
cnf(or_1x_1,axiom,
( ~ mode(X32,ok)
| ~ type(X32,or)
| ~ value(in(X31,X32),n1)
| value(out(n1,X32),n1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',or_1x_1) ).
cnf(halfadder_connection_out1not1_in2and1,axiom,
( ~ type(X30,halfadder)
| connection(out(n1,not1(X30)),in(n2,and1(X30))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_connection_out1not1_in2and1) ).
cnf(halfadder_connection_out1and2_in1not1,axiom,
( ~ type(X29,halfadder)
| connection(out(n1,and2(X29)),in(n1,not1(X29))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_connection_out1and2_in1not1) ).
cnf(halfadder_connection_out1or1_in1_and1,axiom,
( ~ type(X28,halfadder)
| connection(out(n1,or1(X28)),in(n1,and1(X28))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_connection_out1or1_in1_and1) ).
cnf(halfadder_connection_outc_out1and2,axiom,
( ~ type(X27,halfadder)
| connection(out(c,X27),out(n1,and2(X27))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_connection_outc_out1and2) ).
cnf(and_0x_0,axiom,
( ~ mode(X26,ok)
| ~ type(X26,and)
| ~ value(in(X25,X26),n0)
| value(out(n1,X26),n0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',and_0x_0) ).
cnf(halfadder_connection_outs_out1and1,axiom,
( ~ type(X24,halfadder)
| connection(out(s,X24),out(n1,and1(X24))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_connection_outs_out1and1) ).
cnf(halfadder_connection_in2_in2and2,axiom,
( ~ type(X23,halfadder)
| connection(in(n2,X23),in(n2,and2(X23))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_connection_in2_in2and2) ).
cnf(halfadder_connection_in1_in1and2,axiom,
( ~ type(X22,halfadder)
| connection(in(n1,X22),in(n1,and2(X22))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_connection_in1_in1and2) ).
cnf(halfadder_connection_in2_in2or1,axiom,
( ~ type(X21,halfadder)
| connection(in(n2,X21),in(n2,or1(X21))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_connection_in2_in2or1) ).
cnf(halfadder_connection_in1_in1or1,axiom,
( ~ type(X20,halfadder)
| connection(in(n1,X20),in(n1,or1(X20))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_connection_in1_in1or1) ).
cnf(ok_or_abnormal,axiom,
( ~ type(X19,X18)
| mode(X19,ok)
| mode(X19,abnormal) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',ok_or_abnormal) ).
cnf(halfadder_or1,axiom,
( ~ type(X17,halfadder)
| type(or1(X17),or) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_or1) ).
cnf(halfadder_not1,axiom,
( ~ type(X16,halfadder)
| type(not1(X16),not) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_not1) ).
cnf(halfadder_and2,axiom,
( ~ type(X15,halfadder)
| type(and2(X15),and) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_and2) ).
cnf(halfadder_and1,axiom,
( ~ type(X14,halfadder)
| type(and1(X14),and) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-1.ax',halfadder_and1) ).
cnf(unique_value,axiom,
( ~ value(X10,X11)
| ~ value(X10,X9)
| equal_value(X11,X9) ),
file('/export/starexec/sandbox2/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(X7,X6)
| ~ value(X6,X8)
| value(X7,X8) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',value_propagation2) ).
cnf(value_propagation1,axiom,
( ~ connection(X4,X3)
| ~ value(X4,X5)
| value(X3,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',value_propagation1) ).
cnf(not_ok_and_abnormal,axiom,
( ~ mode(X2,ok)
| ~ mode(X2,abnormal) ),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',not_ok_and_abnormal) ).
cnf(equal_value2,axiom,
~ equal_value(n1,n0),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',equal_value2) ).
cnf(equal_value1,axiom,
~ equal_value(n0,n1),
file('/export/starexec/sandbox2/benchmark/Axioms/HWV001-0.ax',equal_value1) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.16 % Problem : HWV035-1 : TPTP v8.1.2. Released v2.5.0.
% 0.03/0.17 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.38 % Computer : n027.cluster.edu
% 0.14/0.38 % Model : x86_64 x86_64
% 0.14/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.38 % Memory : 8042.1875MB
% 0.14/0.38 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.38 % CPULimit : 300
% 0.14/0.38 % WCLimit : 300
% 0.14/0.38 % DateTime : Thu May 9 07:35:08 EDT 2024
% 0.14/0.38 % CPUTime :
% 0.34/0.61 % Version: 1.5
% 0.34/0.61 % SZS status Satisfiable
% 0.34/0.61 % SZS output start Saturation
% See solution above
% 0.34/0.61
% 0.34/0.61 % Initial clauses : 34
% 0.34/0.61 % Processed clauses : 35
% 0.34/0.61 % Factors computed : 1
% 0.34/0.61 % Resolvents computed: 0
% 0.34/0.61 % Tautologies deleted: 0
% 0.34/0.61 % Forward subsumed : 0
% 0.34/0.61 % Backward subsumed : 0
% 0.34/0.61 % -------- CPU Time ---------
% 0.34/0.61 % User time : 0.211 s
% 0.34/0.61 % System time : 0.013 s
% 0.34/0.61 % Total time : 0.224 s
%------------------------------------------------------------------------------