%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN096-1.008 : TPTP v8.1.2. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n018.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:47:22 EDT 2024
% Result : Unsatisfiable 0.41s 0.61s
% Output : Refutation 0.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 31
% Syntax : Number of clauses : 87 ( 32 unt; 0 nHn; 87 RR)
% Number of literals : 169 ( 0 equ; 84 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 31 ( 30 usr; 1 prp; 0-1 aty)
% Number of functors : 1 ( 1 usr; 1 con; 0-0 aty)
% Number of variables : 28 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(m_t3_1,axiom,
p_14(a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_t3_1) ).
cnf(m_s3_type11_25,axiom,
( p_12(X31)
| ~ p_13(X31)
| ~ p_14(X31) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type11_25) ).
cnf(c0,plain,
( p_12(a)
| ~ p_13(a) ),
inference(resolution,[status(thm)],[m_s3_type11_25,m_t3_1]) ).
cnf(m_t3_2,axiom,
p_15(a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_t3_2) ).
cnf(m_s3_type11_27,axiom,
( p_13(X33)
| ~ p_14(X33)
| ~ p_15(X33) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type11_27) ).
cnf(c2,plain,
( p_13(a)
| ~ p_14(a) ),
inference(resolution,[status(thm)],[m_s3_type11_27,m_t3_2]) ).
cnf(c3,plain,
p_13(a),
inference(resolution,[status(thm)],[c2,m_t3_1]) ).
cnf(c5,plain,
p_12(a),
inference(resolution,[status(thm)],[c3,c0]) ).
cnf(m_s3_type11_23,axiom,
( p_11(X29)
| ~ p_12(X29)
| ~ p_13(X29) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type11_23) ).
cnf(c4,plain,
( p_11(a)
| ~ p_12(a) ),
inference(resolution,[status(thm)],[c3,m_s3_type11_23]) ).
cnf(c8,plain,
p_11(a),
inference(resolution,[status(thm)],[c4,c5]) ).
cnf(m_s3_type11_21,axiom,
( p_10(X27)
| ~ p_11(X27)
| ~ p_12(X27) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type11_21) ).
cnf(c6,plain,
( p_10(a)
| ~ p_11(a) ),
inference(resolution,[status(thm)],[c5,m_s3_type11_21]) ).
cnf(c10,plain,
p_10(a),
inference(resolution,[status(thm)],[c6,c8]) ).
cnf(m_s3_type11_19,axiom,
( p_9(X25)
| ~ p_10(X25)
| ~ p_11(X25) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type11_19) ).
cnf(c9,plain,
( p_9(a)
| ~ p_10(a) ),
inference(resolution,[status(thm)],[c8,m_s3_type11_19]) ).
cnf(c12,plain,
p_9(a),
inference(resolution,[status(thm)],[c9,c10]) ).
cnf(m_s3_type11_17,axiom,
( p_8(X23)
| ~ p_9(X23)
| ~ p_10(X23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type11_17) ).
cnf(c11,plain,
( p_8(a)
| ~ p_9(a) ),
inference(resolution,[status(thm)],[c10,m_s3_type11_17]) ).
cnf(c14,plain,
p_8(a),
inference(resolution,[status(thm)],[c11,c12]) ).
cnf(m_s3_type11_15,axiom,
( p_7(X21)
| ~ p_8(X21)
| ~ p_9(X21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type11_15) ).
cnf(c13,plain,
( p_7(a)
| ~ p_8(a) ),
inference(resolution,[status(thm)],[c12,m_s3_type11_15]) ).
cnf(c17,plain,
p_7(a),
inference(resolution,[status(thm)],[c13,c14]) ).
cnf(m_s3_type11_13,axiom,
( p_6(X19)
| ~ p_7(X19)
| ~ p_8(X19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type11_13) ).
cnf(c15,plain,
( p_6(a)
| ~ p_7(a) ),
inference(resolution,[status(thm)],[c14,m_s3_type11_13]) ).
cnf(c20,plain,
p_6(a),
inference(resolution,[status(thm)],[c15,c17]) ).
cnf(m_s3_type11_11,axiom,
( p_5(X17)
| ~ p_6(X17)
| ~ p_7(X17) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type11_11) ).
cnf(c18,plain,
( p_5(a)
| ~ p_6(a) ),
inference(resolution,[status(thm)],[c17,m_s3_type11_11]) ).
cnf(c22,plain,
p_5(a),
inference(resolution,[status(thm)],[c18,c20]) ).
cnf(m_s3_type11_9,axiom,
( p_4(X15)
| ~ p_5(X15)
| ~ p_6(X15) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type11_9) ).
cnf(c21,plain,
( p_4(a)
| ~ p_5(a) ),
inference(resolution,[status(thm)],[c20,m_s3_type11_9]) ).
cnf(c24,plain,
p_4(a),
inference(resolution,[status(thm)],[c21,c22]) ).
cnf(m_s3_type11_7,axiom,
( p_3(X13)
| ~ p_4(X13)
| ~ p_5(X13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type11_7) ).
cnf(c23,plain,
( p_3(a)
| ~ p_4(a) ),
inference(resolution,[status(thm)],[c22,m_s3_type11_7]) ).
cnf(c26,plain,
p_3(a),
inference(resolution,[status(thm)],[c23,c24]) ).
cnf(m_s3_type11_5,axiom,
( p_2(X11)
| ~ p_3(X11)
| ~ p_4(X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type11_5) ).
cnf(c25,plain,
( p_2(a)
| ~ p_3(a) ),
inference(resolution,[status(thm)],[c24,m_s3_type11_5]) ).
cnf(c29,plain,
p_2(a),
inference(resolution,[status(thm)],[c25,c26]) ).
cnf(m_s3_type11_3,axiom,
( p_1(X9)
| ~ p_2(X9)
| ~ p_3(X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type11_3) ).
cnf(c27,plain,
( p_1(a)
| ~ p_2(a) ),
inference(resolution,[status(thm)],[c26,m_s3_type11_3]) ).
cnf(c32,plain,
p_1(a),
inference(resolution,[status(thm)],[c27,c29]) ).
cnf(m_s3_type11_1,axiom,
( p_0(X3)
| ~ p_1(X3)
| ~ p_2(X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type11_1) ).
cnf(c31,plain,
( p_0(a)
| ~ p_1(a) ),
inference(resolution,[status(thm)],[c29,m_s3_type11_1]) ).
cnf(c33,plain,
p_0(a),
inference(resolution,[status(thm)],[c31,c32]) ).
cnf(m_s3_goal_1,negated_conjecture,
( ~ p_0(X2)
| ~ q_0(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_goal_1) ).
cnf(m_s3_type12_2,axiom,
( q_0(X36)
| ~ q_1(X36)
| ~ p_2(X36) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type12_2) ).
cnf(c30,plain,
( q_0(a)
| ~ q_1(a) ),
inference(resolution,[status(thm)],[c29,m_s3_type12_2]) ).
cnf(m_s3_type12_4,axiom,
( q_1(X38)
| ~ q_2(X38)
| ~ p_3(X38) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type12_4) ).
cnf(c28,plain,
( q_1(a)
| ~ q_2(a) ),
inference(resolution,[status(thm)],[c26,m_s3_type12_4]) ).
cnf(m_s3_type12_6,axiom,
( q_2(X40)
| ~ q_3(X40)
| ~ p_4(X40) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type12_6) ).
cnf(c34,plain,
( q_2(a)
| ~ q_3(a) ),
inference(resolution,[status(thm)],[m_s3_type12_6,c24]) ).
cnf(m_s3_type12_8,axiom,
( q_3(X42)
| ~ q_4(X42)
| ~ p_5(X42) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type12_8) ).
cnf(c35,plain,
( q_3(a)
| ~ q_4(a) ),
inference(resolution,[status(thm)],[m_s3_type12_8,c22]) ).
cnf(m_s3_type12_10,axiom,
( q_4(X44)
| ~ q_5(X44)
| ~ p_6(X44) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type12_10) ).
cnf(c36,plain,
( q_4(a)
| ~ q_5(a) ),
inference(resolution,[status(thm)],[m_s3_type12_10,c20]) ).
cnf(m_s3_type12_12,axiom,
( q_5(X46)
| ~ q_6(X46)
| ~ p_7(X46) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type12_12) ).
cnf(c37,plain,
( q_5(a)
| ~ q_6(a) ),
inference(resolution,[status(thm)],[m_s3_type12_12,c17]) ).
cnf(m_s3_type12_14,axiom,
( q_6(X48)
| ~ q_7(X48)
| ~ p_8(X48) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type12_14) ).
cnf(c38,plain,
( q_6(a)
| ~ q_7(a) ),
inference(resolution,[status(thm)],[m_s3_type12_14,c14]) ).
cnf(m_s3_type12_16,axiom,
( q_7(X50)
| ~ q_8(X50)
| ~ p_9(X50) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type12_16) ).
cnf(c39,plain,
( q_7(a)
| ~ q_8(a) ),
inference(resolution,[status(thm)],[m_s3_type12_16,c12]) ).
cnf(m_s3_type12_18,axiom,
( q_8(X52)
| ~ q_9(X52)
| ~ p_10(X52) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type12_18) ).
cnf(c40,plain,
( q_8(a)
| ~ q_9(a) ),
inference(resolution,[status(thm)],[m_s3_type12_18,c10]) ).
cnf(m_s3_type12_20,axiom,
( q_9(X54)
| ~ q_10(X54)
| ~ p_11(X54) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type12_20) ).
cnf(c41,plain,
( q_9(a)
| ~ q_10(a) ),
inference(resolution,[status(thm)],[m_s3_type12_20,c8]) ).
cnf(m_s3_type12_22,axiom,
( q_10(X56)
| ~ q_11(X56)
| ~ p_12(X56) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type12_22) ).
cnf(c42,plain,
( q_10(a)
| ~ q_11(a) ),
inference(resolution,[status(thm)],[m_s3_type12_22,c5]) ).
cnf(m_s3_type12_24,axiom,
( q_11(X58)
| ~ q_12(X58)
| ~ p_13(X58) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type12_24) ).
cnf(c43,plain,
( q_11(a)
| ~ q_12(a) ),
inference(resolution,[status(thm)],[m_s3_type12_24,c3]) ).
cnf(m_t3_3,axiom,
q_14(a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_t3_3) ).
cnf(m_s3_type12_25,axiom,
( q_12(X59)
| ~ p_13(X59)
| ~ q_14(X59) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',m_s3_type12_25) ).
cnf(c44,plain,
( q_12(a)
| ~ p_13(a) ),
inference(resolution,[status(thm)],[m_s3_type12_25,m_t3_3]) ).
cnf(c45,plain,
q_12(a),
inference(resolution,[status(thm)],[c44,c3]) ).
cnf(c47,plain,
q_11(a),
inference(resolution,[status(thm)],[c45,c43]) ).
cnf(c51,plain,
q_10(a),
inference(resolution,[status(thm)],[c47,c42]) ).
cnf(c55,plain,
q_9(a),
inference(resolution,[status(thm)],[c51,c41]) ).
cnf(c58,plain,
q_8(a),
inference(resolution,[status(thm)],[c55,c40]) ).
cnf(c60,plain,
q_7(a),
inference(resolution,[status(thm)],[c58,c39]) ).
cnf(c65,plain,
q_6(a),
inference(resolution,[status(thm)],[c60,c38]) ).
cnf(c69,plain,
q_5(a),
inference(resolution,[status(thm)],[c65,c37]) ).
cnf(c73,plain,
q_4(a),
inference(resolution,[status(thm)],[c69,c36]) ).
cnf(c76,plain,
q_3(a),
inference(resolution,[status(thm)],[c73,c35]) ).
cnf(c79,plain,
q_2(a),
inference(resolution,[status(thm)],[c76,c34]) ).
cnf(c81,plain,
q_1(a),
inference(resolution,[status(thm)],[c79,c28]) ).
cnf(c84,plain,
q_0(a),
inference(resolution,[status(thm)],[c81,c30]) ).
cnf(c85,plain,
~ p_0(a),
inference(resolution,[status(thm)],[c84,m_s3_goal_1]) ).
cnf(c86,plain,
$false,
inference(resolution,[status(thm)],[c85,c33]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SYN096-1.008 : TPTP v8.1.2. Bugfixed v1.2.1.
% 0.13/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n018.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 20:14:38 EDT 2024
% 0.20/0.35 % CPUTime :
% 0.41/0.61 % Version: 1.5
% 0.41/0.61 % SZS status Unsatisfiable
% 0.41/0.61 % SZS output start CNFRefutation
% See solution above
% 0.41/0.61
% 0.41/0.61 % Initial clauses : 65
% 0.41/0.61 % Processed clauses : 123
% 0.41/0.61 % Factors computed : 0
% 0.41/0.61 % Resolvents computed: 87
% 0.41/0.61 % Tautologies deleted: 0
% 0.41/0.61 % Forward subsumed : 4
% 0.41/0.61 % Backward subsumed : 28
% 0.41/0.61 % -------- CPU Time ---------
% 0.41/0.61 % User time : 0.229 s
% 0.41/0.61 % System time : 0.023 s
% 0.41/0.61 % Total time : 0.253 s
%------------------------------------------------------------------------------