%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN100-1.005 : TPTP v8.1.2. Bugfixed v1.2.1.
% 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:47:22 EDT 2024
% Result : Unsatisfiable 0.46s 0.65s
% Output : Refutation 0.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 19
% Syntax : Number of clauses : 51 ( 20 unt; 0 nHn; 51 RR)
% Number of literals : 97 ( 0 equ; 48 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 19 ( 18 usr; 1 prp; 0-1 aty)
% Number of functors : 1 ( 1 usr; 1 con; 0-0 aty)
% Number of variables : 16 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(m_t3_1,axiom,
p_8(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_t3_1) ).
cnf(m_s3_type11_13,axiom,
( p_6(X24)
| ~ p_7(X24)
| ~ p_8(X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_s3_type11_13) ).
cnf(c0,plain,
( p_6(a)
| ~ p_7(a) ),
inference(resolution,[status(thm)],[m_s3_type11_13,m_t3_1]) ).
cnf(m_t3_2,axiom,
p_9(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_t3_2) ).
cnf(m_s3_type11_15,axiom,
( p_7(X26)
| ~ p_8(X26)
| ~ p_9(X26) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_s3_type11_15) ).
cnf(c2,plain,
( p_7(a)
| ~ p_8(a) ),
inference(resolution,[status(thm)],[m_s3_type11_15,m_t3_2]) ).
cnf(c4,plain,
p_7(a),
inference(resolution,[status(thm)],[c2,m_t3_1]) ).
cnf(c5,plain,
p_6(a),
inference(resolution,[status(thm)],[c4,c0]) ).
cnf(m_s3_type11_11,axiom,
( p_5(X22)
| ~ p_6(X22)
| ~ p_7(X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_s3_type11_11) ).
cnf(c6,plain,
( p_5(a)
| ~ p_6(a) ),
inference(resolution,[status(thm)],[c4,m_s3_type11_11]) ).
cnf(c8,plain,
p_5(a),
inference(resolution,[status(thm)],[c6,c5]) ).
cnf(m_s3_type11_9,axiom,
( p_4(X20)
| ~ p_5(X20)
| ~ p_6(X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_s3_type11_9) ).
cnf(c7,plain,
( p_4(a)
| ~ p_5(a) ),
inference(resolution,[status(thm)],[c5,m_s3_type11_9]) ).
cnf(c11,plain,
p_4(a),
inference(resolution,[status(thm)],[c7,c8]) ).
cnf(m_s3_type11_7,axiom,
( p_3(X18)
| ~ p_4(X18)
| ~ p_5(X18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_s3_type11_7) ).
cnf(c10,plain,
( p_3(a)
| ~ p_4(a) ),
inference(resolution,[status(thm)],[c8,m_s3_type11_7]) ).
cnf(c14,plain,
p_3(a),
inference(resolution,[status(thm)],[c10,c11]) ).
cnf(m_s3_type11_5,axiom,
( p_2(X16)
| ~ p_3(X16)
| ~ p_4(X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_s3_type11_5) ).
cnf(c12,plain,
( p_2(a)
| ~ p_3(a) ),
inference(resolution,[status(thm)],[c11,m_s3_type11_5]) ).
cnf(c16,plain,
p_2(a),
inference(resolution,[status(thm)],[c12,c14]) ).
cnf(m_s3_type11_3,axiom,
( p_1(X14)
| ~ p_2(X14)
| ~ p_3(X14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_s3_type11_3) ).
cnf(c15,plain,
( p_1(a)
| ~ p_2(a) ),
inference(resolution,[status(thm)],[c14,m_s3_type11_3]) ).
cnf(c19,plain,
p_1(a),
inference(resolution,[status(thm)],[c15,c16]) ).
cnf(m_s3_type11_1,axiom,
( p_0(X5)
| ~ p_1(X5)
| ~ p_2(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_s3_type11_1) ).
cnf(c18,plain,
( p_0(a)
| ~ p_1(a) ),
inference(resolution,[status(thm)],[c16,m_s3_type11_1]) ).
cnf(c20,plain,
p_0(a),
inference(resolution,[status(thm)],[c18,c19]) ).
cnf(m_s3_goal_1,negated_conjecture,
( ~ p_0(X2)
| ~ q_0(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_s3_goal_1) ).
cnf(m_s3_type12_2,axiom,
( q_0(X29)
| ~ q_1(X29)
| ~ p_2(X29) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_s3_type12_2) ).
cnf(c17,plain,
( q_0(a)
| ~ q_1(a) ),
inference(resolution,[status(thm)],[c16,m_s3_type12_2]) ).
cnf(m_s3_type12_4,axiom,
( q_1(X31)
| ~ q_2(X31)
| ~ p_3(X31) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_s3_type12_4) ).
cnf(c21,plain,
( q_1(a)
| ~ q_2(a) ),
inference(resolution,[status(thm)],[m_s3_type12_4,c14]) ).
cnf(m_s3_type12_6,axiom,
( q_2(X33)
| ~ q_3(X33)
| ~ p_4(X33) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_s3_type12_6) ).
cnf(c22,plain,
( q_2(a)
| ~ q_3(a) ),
inference(resolution,[status(thm)],[m_s3_type12_6,c11]) ).
cnf(m_s3_type12_8,axiom,
( q_3(X35)
| ~ q_4(X35)
| ~ p_5(X35) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_s3_type12_8) ).
cnf(c23,plain,
( q_3(a)
| ~ q_4(a) ),
inference(resolution,[status(thm)],[m_s3_type12_8,c8]) ).
cnf(m_s3_type12_10,axiom,
( q_4(X37)
| ~ q_5(X37)
| ~ p_6(X37) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_s3_type12_10) ).
cnf(c24,plain,
( q_4(a)
| ~ q_5(a) ),
inference(resolution,[status(thm)],[m_s3_type12_10,c5]) ).
cnf(m_s3_type12_12,axiom,
( q_5(X39)
| ~ q_6(X39)
| ~ p_7(X39) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_s3_type12_12) ).
cnf(c25,plain,
( q_5(a)
| ~ q_6(a) ),
inference(resolution,[status(thm)],[m_s3_type12_12,c4]) ).
cnf(m_t3_3,axiom,
q_8(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_t3_3) ).
cnf(m_s3_type12_13,axiom,
( q_6(X40)
| ~ p_7(X40)
| ~ q_8(X40) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',m_s3_type12_13) ).
cnf(c26,plain,
( q_6(a)
| ~ p_7(a) ),
inference(resolution,[status(thm)],[m_s3_type12_13,m_t3_3]) ).
cnf(c27,plain,
q_6(a),
inference(resolution,[status(thm)],[c26,c4]) ).
cnf(c28,plain,
q_5(a),
inference(resolution,[status(thm)],[c27,c25]) ).
cnf(c33,plain,
q_4(a),
inference(resolution,[status(thm)],[c28,c24]) ).
cnf(c39,plain,
q_3(a),
inference(resolution,[status(thm)],[c33,c23]) ).
cnf(c40,plain,
q_2(a),
inference(resolution,[status(thm)],[c39,c22]) ).
cnf(c45,plain,
q_1(a),
inference(resolution,[status(thm)],[c40,c21]) ).
cnf(c46,plain,
q_0(a),
inference(resolution,[status(thm)],[c45,c17]) ).
cnf(c48,plain,
~ p_0(a),
inference(resolution,[status(thm)],[c46,m_s3_goal_1]) ).
cnf(c49,plain,
$false,
inference(resolution,[status(thm)],[c48,c20]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SYN100-1.005 : TPTP v8.1.2. Bugfixed v1.2.1.
% 0.04/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n027.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Wed May 8 20:07:53 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.46/0.65 % Version: 1.5
% 0.46/0.65 % SZS status Unsatisfiable
% 0.46/0.65 % SZS output start CNFRefutation
% See solution above
% 0.46/0.65
% 0.46/0.65 % Initial clauses : 82
% 0.46/0.65 % Processed clauses : 83
% 0.46/0.65 % Factors computed : 0
% 0.46/0.65 % Resolvents computed: 50
% 0.46/0.65 % Tautologies deleted: 0
% 0.46/0.65 % Forward subsumed : 3
% 0.46/0.65 % Backward subsumed : 16
% 0.46/0.65 % -------- CPU Time ---------
% 0.46/0.65 % User time : 0.289 s
% 0.46/0.65 % System time : 0.014 s
% 0.46/0.65 % Total time : 0.303 s
%------------------------------------------------------------------------------