%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN713-1 : TPTP v8.1.2. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n004.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:42 EDT 2024
% Result : Unsatisfiable 0.80s 0.97s
% Output : Refutation 0.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 13
% Syntax : Number of clauses : 25 ( 14 unt; 2 nHn; 19 RR)
% Number of literals : 42 ( 0 equ; 17 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 11 ( 10 usr; 1 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 15 con; 0-2 aty)
% Number of variables : 36 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(not_p57_39,negated_conjecture,
~ p57(f26(f28(c71,f41(c78,c64)),c67),c77),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_p57_39) ).
cnf(p57_74,negated_conjecture,
( p57(f26(f28(c71,X305),X306),X307)
| ~ p57(f26(X305,X306),X307) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p57_74) ).
cnf(p57_101,negated_conjecture,
( p57(f26(f41(c78,X521),X523),X522)
| ~ p56(f11(c65,f14(f17(c66,X523),f23(c74,X522))),X521) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p57_101) ).
cnf(p40_14,negated_conjecture,
p40(X15,X15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p40_14) ).
cnf(p56_38,negated_conjecture,
p56(f11(c65,f14(f17(c66,c67),c68)),c64),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p56_38) ).
cnf(p56_76,negated_conjecture,
( p56(X319,X320)
| ~ p40(X321,X320)
| ~ p56(X318,X321)
| ~ p4(X318,X319) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p56_76) ).
cnf(p9_2,negated_conjecture,
p9(X3,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p9_2) ).
cnf(p4_87,negated_conjecture,
( p4(f11(X398,X396),f11(X397,X395))
| ~ p10(X396,X395)
| ~ p9(X398,X397) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p4_87) ).
cnf(c126,plain,
( p4(f11(X405,X404),f11(X405,X406))
| ~ p10(X404,X406) ),
inference(resolution,[status(thm)],[p4_87,p9_2]) ).
cnf(p12_34,negated_conjecture,
p12(X35,X35),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p12_34) ).
cnf(p10_81,negated_conjecture,
( p10(f14(X348,X349),f14(X347,X346))
| ~ p12(X348,X347)
| ~ p13(X349,X346) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p10_81) ).
cnf(not_p58_80,negated_conjecture,
~ p58(f31(f33(c75,c76),f23(c69,c77)),f19(f22(c70,c69),c68)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_p58_80) ).
cnf(p59_35,negated_conjecture,
p59(f38(c72,c77),f35(c73,c68)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p59_35) ).
cnf(p13_105,negated_conjecture,
( p13(X548,f23(c74,X547))
| p58(f31(f33(c75,c76),f23(c69,X547)),f19(f22(c70,c69),X548))
| ~ p59(f38(c72,X547),f35(c73,X548)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p13_105) ).
cnf(c189,plain,
( p13(c68,f23(c74,c77))
| p58(f31(f33(c75,c76),f23(c69,c77)),f19(f22(c70,c69),c68)) ),
inference(resolution,[status(thm)],[p13_105,p59_35]) ).
cnf(c263,plain,
p13(c68,f23(c74,c77)),
inference(resolution,[status(thm)],[c189,not_p58_80]) ).
cnf(c269,plain,
( p10(f14(X672,c68),f14(X671,f23(c74,c77)))
| ~ p12(X672,X671) ),
inference(resolution,[status(thm)],[c263,p10_81]) ).
cnf(c324,plain,
p10(f14(X673,c68),f14(X673,f23(c74,c77))),
inference(resolution,[status(thm)],[c269,p12_34]) ).
cnf(c327,plain,
p4(f11(X758,f14(X757,c68)),f11(X758,f14(X757,f23(c74,c77)))),
inference(resolution,[status(thm)],[c324,c126]) ).
cnf(c422,plain,
( p56(f11(X1132,f14(X1133,f23(c74,c77))),X1135)
| ~ p40(X1134,X1135)
| ~ p56(f11(X1132,f14(X1133,c68)),X1134) ),
inference(resolution,[status(thm)],[c327,p56_76]) ).
cnf(c627,plain,
( p56(f11(c65,f14(f17(c66,c67),f23(c74,c77))),X1136)
| ~ p40(c64,X1136) ),
inference(resolution,[status(thm)],[c422,p56_38]) ).
cnf(c628,plain,
p56(f11(c65,f14(f17(c66,c67),f23(c74,c77))),c64),
inference(resolution,[status(thm)],[c627,p40_14]) ).
cnf(c632,plain,
p57(f26(f41(c78,c64),c67),c77),
inference(resolution,[status(thm)],[c628,p57_101]) ).
cnf(c634,plain,
p57(f26(f28(c71,f41(c78,c64)),c67),c77),
inference(resolution,[status(thm)],[c632,p57_74]) ).
cnf(c637,plain,
$false,
inference(resolution,[status(thm)],[c634,not_p57_39]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYN713-1 : TPTP v8.1.2. Released v2.5.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.33 % Computer : n004.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:13:08 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.80/0.97 % Version: 1.5
% 0.80/0.97 % SZS status Unsatisfiable
% 0.80/0.97 % SZS output start CNFRefutation
% See solution above
% 0.80/0.97
% 0.80/0.97 % Initial clauses : 105
% 0.80/0.97 % Processed clauses : 336
% 0.80/0.97 % Factors computed : 34
% 0.80/0.97 % Resolvents computed: 606
% 0.80/0.97 % Tautologies deleted: 0
% 0.80/0.97 % Forward subsumed : 273
% 0.80/0.97 % Backward subsumed : 1
% 0.80/0.97 % -------- CPU Time ---------
% 0.80/0.97 % User time : 0.615 s
% 0.80/0.97 % System time : 0.014 s
% 0.80/0.97 % Total time : 0.629 s
%------------------------------------------------------------------------------