%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN718-1 : TPTP v8.1.2. Released v2.5.0.
% 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:48:43 EDT 2024
% Result : Unsatisfiable 108.80s 109.04s
% Output : Refutation 108.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 14
% Syntax : Number of clauses : 28 ( 16 unt; 0 nHn; 22 RR)
% Number of literals : 47 ( 0 equ; 20 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 11 con; 0-2 aty)
% Number of variables : 38 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(not_p57_105,negated_conjecture,
~ p57(f26(f30(c85,c70),f22(f24(c71,c79),c80)),f22(f24(c71,c83),f10(c72,c73))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_p57_105) ).
cnf(p25_23,negated_conjecture,
p25(X24,X24),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p25_23) ).
cnf(p57_76,negated_conjecture,
( p57(X316,X319)
| ~ p25(X317,X316)
| ~ p57(X317,X318)
| ~ p21(X318,X319) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p57_76) ).
cnf(p21_25,negated_conjecture,
p21(X26,X26),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p21_25) ).
cnf(p21_63,negated_conjecture,
( p21(X227,X226)
| ~ p21(X228,X227)
| ~ p21(X228,X226) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p21_63) ).
cnf(c77,plain,
( p21(X235,X234)
| ~ p21(X234,X235) ),
inference(resolution,[status(thm)],[p21_63,p21_25]) ).
cnf(p20_26,negated_conjecture,
p20(X27,X27),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p20_26) ).
cnf(p3_36,negated_conjecture,
p3(c84,f10(c72,c73)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_36) ).
cnf(p3_20,negated_conjecture,
p3(X21,X21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_20) ).
cnf(p3_58,negated_conjecture,
( p3(X187,X186)
| ~ p3(X185,X187)
| ~ p3(X185,X186) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_58) ).
cnf(c58,plain,
( p3(X191,X192)
| ~ p3(X192,X191) ),
inference(resolution,[status(thm)],[p3_58,p3_20]) ).
cnf(c61,plain,
p3(f10(c72,c73),c84),
inference(resolution,[status(thm)],[c58,p3_36]) ).
cnf(p21_101,negated_conjecture,
( p21(f22(X548,X549),f22(X546,X547))
| ~ p20(X548,X546)
| ~ p3(X549,X547) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p21_101) ).
cnf(c256,plain,
( p21(f22(X705,f10(c72,c73)),f22(X704,c84))
| ~ p20(X705,X704) ),
inference(resolution,[status(thm)],[p21_101,c61]) ).
cnf(c408,plain,
p21(f22(X706,f10(c72,c73)),f22(X706,c84)),
inference(resolution,[status(thm)],[c256,p20_26]) ).
cnf(c412,plain,
p21(f22(X707,c84),f22(X707,f10(c72,c73))),
inference(resolution,[status(thm)],[c408,c77]) ).
cnf(c414,plain,
( p57(X1071,f22(X1072,f10(c72,c73)))
| ~ p25(X1073,X1071)
| ~ p57(X1073,f22(X1072,c84)) ),
inference(resolution,[status(thm)],[c412,p57_76]) ).
cnf(p57_72,negated_conjecture,
( p57(f26(f30(c85,X291),X293),X292)
| ~ p57(f26(X291,X293),X292) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p57_72) ).
cnf(p57_81,negated_conjecture,
p57(f26(c70,f22(f24(c71,c79),c80)),f22(f24(c71,c81),c82)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p57_81) ).
cnf(c138,plain,
p57(f26(f30(c85,c70),f22(f24(c71,c79),c80)),f22(f24(c71,c81),c82)),
inference(resolution,[status(thm)],[p57_81,p57_72]) ).
cnf(p57_107,negated_conjecture,
( p57(f26(f30(c85,X603),X602),X601)
| ~ p57(f26(f30(c85,X603),X602),X600)
| ~ p57(f26(f30(c85,X603),X600),X601) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p57_107) ).
cnf(p57_80,negated_conjecture,
p57(f26(c70,f22(f24(c71,c81),c82)),f22(f24(c71,c83),c84)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p57_80) ).
cnf(c134,plain,
p57(f26(f30(c85,c70),f22(f24(c71,c81),c82)),f22(f24(c71,c83),c84)),
inference(resolution,[status(thm)],[p57_80,p57_72]) ).
cnf(c431,plain,
( p57(f26(f30(c85,c70),X1467),f22(f24(c71,c83),c84))
| ~ p57(f26(f30(c85,c70),X1467),f22(f24(c71,c81),c82)) ),
inference(resolution,[status(thm)],[c134,p57_107]) ).
cnf(c1795,plain,
p57(f26(f30(c85,c70),f22(f24(c71,c79),c80)),f22(f24(c71,c83),c84)),
inference(resolution,[status(thm)],[c431,c138]) ).
cnf(c5135,plain,
( p57(X16671,f22(f24(c71,c83),f10(c72,c73)))
| ~ p25(f26(f30(c85,c70),f22(f24(c71,c79),c80)),X16671) ),
inference(resolution,[status(thm)],[c1795,c414]) ).
cnf(c90564,plain,
p57(f26(f30(c85,c70),f22(f24(c71,c79),c80)),f22(f24(c71,c83),f10(c72,c73))),
inference(resolution,[status(thm)],[c5135,p25_23]) ).
cnf(c90566,plain,
$false,
inference(resolution,[status(thm)],[c90564,not_p57_105]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SYN718-1 : TPTP v8.1.2. Released v2.5.0.
% 0.08/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 19:45:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 108.80/109.04 % Version: 1.5
% 108.80/109.04 % SZS status Unsatisfiable
% 108.80/109.04 % SZS output start CNFRefutation
% See solution above
% 108.80/109.04
% 108.80/109.04 % Initial clauses : 118
% 108.80/109.04 % Processed clauses : 3269
% 108.80/109.04 % Factors computed : 34
% 108.80/109.04 % Resolvents computed: 90539
% 108.80/109.04 % Tautologies deleted: 2
% 108.80/109.04 % Forward subsumed : 4329
% 108.80/109.04 % Backward subsumed : 1
% 108.80/109.04 % -------- CPU Time ---------
% 108.80/109.04 % User time : 108.342 s
% 108.80/109.04 % System time : 0.336 s
% 108.80/109.04 % Total time : 108.678 s
%------------------------------------------------------------------------------