%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN604-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 : n020.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:38:56 AM UTC 2026
% Result : Unsatisfiable 1.89s 0.71s
% Output : CNFRefutation 1.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 11
% Syntax : Number of formulae : 47 ( 24 unt; 0 def)
% Number of atoms : 81 ( 0 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 70 ( 36 ~; 34 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 5 con; 0-2 aty)
% Number of variables : 69 ( 4 sgn 19 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(p3_4,axiom,
! [VAR_0] : p3(VAR_0,VAR_0),
file('theBenchmark.p',p3_4) ).
cnf(c_4,plain,
p3(A,A),
inference(clausify,[status(thm)],[p3_4]) ).
fof(p3_7,axiom,
! [VAR_0] : p3(f4(f8(VAR_0)),f12(VAR_0)),
file('theBenchmark.p',p3_7) ).
cnf(c_7,plain,
p3(f4(f8(A)),f12(A)),
inference(clausify,[status(thm)],[p3_7]) ).
fof(p3_8,axiom,
! [VAR_0] : p3(f12(f10(VAR_0)),f10(VAR_0)),
file('theBenchmark.p',p3_8) ).
cnf(c_8,plain,
p3(f12(f10(A)),f10(A)),
inference(clausify,[status(thm)],[p3_8]) ).
fof(p16_9,axiom,
! [VAR_0] : p16(f10(f11(c21)),f12(VAR_0)),
file('theBenchmark.p',p16_9) ).
cnf(c_9,plain,
p16(f10(f11(c21)),f12(A)),
inference(clausify,[status(thm)],[p16_9]) ).
fof(p16_10,axiom,
! [VAR_0,VAR_1] :
( p16(VAR_1,f12(VAR_0))
| p16(VAR_0,VAR_1) ),
file('theBenchmark.p',p16_10) ).
cnf(c_10,plain,
( p16(B,f12(A))
| p16(A,B) ),
inference(clausify,[status(thm)],[p16_10]) ).
fof(p3_21,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ p3(VAR_2,VAR_1)
| ~ p3(VAR_2,VAR_0)
| p3(VAR_0,VAR_1) ),
file('theBenchmark.p',p3_21) ).
cnf(c_21,plain,
( ~ p3(C,B)
| ~ p3(C,A)
| p3(A,B) ),
inference(clausify,[status(thm)],[p3_21]) ).
fof(p16_23,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ p16(VAR_2,VAR_1)
| ~ p16(VAR_0,VAR_2)
| p16(VAR_0,VAR_1) ),
file('theBenchmark.p',p16_23) ).
cnf(c_23,plain,
( ~ p16(C,B)
| ~ p16(A,C)
| p16(A,B) ),
inference(clausify,[status(thm)],[p16_23]) ).
fof(p16_25,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p16(VAR_2,VAR_3)
| ~ p3(VAR_3,VAR_1)
| ~ p3(VAR_2,VAR_0)
| p16(VAR_0,VAR_1) ),
file('theBenchmark.p',p16_25) ).
cnf(c_25,plain,
( ~ p16(C,D)
| ~ p3(D,B)
| ~ p3(C,A)
| p16(A,B) ),
inference(clausify,[status(thm)],[p16_25]) ).
fof(not_p16_28,axiom,
! [VAR_0] : ~ p16(f4(f6(f7(c20,c18),VAR_0)),f4(f6(f7(c20,c18),f13(VAR_0)))),
file('theBenchmark.p',not_p16_28) ).
cnf(c_28,plain,
~ p16(f4(f6(f7(c20,c18),A)),f4(f6(f7(c20,c18),f13(A)))),
inference(clausify,[status(thm)],[not_p16_28]) ).
fof(p16_29,axiom,
! [VAR_0] :
( ~ p16(f4(VAR_0),f12(c19))
| p16(f4(f6(f7(c20,c18),c23)),f4(f6(f7(c20,c18),VAR_0))) ),
file('theBenchmark.p',p16_29) ).
cnf(c_29,plain,
( ~ p16(f4(A),f12(c19))
| p16(f4(f6(f7(c20,c18),c23)),f4(f6(f7(c20,c18),A))) ),
inference(clausify,[status(thm)],[p16_29]) ).
fof(p16_30,axiom,
! [VAR_0] :
( ~ p16(c19,f4(VAR_0))
| p16(f4(f6(f7(c20,c18),f8(f10(f11(c21))))),f4(f6(f7(c20,c18),VAR_0))) ),
file('theBenchmark.p',p16_30) ).
cnf(c_30,plain,
( ~ p16(c19,f4(A))
| p16(f4(f6(f7(c20,c18),f8(f10(f11(c21))))),f4(f6(f7(c20,c18),A))) ),
inference(clausify,[status(thm)],[p16_30]) ).
cnf(c_31,plain,
( ~ p16(B,B)
| ~ p3(B,A)
| p16(A,A) ),
inference(factor,[status(thm)],[c_25]) ).
cnf(c_43,plain,
( ~ p3(B,A)
| p3(A,B) ),
inference(resolve,[status(thm)],[c_21,c_4]) ).
cnf(c_51,plain,
( ~ p16(A,f10(f11(c21)))
| p16(A,f12(B)) ),
inference(resolve,[status(thm)],[c_23,c_9]) ).
cnf(c_57,plain,
( ~ p16(A,C)
| ~ p3(C,B)
| p16(A,B) ),
inference(resolve,[status(thm)],[c_25,c_4]) ).
cnf(c_60,plain,
( ~ p16(C,B)
| ~ p3(C,A)
| p16(A,B) ),
inference(resolve,[status(thm)],[c_25,c_4]) ).
cnf(c_66,plain,
~ p16(f4(f13(c23)),f12(c19)),
inference(resolve,[status(thm)],[c_29,c_28]) ).
cnf(c_75,plain,
p16(c19,f4(f13(c23))),
inference(resolve,[status(thm)],[c_66,c_10]) ).
cnf(c_84,plain,
p16(f4(f6(f7(c20,c18),f8(f10(f11(c21))))),f4(f6(f7(c20,c18),f13(c23)))),
inference(resolve,[status(thm)],[c_75,c_30]) ).
cnf(c_99,plain,
p3(f10(A),f12(f10(A))),
inference(resolve,[status(thm)],[c_43,c_8]) ).
cnf(c_100,plain,
p3(f12(A),f4(f8(A))),
inference(resolve,[status(thm)],[c_43,c_7]) ).
cnf(c_103,plain,
( ~ p16(f10(A),f10(A))
| p16(f12(f10(A)),f12(f10(A))) ),
inference(resolve,[status(thm)],[c_99,c_31]) ).
cnf(c_244,plain,
( ~ p16(A,f10(B))
| p16(A,f12(f10(B))) ),
inference(resolve,[status(thm)],[c_57,c_99]) ).
cnf(c_247,plain,
( ~ p16(A,f12(f10(B)))
| p16(A,f10(B)) ),
inference(resolve,[status(thm)],[c_57,c_8]) ).
cnf(c_265,plain,
( ~ p16(f12(A),B)
| p16(f4(f8(A)),B) ),
inference(resolve,[status(thm)],[c_60,c_100]) ).
cnf(c_663,plain,
( p16(f10(B),f12(A))
| p16(A,f12(f10(B))) ),
inference(resolve,[status(thm)],[c_244,c_10]) ).
cnf(c_664,plain,
p16(f10(A),f12(f10(A))),
inference(factor,[status(thm)],[c_663]) ).
cnf(c_682,plain,
p16(f10(A),f10(A)),
inference(resolve,[status(thm)],[c_247,c_664]) ).
cnf(c_694,plain,
p16(f12(f10(A)),f12(f10(A))),
inference(resolve,[status(thm)],[c_682,c_103]) ).
cnf(c_709,plain,
p16(f12(f10(A)),f10(A)),
inference(resolve,[status(thm)],[c_694,c_247]) ).
cnf(c_711,plain,
p16(f12(f10(f11(c21))),f12(A)),
inference(resolve,[status(thm)],[c_709,c_51]) ).
cnf(c_764,plain,
p16(f4(f8(f10(f11(c21)))),f12(A)),
inference(resolve,[status(thm)],[c_265,c_711]) ).
cnf(c_778,plain,
p16(f4(f6(f7(c20,c18),c23)),f4(f6(f7(c20,c18),f8(f10(f11(c21)))))),
inference(resolve,[status(thm)],[c_764,c_29]) ).
cnf(c_1112,plain,
( ~ p16(B,f4(f6(f7(c20,c18),f13(A))))
| ~ p16(f4(f6(f7(c20,c18),A)),B) ),
inference(resolve,[status(thm)],[c_23,c_28]) ).
cnf(c_1113,plain,
~ p16(f4(f6(f7(c20,c18),c23)),f4(f6(f7(c20,c18),f8(f10(f11(c21)))))),
inference(resolve,[status(thm)],[c_1112,c_84]) ).
cnf(c_1111,plain,
$false,
inference(resolve,[status(thm)],[c_778,c_1113]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SYN604-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.05 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.43 % Computer : n020.cluster.edu
% 0.15/0.43 % Model : x86_64 x86_64
% 0.15/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.43 % Memory : 8046.5625MB
% 0.15/0.43 % OS : Linux 6.8.0-71-generic
% 0.15/0.43 % CPULimit : 300
% 0.15/0.43 % WCLimit : 300
% 0.15/0.43 % DateTime : Sat Sep 26 18:16:34 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.43 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.15/0.43 % Process 2219164 was started by sandbox2 on n020,
% 0.15/0.43 % Sat Sep 26 18:16:34 2026
% 0.15/0.43 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.15/0.44
% 0.15/0.44 % From the command line: assign(max_seconds, 300).
% 1.89/0.71
% 1.89/0.71 % SZS status Unsatisfiable for theBenchmark
% 1.89/0.71
% 1.89/0.71 % Proof 1 at 0.18 (+ 0.08) seconds.
% 1.89/0.71 % Length of proof is 34.
% 1.89/0.71 % Level of proof is 12.
% 1.89/0.71 % Maximum clause weight is 20.000.
% 1.89/0.71 % Given clauses 266.
% 1.89/0.71
% 1.89/0.71 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------