%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN673-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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:05 AM UTC 2026
% Result : Unsatisfiable 0.13s 0.48s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 14
% Syntax : Number of formulae : 44 ( 18 unt; 0 def)
% Number of atoms : 84 ( 0 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 80 ( 40 ~; 40 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 13 con; 0-2 aty)
% Number of variables : 47 ( 0 sgn 20 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(p10_1,axiom,
! [VAR_0] : p10(VAR_0,VAR_0),
file('theBenchmark.p',p10_1) ).
cnf(c_1,plain,
p10(A,A),
inference(clausify,[status(thm)],[p10_1]) ).
fof(p4_5,axiom,
! [VAR_0] : p4(VAR_0,VAR_0),
file('theBenchmark.p',p4_5) ).
cnf(c_5,plain,
p4(A,A),
inference(clausify,[status(thm)],[p4_5]) ).
fof(p16_12,axiom,
! [VAR_0] : p16(VAR_0,VAR_0),
file('theBenchmark.p',p16_12) ).
cnf(c_12,plain,
p16(A,A),
inference(clausify,[status(thm)],[p16_12]) ).
fof(not_p29_17,axiom,
~ p29(f5(c33,f8(c34,c30)),c38),
file('theBenchmark.p',not_p29_17) ).
cnf(c_17,plain,
~ p29(f5(c33,f8(c34,c30)),c38),
inference(clausify,[status(thm)],[not_p29_17]) ).
fof(p29_18,axiom,
! [VAR_0,VAR_1] :
( ~ p27(f12(c32,VAR_1),VAR_0)
| p29(VAR_0,VAR_1) ),
file('theBenchmark.p',p29_18) ).
cnf(c_18,plain,
( ~ p27(f12(c32,B),A)
| p29(A,B) ),
inference(clausify,[status(thm)],[p29_18]) ).
fof(p27_19,axiom,
! [VAR_0,VAR_1] :
( ~ p29(VAR_1,VAR_0)
| p27(f12(c32,VAR_0),VAR_1) ),
file('theBenchmark.p',p27_19) ).
cnf(c_19,plain,
( ~ p29(B,A)
| p27(f12(c32,A),B) ),
inference(clausify,[status(thm)],[p27_19]) ).
fof(p28_20,axiom,
! [VAR_0] :
( ~ p16(VAR_0,c40)
| p28(f21(c30,VAR_0),c31) ),
file('theBenchmark.p',p28_20) ).
cnf(c_20,plain,
( ~ p16(A,c40)
| p28(f21(c30,A),c31) ),
inference(clausify,[status(thm)],[p28_20]) ).
fof(p10_22,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_22) ).
cnf(c_22,plain,
( ~ p10(C,B)
| ~ p10(C,A)
| p10(A,B) ),
inference(clausify,[status(thm)],[p10_22]) ).
fof(p28_37,axiom,
! [VAR_0] :
( ~ p29(f24(c42,VAR_0),c39)
| p28(f21(c30,VAR_0),c31) ),
file('theBenchmark.p',p28_37) ).
cnf(c_37,plain,
( ~ p29(f24(c42,A),c39)
| p28(f21(c30,A),c31) ),
inference(clausify,[status(thm)],[p28_37]) ).
fof(p29_38,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p10(VAR_3,VAR_1)
| ~ p4(VAR_2,VAR_0)
| ~ p29(VAR_2,VAR_3)
| p29(VAR_0,VAR_1) ),
file('theBenchmark.p',p29_38) ).
cnf(c_38,plain,
( ~ p10(D,B)
| ~ p4(C,A)
| ~ p29(C,D)
| p29(A,B) ),
inference(clausify,[status(thm)],[p29_38]) ).
fof(p10_41,axiom,
p10(c38,f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40))),
file('theBenchmark.p',p10_41) ).
cnf(c_41,plain,
p10(c38,f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40))),
inference(clausify,[status(thm)],[p10_41]) ).
fof(p29_52,axiom,
! [VAR_0] :
( ~ p10(VAR_0,f14(f19(c35,c37),c39))
| p29(f5(c33,f8(c34,c30)),VAR_0)
| p29(f24(c42,f26(c43,VAR_0)),c39) ),
file('theBenchmark.p',p29_52) ).
cnf(c_52,plain,
( ~ p10(A,f14(f19(c35,c37),c39))
| p29(f5(c33,f8(c34,c30)),A)
| p29(f24(c42,f26(c43,A)),c39) ),
inference(clausify,[status(thm)],[p29_52]) ).
fof(p29_53,axiom,
! [VAR_0] :
( ~ p28(f21(c30,f26(c43,VAR_0)),c31)
| ~ p10(VAR_0,f14(f19(c35,c37),c39))
| p29(f5(c33,f8(c34,c30)),VAR_0) ),
file('theBenchmark.p',p29_53) ).
cnf(c_53,plain,
( ~ p28(f21(c30,f26(c43,A)),c31)
| ~ p10(A,f14(f19(c35,c37),c39))
| p29(f5(c33,f8(c34,c30)),A) ),
inference(clausify,[status(thm)],[p29_53]) ).
fof(p27_55,axiom,
! [VAR_0,VAR_1] :
( ~ p27(f12(c32,VAR_0),f5(c33,f8(c34,c30)))
| ~ p28(f21(c30,VAR_1),c31)
| p27(f12(c32,f14(f19(c35,VAR_0),f17(c36,VAR_1))),f5(c33,f8(c34,c30))) ),
file('theBenchmark.p',p27_55) ).
cnf(c_55,plain,
( ~ p27(f12(c32,A),f5(c33,f8(c34,c30)))
| ~ p28(f21(c30,B),c31)
| p27(f12(c32,f14(f19(c35,A),f17(c36,B))),f5(c33,f8(c34,c30))) ),
inference(clausify,[status(thm)],[p27_55]) ).
cnf(c_57,plain,
p28(f21(c30,c40),c31),
inference(resolve,[status(thm)],[c_20,c_12]) ).
cnf(c_61,plain,
( ~ p10(B,A)
| p10(A,B) ),
inference(resolve,[status(thm)],[c_22,c_1]) ).
cnf(c_76,plain,
( ~ p10(C,B)
| ~ p29(A,C)
| p29(A,B) ),
inference(resolve,[status(thm)],[c_38,c_5]) ).
cnf(c_92,plain,
( p29(f5(c33,f8(c34,c30)),f14(f19(c35,c37),c39))
| p29(f24(c42,f26(c43,f14(f19(c35,c37),c39))),c39) ),
inference(resolve,[status(thm)],[c_52,c_1]) ).
cnf(c_94,plain,
( ~ p27(f12(c32,A),f5(c33,f8(c34,c30)))
| p27(f12(c32,f14(f19(c35,A),f17(c36,c40))),f5(c33,f8(c34,c30))) ),
inference(resolve,[status(thm)],[c_57,c_55]) ).
cnf(c_101,plain,
p10(f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40)),c38),
inference(resolve,[status(thm)],[c_61,c_41]) ).
cnf(c_154,plain,
( p28(f21(c30,f26(c43,f14(f19(c35,c37),c39))),c31)
| p29(f5(c33,f8(c34,c30)),f14(f19(c35,c37),c39)) ),
inference(resolve,[status(thm)],[c_92,c_37]) ).
cnf(c_664,plain,
( ~ p10(A,c38)
| ~ p29(f5(c33,f8(c34,c30)),A) ),
inference(resolve,[status(thm)],[c_76,c_17]) ).
cnf(c_209,plain,
~ p29(f5(c33,f8(c34,c30)),f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40))),
inference(resolve,[status(thm)],[c_664,c_101]) ).
cnf(c_595,plain,
~ p27(f12(c32,f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40))),f5(c33,f8(c34,c30))),
inference(resolve,[status(thm)],[c_18,c_209]) ).
cnf(c_665,plain,
( ~ p10(f14(f19(c35,c37),c39),f14(f19(c35,c37),c39))
| p29(f5(c33,f8(c34,c30)),f14(f19(c35,c37),c39))
| p29(f5(c33,f8(c34,c30)),f14(f19(c35,c37),c39)) ),
inference(resolve,[status(thm)],[c_154,c_53]) ).
cnf(c_666,plain,
( ~ p10(f14(f19(c35,c37),c39),f14(f19(c35,c37),c39))
| p29(f5(c33,f8(c34,c30)),f14(f19(c35,c37),c39)) ),
inference(copy,[status(thm)],[c_665]) ).
cnf(c_641,plain,
p29(f5(c33,f8(c34,c30)),f14(f19(c35,c37),c39)),
inference(resolve,[status(thm)],[c_1,c_666]) ).
cnf(c_653,plain,
p27(f12(c32,f14(f19(c35,c37),c39)),f5(c33,f8(c34,c30))),
inference(resolve,[status(thm)],[c_641,c_19]) ).
cnf(c_667,plain,
p27(f12(c32,f14(f19(c35,f14(f19(c35,c37),c39)),f17(c36,c40))),f5(c33,f8(c34,c30))),
inference(resolve,[status(thm)],[c_653,c_94]) ).
cnf(c_663,plain,
$false,
inference(resolve,[status(thm)],[c_595,c_667]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN673-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n016.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 18:24:30 UTC 2026
% 0.13/0.36 % CPUTime :
% 0.13/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.13/0.36 % Process 1460289 was started by sandbox on n016,
% 0.13/0.36 % Sat Sep 26 18:24:30 2026
% 0.13/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.13/0.37
% 0.13/0.37 % From the command line: assign(max_seconds, 300).
% 0.13/0.48
% 0.13/0.48 % SZS status Unsatisfiable for theBenchmark
% 0.13/0.48
% 0.13/0.48 % Proof 1 at 0.04 (+ 0.02) seconds.
% 0.13/0.48 % Length of proof is 26.
% 0.13/0.48 % Level of proof is 5.
% 0.13/0.48 % Maximum clause weight is 49.000.
% 0.13/0.48 % Given clauses 256.
% 0.13/0.48
% 0.13/0.48 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------