%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN625-1 : TPTP v8.1.2. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n012.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 1.00s 1.15s
% Output : Refutation 1.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 9
% Syntax : Number of clauses : 24 ( 6 unt; 15 nHn; 13 RR)
% Number of literals : 53 ( 0 equ; 15 neg)
% Maximal clause size : 3 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-5 aty)
% Number of variables : 52 ( 1 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(f4_is_not_p15_8,negated_conjecture,
~ p15(f4(f7(c19,c20),c21)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f4_is_not_p15_8) ).
cnf(c21_is_p15_1,negated_conjecture,
p15(c21),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c21_is_p15_1) ).
cnf(not_p15_10,negated_conjecture,
( ~ p15(X14)
| ~ p18(f9(X14),X13,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_p15_10) ).
cnf(p15_15,negated_conjecture,
( p15(X35)
| p18(f9(X35),f14(X35),f14(X35)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p15_15) ).
cnf(p18_33,negated_conjecture,
( p18(f9(X185),X188,X186)
| p17(f12(X185,X187,X189,X188,X186),f11(X189))
| ~ p18(f9(f4(f7(X187,X189),X185)),X188,X186) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p18_33) ).
cnf(c49,plain,
( p18(f9(X274),f14(f4(f7(X272,X273),X274)),f14(f4(f7(X272,X273),X274)))
| p17(f12(X274,X272,X273,f14(f4(f7(X272,X273),X274)),f14(f4(f7(X272,X273),X274))),f11(X273))
| p15(f4(f7(X272,X273),X274)) ),
inference(resolution,[status(thm)],[p18_33,p15_15]) ).
cnf(c97,plain,
( p17(f12(X417,X415,X416,f14(f4(f7(X415,X416),X417)),f14(f4(f7(X415,X416),X417))),f11(X416))
| p15(f4(f7(X415,X416),X417))
| ~ p15(X417) ),
inference(resolution,[status(thm)],[c49,not_p15_10]) ).
cnf(c170,plain,
( p17(f12(c21,X418,X419,f14(f4(f7(X418,X419),c21)),f14(f4(f7(X418,X419),c21))),f11(X419))
| p15(f4(f7(X418,X419),c21)) ),
inference(resolution,[status(thm)],[c97,c21_is_p15_1]) ).
cnf(c178,plain,
p17(f12(c21,c19,c20,f14(f4(f7(c19,c20),c21)),f14(f4(f7(c19,c20),c21))),f11(c20)),
inference(resolution,[status(thm)],[c170,f4_is_not_p15_8]) ).
cnf(not_p17_16,negated_conjecture,
( ~ p17(X45,f11(c20))
| ~ p16(f9(c21),X45,c19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',not_p17_16) ).
cnf(p16_23,negated_conjecture,
( p16(X79,X78,X81)
| ~ p16(X79,X78,X80)
| ~ p16(X79,X80,X81) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p16_23) ).
cnf(p16_32,negated_conjecture,
( p16(f9(X162),X165,X164)
| p18(f9(X162),X165,X163)
| ~ p18(f9(f4(f7(X164,X166),X162)),X165,X163) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p16_32) ).
cnf(c44,plain,
( p16(f9(X260),f14(f4(f7(X261,X262),X260)),X261)
| p18(f9(X260),f14(f4(f7(X261,X262),X260)),f14(f4(f7(X261,X262),X260)))
| p15(f4(f7(X261,X262),X260)) ),
inference(resolution,[status(thm)],[p16_32,p15_15]) ).
cnf(c76,plain,
( p16(f9(X269),f14(f4(f7(X268,X267),X269)),X268)
| p15(f4(f7(X268,X267),X269))
| ~ p15(X269) ),
inference(resolution,[status(thm)],[c44,not_p15_10]) ).
cnf(c82,plain,
( p16(f9(c21),f14(f4(f7(X270,X271),c21)),X270)
| p15(f4(f7(X270,X271),c21)) ),
inference(resolution,[status(thm)],[c76,c21_is_p15_1]) ).
cnf(c85,plain,
( p15(f4(f7(X388,X389),c21))
| p16(f9(c21),X390,X388)
| ~ p16(f9(c21),X390,f14(f4(f7(X388,X389),c21))) ),
inference(resolution,[status(thm)],[c82,p16_23]) ).
cnf(p18_34,negated_conjecture,
( p18(f9(X201),X204,X202)
| p16(f9(X201),f12(X201,X203,X205,X204,X202),X202)
| ~ p18(f9(f4(f7(X203,X205),X201)),X204,X202) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p18_34) ).
cnf(c53,plain,
( p18(f9(X292),f14(f4(f7(X291,X293),X292)),f14(f4(f7(X291,X293),X292)))
| p16(f9(X292),f12(X292,X291,X293,f14(f4(f7(X291,X293),X292)),f14(f4(f7(X291,X293),X292))),f14(f4(f7(X291,X293),X292)))
| p15(f4(f7(X291,X293),X292)) ),
inference(resolution,[status(thm)],[p18_34,p15_15]) ).
cnf(c109,plain,
( p16(f9(X562),f12(X562,X561,X563,f14(f4(f7(X561,X563),X562)),f14(f4(f7(X561,X563),X562))),f14(f4(f7(X561,X563),X562)))
| p15(f4(f7(X561,X563),X562))
| ~ p15(X562) ),
inference(resolution,[status(thm)],[c53,not_p15_10]) ).
cnf(c682,plain,
( p16(f9(c21),f12(c21,X677,X676,f14(f4(f7(X677,X676),c21)),f14(f4(f7(X677,X676),c21))),f14(f4(f7(X677,X676),c21)))
| p15(f4(f7(X677,X676),c21)) ),
inference(resolution,[status(thm)],[c109,c21_is_p15_1]) ).
cnf(c1093,plain,
( p15(f4(f7(X679,X678),c21))
| p16(f9(c21),f12(c21,X679,X678,f14(f4(f7(X679,X678),c21)),f14(f4(f7(X679,X678),c21))),X679) ),
inference(resolution,[status(thm)],[c682,c85]) ).
cnf(c1103,plain,
p16(f9(c21),f12(c21,c19,c20,f14(f4(f7(c19,c20),c21)),f14(f4(f7(c19,c20),c21))),c19),
inference(resolution,[status(thm)],[c1093,f4_is_not_p15_8]) ).
cnf(c1123,plain,
~ p17(f12(c21,c19,c20,f14(f4(f7(c19,c20),c21)),f14(f4(f7(c19,c20),c21))),f11(c20)),
inference(resolution,[status(thm)],[c1103,not_p17_16]) ).
cnf(c1137,plain,
$false,
inference(resolution,[status(thm)],[c1123,c178]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SYN625-1 : TPTP v8.1.2. Released v2.5.0.
% 0.04/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.33 % Computer : n012.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Wed May 8 20:30:22 EDT 2024
% 0.13/0.33 % CPUTime :
% 1.00/1.15 % Version: 1.5
% 1.00/1.15 % SZS status Unsatisfiable
% 1.00/1.15 % SZS output start CNFRefutation
% See solution above
% 1.00/1.15
% 1.00/1.15 % Initial clauses : 35
% 1.00/1.15 % Processed clauses : 180
% 1.00/1.15 % Factors computed : 20
% 1.00/1.15 % Resolvents computed: 1121
% 1.00/1.15 % Tautologies deleted: 6
% 1.00/1.15 % Forward subsumed : 91
% 1.00/1.15 % Backward subsumed : 4
% 1.00/1.15 % -------- CPU Time ---------
% 1.00/1.15 % User time : 0.785 s
% 1.00/1.15 % System time : 0.027 s
% 1.00/1.15 % Total time : 0.812 s
%------------------------------------------------------------------------------