%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN708-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 09:39:10 AM UTC 2026
% Result : Unsatisfiable 0.14s 5.55s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 13
% Syntax : Number of formulae : 40 ( 20 unt; 0 def)
% Number of atoms : 74 ( 0 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 73 ( 39 ~; 34 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 13 ( 4 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 3 con; 0-2 aty)
% Number of variables : 38 ( 0 sgn 16 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(c56_is_p38_1,axiom,
p38(c56),
file('theBenchmark.p',c56_is_p38_1) ).
cnf(c_1,plain,
p38(c56),
inference(clausify,[status(thm)],[c56_is_p38_1]) ).
fof(p10_3,axiom,
! [VAR_0] : p10(VAR_0,VAR_0),
file('theBenchmark.p',p10_3) ).
cnf(c_3,plain,
p10(A,A),
inference(clausify,[status(thm)],[p10_3]) ).
fof(p37_13,axiom,
p37(f15(c56),c48),
file('theBenchmark.p',p37_13) ).
cnf(c_13,plain,
p37(f15(c56),c48),
inference(clausify,[status(thm)],[p37_13]) ).
fof(p38_15,axiom,
! [VAR_0] :
( ~ p38(VAR_0)
| p38(f15(VAR_0)) ),
file('theBenchmark.p',p38_15) ).
cnf(c_15,plain,
( ~ p38(A)
| p38(f15(A)) ),
inference(clausify,[status(thm)],[p38_15]) ).
fof(p38_19,axiom,
! [VAR_0,VAR_1] :
( ~ p10(VAR_1,VAR_0)
| ~ p38(VAR_1)
| p38(VAR_0) ),
file('theBenchmark.p',p38_19) ).
cnf(c_19,plain,
( ~ p10(B,A)
| ~ p38(B)
| p38(A) ),
inference(clausify,[status(thm)],[p38_19]) ).
fof(p16_32,axiom,
! [VAR_0,VAR_1] :
( ~ p10(VAR_0,VAR_1)
| p16(f19(VAR_0),f19(VAR_1)) ),
file('theBenchmark.p',p16_32) ).
cnf(c_32,plain,
( ~ p10(A,B)
| p16(f19(A),f19(B)) ),
inference(clausify,[status(thm)],[p16_32]) ).
fof(p16_36,axiom,
! [VAR_0] :
( ~ p38(VAR_0)
| p16(f19(f15(VAR_0)),f28(f19(VAR_0))) ),
file('theBenchmark.p',p16_36) ).
cnf(c_36,plain,
( ~ p38(A)
| p16(f19(f15(A)),f28(f19(A))) ),
inference(clausify,[status(thm)],[p16_36]) ).
fof(p10_37,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ p10(VAR_2,VAR_1)
| ~ p10(VAR_2,VAR_0)
| p10(VAR_0,VAR_1) ),
file('theBenchmark.p',p10_37) ).
cnf(c_37,plain,
( ~ p10(C,B)
| ~ p10(C,A)
| p10(A,B) ),
inference(clausify,[status(thm)],[p10_37]) ).
fof(p39_52,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p16(VAR_3,VAR_0)
| ~ p39(VAR_3,VAR_2)
| ~ p16(VAR_2,VAR_1)
| p39(VAR_0,VAR_1) ),
file('theBenchmark.p',p39_52) ).
cnf(c_52,plain,
( ~ p16(D,A)
| ~ p39(D,C)
| ~ p16(C,B)
| p39(A,B) ),
inference(clausify,[status(thm)],[p39_52]) ).
fof(p39_54,axiom,
! [VAR_0,VAR_1] :
( ~ p37(VAR_0,VAR_1)
| ~ p38(VAR_0)
| ~ p38(VAR_1)
| p39(f19(VAR_0),f19(VAR_1)) ),
file('theBenchmark.p',p39_54) ).
cnf(c_54,plain,
( ~ p37(A,B)
| ~ p38(A)
| ~ p38(B)
| p39(f19(A),f19(B)) ),
inference(clausify,[status(thm)],[p39_54]) ).
fof(f11_is_p38_64,axiom,
p38(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44))))),
file('theBenchmark.p',f11_is_p38_64) ).
cnf(c_64,plain,
p38(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44))))),
inference(clausify,[status(thm)],[f11_is_p38_64]) ).
fof(p10_66,axiom,
p10(c48,f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44))))),
file('theBenchmark.p',p10_66) ).
cnf(c_66,plain,
p10(c48,f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44))))),
inference(clausify,[status(thm)],[p10_66]) ).
fof(not_p39_69,axiom,
~ p39(f28(f19(c56)),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))),
file('theBenchmark.p',not_p39_69) ).
cnf(c_69,plain,
~ p39(f28(f19(c56)),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))),
inference(clausify,[status(thm)],[not_p39_69]) ).
cnf(c_84,plain,
p38(f15(c56)),
inference(resolve,[status(thm)],[c_15,c_1]) ).
cnf(c_86,plain,
p16(f19(f15(c56)),f28(f19(c56))),
inference(resolve,[status(thm)],[c_36,c_1]) ).
cnf(c_807,plain,
( ~ p10(c48,A)
| p10(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))),A) ),
inference(resolve,[status(thm)],[c_37,c_66]) ).
cnf(c_94,plain,
p10(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))),c48),
inference(resolve,[status(thm)],[c_807,c_3]) ).
cnf(c_96,plain,
p16(f19(c48),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))),
inference(resolve,[status(thm)],[c_32,c_66]) ).
cnf(c_808,plain,
( ~ p10(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))),A)
| p38(A) ),
inference(resolve,[status(thm)],[c_19,c_64]) ).
cnf(c_771,plain,
p38(c48),
inference(resolve,[status(thm)],[c_808,c_94]) ).
cnf(c_809,plain,
( ~ p16(B,f28(f19(c56)))
| ~ p39(B,A)
| ~ p16(A,f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))) ),
inference(resolve,[status(thm)],[c_52,c_69]) ).
cnf(c_810,plain,
( ~ p16(A,f28(f19(c56)))
| ~ p39(A,f19(c48)) ),
inference(resolve,[status(thm)],[c_809,c_96]) ).
cnf(c_772,plain,
~ p39(f19(f15(c56)),f19(c48)),
inference(resolve,[status(thm)],[c_810,c_86]) ).
cnf(c_811,plain,
( ~ p37(A,c48)
| ~ p38(A)
| p39(f19(A),f19(c48)) ),
inference(resolve,[status(thm)],[c_54,c_771]) ).
cnf(c_812,plain,
( ~ p37(f15(c56),c48)
| p39(f19(f15(c56)),f19(c48)) ),
inference(resolve,[status(thm)],[c_811,c_84]) ).
cnf(c_805,plain,
p39(f19(f15(c56)),f19(c48)),
inference(resolve,[status(thm)],[c_812,c_13]) ).
cnf(c_806,plain,
$false,
inference(resolve,[status(thm)],[c_805,c_772]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN708-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/5.38 % Computer : n009.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.09/5.38 % CPULimit : 300
% 0.09/5.38 % WCLimit : 300
% 0.09/5.38 % DateTime : Sat Sep 26 18:21:20 UTC 2026
% 0.09/5.38 % CPUTime :
% 0.09/5.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/5.38 % Process 837665 was started by sandbox2 on n009,
% 0.09/5.38 % Sat Sep 26 18:21:20 2026
% 0.09/5.38 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/5.39
% 0.09/5.39 % From the command line: assign(max_seconds, 300).
% 0.14/5.55
% 0.14/5.55 % SZS status Unsatisfiable for theBenchmark
% 0.14/5.55
% 0.14/5.55 % Proof 1 at 0.10 (+ 0.05) seconds.
% 0.14/5.55 % Length of proof is 21.
% 0.14/5.55 % Level of proof is 4.
% 0.14/5.55 % Maximum clause weight is 101.000.
% 0.14/5.55 % Given clauses 130.
% 0.14/5.55
% 0.14/5.55 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------