%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SYN708-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 : n014.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 7.53s 1.56s
% Output : CNFRefutation 7.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 16
% Syntax : Number of formulae : 61 ( 61 unt; 0 def)
% Number of atoms : 61 ( 60 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 : 16 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 6 con; 0-4 aty)
% Number of variables : 52 ( 2 sgn 22 !; 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(c56_is_p38_1,axiom,
p38(c56) = true,
file('theBenchmark.p',c56_is_p38_1) ).
cnf(c_3,plain,
p38(c56) = true,
inference(clausify,[status(thm)],[c56_is_p38_1]) ).
fof(p10_3,axiom,
! [VAR_0] : p10(VAR_0,VAR_0) = true,
file('theBenchmark.p',p10_3) ).
cnf(c_4,plain,
p10(A,A) = true,
inference(clausify,[status(thm)],[p10_3]) ).
fof(p37_13,axiom,
p37(f15(c56),c48) = true,
file('theBenchmark.p',p37_13) ).
cnf(c_12,plain,
p37(f15(c56),c48) = true,
inference(clausify,[status(thm)],[p37_13]) ).
fof(p38_15,axiom,
! [VAR_0] : ifeq2(p38(VAR_0),true,p38(f15(VAR_0)),true) = true,
file('theBenchmark.p',p38_15) ).
cnf(c_13,plain,
ifeq2(p38(A),true,p38(f15(A)),true) = true,
inference(clausify,[status(thm)],[p38_15]) ).
fof(p38_19,axiom,
! [VAR_0,VAR_1] : ifeq2(p10(VAR_0,VAR_1),true,ifeq2(p38(VAR_0),true,p38(VAR_1),true),true) = true,
file('theBenchmark.p',p38_19) ).
cnf(c_17,plain,
ifeq2(p10(A,B),true,ifeq2(p38(A),true,p38(B),true),true) = true,
inference(clausify,[status(thm)],[p38_19]) ).
fof(p16_32,axiom,
! [VAR_0,VAR_1] : ifeq2(p10(VAR_0,VAR_1),true,p16(f19(VAR_0),f19(VAR_1)),true) = true,
file('theBenchmark.p',p16_32) ).
cnf(c_30,plain,
ifeq2(p10(A,B),true,p16(f19(A),f19(B)),true) = true,
inference(clausify,[status(thm)],[p16_32]) ).
fof(p16_36,axiom,
! [VAR_0] : ifeq2(p38(VAR_0),true,p16(f19(f15(VAR_0)),f28(f19(VAR_0))),true) = true,
file('theBenchmark.p',p16_36) ).
cnf(c_34,plain,
ifeq2(p38(A),true,p16(f19(f15(A)),f28(f19(A))),true) = true,
inference(clausify,[status(thm)],[p16_36]) ).
fof(p10_37,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq2(p10(VAR_0,VAR_1),true,ifeq2(p10(VAR_0,VAR_2),true,p10(VAR_2,VAR_1),true),true) = true,
file('theBenchmark.p',p10_37) ).
cnf(c_35,plain,
ifeq2(p10(A,B),true,ifeq2(p10(A,C),true,p10(C,B),true),true) = true,
inference(clausify,[status(thm)],[p10_37]) ).
fof(p39_52,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : ifeq2(p39(VAR_0,VAR_1),true,ifeq2(p16(VAR_0,VAR_2),true,ifeq2(p16(VAR_1,VAR_3),true,p39(VAR_2,VAR_3),true),true),true) = true,
file('theBenchmark.p',p39_52) ).
cnf(c_50,plain,
ifeq2(p39(A,B),true,ifeq2(p16(A,C),true,ifeq2(p16(B,D),true,p39(C,D),true),true),true) = true,
inference(clausify,[status(thm)],[p39_52]) ).
fof(p39_54,axiom,
! [VAR_0,VAR_1] : ifeq2(p37(VAR_0,VAR_1),true,ifeq2(p38(VAR_1),true,ifeq2(p38(VAR_0),true,p39(f19(VAR_0),f19(VAR_1)),true),true),true) = true,
file('theBenchmark.p',p39_54) ).
cnf(c_52,plain,
ifeq2(p37(A,B),true,ifeq2(p38(B),true,ifeq2(p38(A),true,p39(f19(A),f19(B)),true),true),true) = true,
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))))) = true,
file('theBenchmark.p',f11_is_p38_64) ).
cnf(c_62,plain,
p38(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44))))) = true,
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))))) = true,
file('theBenchmark.p',p10_66) ).
cnf(c_64,plain,
p10(c48,f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44))))) = true,
inference(clausify,[status(thm)],[p10_66]) ).
fof(not_p39_69,axiom,
ifeq(p39(f28(f19(c56)),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))),true,a,b) = b,
file('theBenchmark.p',not_p39_69) ).
cnf(c_85,plain,
ifeq(p39(f28(f19(c56)),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))),true,a,b) = b,
inference(clausify,[status(thm)],[not_p39_69]) ).
fof(goal,axiom,
a != b,
file('theBenchmark.p',goal) ).
cnf(c_86,plain,
a != b,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_3546,plain,
ifeq2(true,true,p38(f15(c56)),true) = true,
inference(paramod,[status(thm)],[c_3,c_13]) ).
cnf(c_87,plain,
p38(f15(c56)) = true,
inference(paramod,[status(thm)],[c_1,c_3546]) ).
cnf(c_3547,plain,
ifeq2(true,true,p16(f19(f15(c56)),f28(f19(c56))),true) = true,
inference(paramod,[status(thm)],[c_3,c_34]) ).
cnf(c_94,plain,
p16(f19(f15(c56)),f28(f19(c56))) = true,
inference(paramod,[status(thm)],[c_1,c_3547]) ).
cnf(c_3548,plain,
ifeq2(true,true,ifeq2(p10(A,B),true,p10(B,A),true),true) = true,
inference(paramod,[status(thm)],[c_4,c_35]) ).
cnf(c_95,plain,
ifeq2(p10(A,B),true,p10(B,A),true) = true,
inference(paramod,[status(thm)],[c_1,c_3548]) ).
cnf(c_3549,plain,
ifeq2(true,true,ifeq2(p38(c48),true,ifeq2(p38(f15(c56)),true,p39(f19(f15(c56)),f19(c48)),true),true),true) = true,
inference(paramod,[status(thm)],[c_12,c_52]) ).
cnf(c_3550,plain,
ifeq2(true,true,ifeq2(p38(c48),true,ifeq2(true,true,p39(f19(f15(c56)),f19(c48)),true),true),true) = true,
inference(paramod,[status(thm)],[c_87,c_3549]) ).
cnf(c_3551,plain,
ifeq2(true,true,ifeq2(p38(c48),true,p39(f19(f15(c56)),f19(c48)),true),true) = true,
inference(paramod,[status(thm)],[c_1,c_3550]) ).
cnf(c_154,plain,
ifeq2(p38(c48),true,p39(f19(f15(c56)),f19(c48)),true) = true,
inference(paramod,[status(thm)],[c_1,c_3551]) ).
cnf(c_3552,plain,
ifeq2(true,true,p16(f19(c48),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))),true) = true,
inference(paramod,[status(thm)],[c_64,c_30]) ).
cnf(c_179,plain,
p16(f19(c48),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))) = true,
inference(paramod,[status(thm)],[c_1,c_3552]) ).
cnf(c_3553,plain,
ifeq2(true,true,p10(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))),c48),true) = true,
inference(paramod,[status(thm)],[c_64,c_95]) ).
cnf(c_192,plain,
p10(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))),c48) = true,
inference(paramod,[status(thm)],[c_1,c_3553]) ).
cnf(c_3554,plain,
ifeq2(p39(f19(f15(c56)),A),true,ifeq2(true,true,ifeq2(p16(A,B),true,p39(f28(f19(c56)),B),true),true),true) = true,
inference(paramod,[status(thm)],[c_94,c_50]) ).
cnf(c_207,plain,
ifeq2(p39(f19(f15(c56)),A),true,ifeq2(p16(A,B),true,p39(f28(f19(c56)),B),true),true) = true,
inference(paramod,[status(thm)],[c_1,c_3554]) ).
cnf(c_3555,plain,
ifeq2(true,true,ifeq2(p38(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44))))),true,p38(c48),true),true) = true,
inference(paramod,[status(thm)],[c_192,c_17]) ).
cnf(c_3556,plain,
ifeq2(true,true,ifeq2(true,true,p38(c48),true),true) = true,
inference(paramod,[status(thm)],[c_62,c_3555]) ).
cnf(c_3557,plain,
ifeq2(true,true,p38(c48),true) = true,
inference(paramod,[status(thm)],[c_1,c_3556]) ).
cnf(c_2762,plain,
p38(c48) = true,
inference(paramod,[status(thm)],[c_1,c_3557]) ).
cnf(c_3558,plain,
ifeq2(true,true,p39(f19(f15(c56)),f19(c48)),true) = true,
inference(paramod,[status(thm)],[c_2762,c_154]) ).
cnf(c_2765,plain,
p39(f19(f15(c56)),f19(c48)) = true,
inference(paramod,[status(thm)],[c_1,c_3558]) ).
cnf(c_3559,plain,
ifeq2(p39(f19(f15(c56)),f19(c48)),true,ifeq2(true,true,p39(f28(f19(c56)),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))),true),true) = true,
inference(paramod,[status(thm)],[c_179,c_207]) ).
cnf(c_3560,plain,
ifeq2(true,true,ifeq2(true,true,p39(f28(f19(c56)),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))),true),true) = true,
inference(paramod,[status(thm)],[c_2765,c_3559]) ).
cnf(c_3561,plain,
ifeq2(true,true,p39(f28(f19(c56)),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))),true) = true,
inference(paramod,[status(thm)],[c_1,c_3560]) ).
cnf(c_3502,plain,
p39(f28(f19(c56)),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))) = true,
inference(paramod,[status(thm)],[c_1,c_3561]) ).
cnf(c_3562,plain,
ifeq(true,true,a,b) = b,
inference(paramod,[status(thm)],[c_3502,c_85]) ).
cnf(c_3563,plain,
a = b,
inference(paramod,[status(thm)],[c_2,c_3562]) ).
cnf(c_3545,plain,
$false,
inference(resolve,[status(thm)],[c_86,c_3563]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN708-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.54 % Computer : n014.cluster.edu
% 0.10/0.54 % Model : x86_64 x86_64
% 0.10/0.54 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.54 % Memory : 8046.5625MB
% 0.10/0.54 % OS : Linux 6.8.0-71-generic
% 0.10/0.54 % CPULimit : 300
% 0.10/0.54 % WCLimit : 300
% 0.10/0.54 % DateTime : Sat Sep 26 18:20:47 UTC 2026
% 0.10/0.55 % CPUTime :
% 0.10/0.55 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.55 % Process 3826985 was started by sandbox on n014,
% 0.10/0.55 % Sat Sep 26 18:20:47 2026
% 0.10/0.55 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.55
% 0.10/0.55 % From the command line: assign(max_seconds, 300).
% 7.53/1.56
% 7.53/1.56 % SZS status Unsatisfiable for theBenchmark
% 7.53/1.56
% 7.53/1.56 % Proof 1 at 0.75 (+ 0.16) seconds.
% 7.53/1.56 % Length of proof is 27.
% 7.53/1.56 % Level of proof is 6.
% 7.53/1.56 % Maximum clause weight is 108.000.
% 7.53/1.56 % Given clauses 395.
% 7.53/1.56
% 7.53/1.56 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------