%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN627-1 : TPTP v8.1.2. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n010.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:48:34 EDT 2024
% Result : Unsatisfiable 0.52s 0.69s
% Output : Refutation 0.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 11
% Syntax : Number of clauses : 25 ( 15 unt; 0 nHn; 22 RR)
% Number of literals : 38 ( 0 equ; 14 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-5 aty)
% Number of functors : 13 ( 13 usr; 9 con; 0-2 aty)
% Number of variables : 24 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(not_p3_8,negated_conjecture,
~ p3(c23,c24),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_p3_8) ).
cnf(p3_18,negated_conjecture,
( p3(X46,X44)
| ~ p3(X45,X46)
| ~ p3(X45,X44) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p3_18) ).
cnf(p3_9,negated_conjecture,
p3(c23,f4(f7(c17,c18),c21)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p3_9) ).
cnf(p3_5,negated_conjecture,
p3(X6,X6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p3_5) ).
cnf(c15,plain,
( p3(X55,X54)
| ~ p3(X54,X55) ),
inference(resolution,[status(thm)],[p3_18,p3_5]) ).
cnf(c19,plain,
p3(f4(f7(c17,c18),c21),c23),
inference(resolution,[status(thm)],[c15,p3_9]) ).
cnf(c24,plain,
( p3(X110,c23)
| ~ p3(f4(f7(c17,c18),c21),X110) ),
inference(resolution,[status(thm)],[c19,p3_18]) ).
cnf(p2_6,negated_conjecture,
p2(X7,X7),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p2_6) ).
cnf(p3_27,negated_conjecture,
( p3(f4(X97,X94),f4(X96,X95))
| ~ p2(X97,X96)
| ~ p3(X94,X95) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p3_27) ).
cnf(p15_7,negated_conjecture,
p15(c18,c19),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p15_7) ).
cnf(p16_23,negated_conjecture,
( p16(c17,c20,f9(c19,X88),f14(X88),c25)
| ~ p15(X88,c19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p16_23) ).
cnf(c42,plain,
p16(c17,c20,f9(c19,c18),f14(c18),c25),
inference(resolution,[status(thm)],[p16_23,p15_7]) ).
cnf(p16_10,negated_conjecture,
p16(c17,c20,f9(c19,c18),c21,c22),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p16_10) ).
cnf(p3_28,negated_conjecture,
( p3(X106,X105)
| ~ p16(c17,c20,X103,X105,X104)
| ~ p16(c17,c20,X103,X106,c22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p3_28) ).
cnf(c53,plain,
( p3(c21,X117)
| ~ p16(c17,c20,f9(c19,c18),X117,X118) ),
inference(resolution,[status(thm)],[p3_28,p16_10]) ).
cnf(c63,plain,
p3(c21,f14(c18)),
inference(resolution,[status(thm)],[c53,c42]) ).
cnf(c68,plain,
( p3(f4(X164,c21),f4(X165,f14(c18)))
| ~ p2(X164,X165) ),
inference(resolution,[status(thm)],[c63,p3_27]) ).
cnf(c130,plain,
p3(f4(X166,c21),f4(X166,f14(c18))),
inference(resolution,[status(thm)],[c68,p2_6]) ).
cnf(c135,plain,
p3(f4(f7(c17,c18),f14(c18)),c23),
inference(resolution,[status(thm)],[c130,c24]) ).
cnf(p3_20,negated_conjecture,
( p3(c24,f4(f7(c17,X65),f14(X65)))
| ~ p15(X65,c19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p3_20) ).
cnf(c25,plain,
p3(c24,f4(f7(c17,c18),f14(c18))),
inference(resolution,[status(thm)],[p3_20,p15_7]) ).
cnf(c30,plain,
p3(f4(f7(c17,c18),f14(c18)),c24),
inference(resolution,[status(thm)],[c25,c15]) ).
cnf(c35,plain,
( p3(X175,c24)
| ~ p3(f4(f7(c17,c18),f14(c18)),X175) ),
inference(resolution,[status(thm)],[c30,p3_18]) ).
cnf(c166,plain,
p3(c23,c24),
inference(resolution,[status(thm)],[c35,c135]) ).
cnf(c173,plain,
$false,
inference(resolution,[status(thm)],[c166,not_p3_8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYN627-1 : TPTP v8.1.2. Released v2.5.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n010.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed May 8 20:17:08 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.52/0.69 % Version: 1.5
% 0.52/0.69 % SZS status Unsatisfiable
% 0.52/0.69 % SZS output start CNFRefutation
% See solution above
% 0.52/0.69
% 0.52/0.69 % Initial clauses : 36
% 0.52/0.69 % Processed clauses : 81
% 0.52/0.69 % Factors computed : 9
% 0.52/0.69 % Resolvents computed: 167
% 0.52/0.69 % Tautologies deleted: 0
% 0.52/0.69 % Forward subsumed : 52
% 0.52/0.69 % Backward subsumed : 0
% 0.52/0.69 % -------- CPU Time ---------
% 0.52/0.69 % User time : 0.323 s
% 0.52/0.69 % System time : 0.016 s
% 0.52/0.69 % Total time : 0.339 s
%------------------------------------------------------------------------------