%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN563-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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:50 AM UTC 2026
% Result : Unsatisfiable 0.82s 0.49s
% Output : CNFRefutation 0.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 14
% Syntax : Number of formulae : 59 ( 59 unt; 0 def)
% Number of atoms : 59 ( 58 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 5 con; 0-4 aty)
% Number of variables : 68 ( 2 sgn 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ifeq_axiom,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq2(VAR_0,VAR_0,VAR_1,VAR_2) = VAR_1,
file('theBenchmark.p',ifeq_axiom) ).
cnf(c_1,plain,
ifeq2(A,A,B,C) = B,
inference(clausify,[status(thm)],[ifeq_axiom]) ).
fof(ifeq_axiom_001,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq(VAR_0,VAR_0,VAR_1,VAR_2) = VAR_1,
file('theBenchmark.p',ifeq_axiom_001) ).
cnf(c_2,plain,
ifeq(A,A,B,C) = B,
inference(clausify,[status(thm)],[ifeq_axiom_001]) ).
fof(p2_1,axiom,
! [VAR_0] : p2(VAR_0,VAR_0) = true,
file('theBenchmark.p',p2_1) ).
cnf(c_3,plain,
p2(A,A) = true,
inference(clausify,[status(thm)],[p2_1]) ).
fof(p6_2,axiom,
! [VAR_0] : p6(VAR_0,VAR_0) = true,
file('theBenchmark.p',p6_2) ).
cnf(c_4,plain,
p6(A,A) = true,
inference(clausify,[status(thm)],[p6_2]) ).
fof(p2_4,axiom,
p2(f4(c7),f4(c8)) = true,
file('theBenchmark.p',p2_4) ).
cnf(c_5,plain,
p2(f4(c7),f4(c8)) = true,
inference(clausify,[status(thm)],[p2_4]) ).
fof(p5_7,axiom,
! [VAR_0] : p5(f3(f3(VAR_0)),f3(f4(VAR_0))) = true,
file('theBenchmark.p',p5_7) ).
cnf(c_7,plain,
p5(f3(f3(A)),f3(f4(A))) = true,
inference(clausify,[status(thm)],[p5_7]) ).
fof(p6_9,axiom,
! [VAR_0] : ifeq2(p6(c7,VAR_0),true,p6(c7,f3(VAR_0)),true) = true,
file('theBenchmark.p',p6_9) ).
cnf(c_9,plain,
ifeq2(p6(c7,A),true,p6(c7,f3(A)),true) = true,
inference(clausify,[status(thm)],[p6_9]) ).
fof(p6_10,axiom,
! [VAR_0,VAR_1] : ifeq2(p5(VAR_0,VAR_1),true,p6(f4(VAR_0),VAR_1),true) = true,
file('theBenchmark.p',p6_10) ).
cnf(c_10,plain,
ifeq2(p5(A,B),true,p6(f4(A),B),true) = true,
inference(clausify,[status(thm)],[p6_10]) ).
fof(p2_11,axiom,
! [VAR_0,VAR_1] : ifeq2(p2(VAR_0,VAR_1),true,p2(f3(VAR_0),f3(VAR_1)),true) = true,
file('theBenchmark.p',p2_11) ).
cnf(c_11,plain,
ifeq2(p2(A,B),true,p2(f3(A),f3(B)),true) = true,
inference(clausify,[status(thm)],[p2_11]) ).
fof(p2_13,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq2(p2(VAR_0,VAR_1),true,ifeq2(p2(VAR_0,VAR_2),true,p2(VAR_2,VAR_1),true),true) = true,
file('theBenchmark.p',p2_13) ).
cnf(c_13,plain,
ifeq2(p2(A,B),true,ifeq2(p2(A,C),true,p2(C,B),true),true) = true,
inference(clausify,[status(thm)],[p2_13]) ).
fof(p5_15,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq2(p6(VAR_0,VAR_1),true,ifeq2(p5(VAR_1,VAR_2),true,p5(VAR_0,VAR_2),true),true) = true,
file('theBenchmark.p',p5_15) ).
cnf(c_15,plain,
ifeq2(p6(A,B),true,ifeq2(p5(B,C),true,p5(A,C),true),true) = true,
inference(clausify,[status(thm)],[p5_15]) ).
fof(p6_16,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : ifeq2(p2(VAR_0,VAR_1),true,ifeq2(p2(VAR_2,VAR_3),true,ifeq2(p6(VAR_2,VAR_0),true,p6(VAR_3,VAR_1),true),true),true) = true,
file('theBenchmark.p',p6_16) ).
cnf(c_16,plain,
ifeq2(p2(A,B),true,ifeq2(p2(C,D),true,ifeq2(p6(C,A),true,p6(D,B),true),true),true) = true,
inference(clausify,[status(thm)],[p6_16]) ).
fof(not_p6_5,axiom,
ifeq(p6(f4(c7),f3(f4(c8))),true,a,b) = b,
file('theBenchmark.p',not_p6_5) ).
cnf(c_19,plain,
ifeq(p6(f4(c7),f3(f4(c8))),true,a,b) = b,
inference(clausify,[status(thm)],[not_p6_5]) ).
fof(goal,axiom,
a != b,
file('theBenchmark.p',goal) ).
cnf(c_20,plain,
a != b,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_1205,plain,
ifeq2(true,true,p6(c7,f3(c7)),true) = true,
inference(paramod,[status(thm)],[c_4,c_9]) ).
cnf(c_25,plain,
p6(c7,f3(c7)) = true,
inference(paramod,[status(thm)],[c_1,c_1205]) ).
cnf(c_1206,plain,
ifeq2(true,true,p2(f3(f4(c7)),f3(f4(c8))),true) = true,
inference(paramod,[status(thm)],[c_5,c_11]) ).
cnf(c_27,plain,
p2(f3(f4(c7)),f3(f4(c8))) = true,
inference(paramod,[status(thm)],[c_1,c_1206]) ).
cnf(c_1207,plain,
ifeq2(true,true,ifeq2(p2(A,B),true,p2(B,A),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_13]) ).
cnf(c_30,plain,
ifeq2(p2(A,B),true,p2(B,A),true) = true,
inference(paramod,[status(thm)],[c_1,c_1207]) ).
cnf(c_1208,plain,
ifeq2(p6(A,f3(f3(B))),true,ifeq2(true,true,p5(A,f3(f4(B))),true),true) = true,
inference(paramod,[status(thm)],[c_7,c_15]) ).
cnf(c_42,plain,
ifeq2(p6(A,f3(f3(B))),true,p5(A,f3(f4(B))),true) = true,
inference(paramod,[status(thm)],[c_1,c_1208]) ).
cnf(c_1209,plain,
ifeq2(true,true,ifeq2(p2(A,B),true,ifeq2(p6(A,C),true,p6(B,C),true),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_16]) ).
cnf(c_43,plain,
ifeq2(p2(A,B),true,ifeq2(p6(A,C),true,p6(B,C),true),true) = true,
inference(paramod,[status(thm)],[c_1,c_1209]) ).
cnf(c_1210,plain,
ifeq2(true,true,p6(c7,f3(f3(c7))),true) = true,
inference(paramod,[status(thm)],[c_25,c_9]) ).
cnf(c_61,plain,
p6(c7,f3(f3(c7))) = true,
inference(paramod,[status(thm)],[c_1,c_1210]) ).
cnf(c_1211,plain,
ifeq2(true,true,p2(f4(c8),f4(c7)),true) = true,
inference(paramod,[status(thm)],[c_5,c_30]) ).
cnf(c_89,plain,
p2(f4(c8),f4(c7)) = true,
inference(paramod,[status(thm)],[c_1,c_1211]) ).
cnf(c_1212,plain,
ifeq2(p2(A,B),true,ifeq2(true,true,ifeq2(p6(f4(c8),A),true,p6(f4(c7),B),true),true),true) = true,
inference(paramod,[status(thm)],[c_89,c_16]) ).
cnf(c_97,plain,
ifeq2(p2(A,B),true,ifeq2(p6(f4(c8),A),true,p6(f4(c7),B),true),true) = true,
inference(paramod,[status(thm)],[c_1,c_1212]) ).
cnf(c_1213,plain,
ifeq2(true,true,p5(c7,f3(f4(c7))),true) = true,
inference(paramod,[status(thm)],[c_61,c_42]) ).
cnf(c_188,plain,
p5(c7,f3(f4(c7))) = true,
inference(paramod,[status(thm)],[c_1,c_1213]) ).
cnf(c_1214,plain,
ifeq2(true,true,ifeq2(p6(f4(c7),A),true,p6(f4(c8),A),true),true) = true,
inference(paramod,[status(thm)],[c_5,c_43]) ).
cnf(c_191,plain,
ifeq2(p6(f4(c7),A),true,p6(f4(c8),A),true) = true,
inference(paramod,[status(thm)],[c_1,c_1214]) ).
cnf(c_1215,plain,
ifeq2(true,true,p6(f4(c7),f3(f4(c7))),true) = true,
inference(paramod,[status(thm)],[c_188,c_10]) ).
cnf(c_213,plain,
p6(f4(c7),f3(f4(c7))) = true,
inference(paramod,[status(thm)],[c_1,c_1215]) ).
cnf(c_1216,plain,
ifeq2(true,true,ifeq2(p6(f4(c8),f3(f4(c7))),true,p6(f4(c7),f3(f4(c8))),true),true) = true,
inference(paramod,[status(thm)],[c_27,c_97]) ).
cnf(c_1141,plain,
ifeq2(p6(f4(c8),f3(f4(c7))),true,p6(f4(c7),f3(f4(c8))),true) = true,
inference(paramod,[status(thm)],[c_1,c_1216]) ).
cnf(c_1217,plain,
ifeq2(true,true,p6(f4(c8),f3(f4(c7))),true) = true,
inference(paramod,[status(thm)],[c_213,c_191]) ).
cnf(c_1201,plain,
p6(f4(c8),f3(f4(c7))) = true,
inference(paramod,[status(thm)],[c_1,c_1217]) ).
cnf(c_1218,plain,
ifeq2(true,true,p6(f4(c7),f3(f4(c8))),true) = true,
inference(paramod,[status(thm)],[c_1201,c_1141]) ).
cnf(c_1202,plain,
p6(f4(c7),f3(f4(c8))) = true,
inference(paramod,[status(thm)],[c_1,c_1218]) ).
cnf(c_1219,plain,
ifeq(true,true,a,b) = b,
inference(paramod,[status(thm)],[c_1202,c_19]) ).
cnf(c_1203,plain,
a = b,
inference(paramod,[status(thm)],[c_2,c_1219]) ).
cnf(c_1204,plain,
$false,
inference(resolve,[status(thm)],[c_1203,c_20]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN563-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n011.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 18:14:00 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 1239179 was started by sandbox on n011,
% 0.10/0.37 % Sat Sep 26 18:14:00 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.37
% 0.10/0.37 % From the command line: assign(max_seconds, 300).
% 0.82/0.49
% 0.82/0.49 % SZS status Unsatisfiable for theBenchmark
% 0.82/0.49
% 0.82/0.49 % Proof 1 at 0.10 (+ 0.02) seconds.
% 0.82/0.49 % Length of proof is 30.
% 0.82/0.49 % Level of proof is 8.
% 0.82/0.49 % Maximum clause weight is 33.000.
% 0.82/0.49 % Given clauses 219.
% 0.82/0.49
% 0.82/0.49 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------