%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : BOO004-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/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 06:55:00 AM UTC 2026
% Result : Unsatisfiable 106.16s 16.17s
% Output : CNFRefutation 106.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 13
% Syntax : Number of formulae : 80 ( 80 unt; 0 def)
% Number of atoms : 80 ( 79 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 4 con; 0-4 aty)
% Number of variables : 193 ( 17 sgn 36 !; 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(closure_of_addition,axiom,
! [VAR_0,VAR_1] : sum(VAR_0,VAR_1,add(VAR_0,VAR_1)) = true,
file('theBenchmark.p',closure_of_addition) ).
cnf(c_3,plain,
sum(A,B,add(A,B)) = true,
inference(clausify,[status(thm)],[closure_of_addition]) ).
fof(closure_of_multiplication,axiom,
! [VAR_0,VAR_1] : product(VAR_0,VAR_1,multiply(VAR_0,VAR_1)) = true,
file('theBenchmark.p',closure_of_multiplication) ).
cnf(c_4,plain,
product(A,B,multiply(A,B)) = true,
inference(clausify,[status(thm)],[closure_of_multiplication]) ).
fof(additive_identity1,axiom,
! [VAR_0] : sum(additive_identity,VAR_0,VAR_0) = true,
file('theBenchmark.p',additive_identity1) ).
cnf(c_7,plain,
sum(additive_identity,A,A) = true,
inference(clausify,[status(thm)],[additive_identity1]) ).
fof(additive_identity2,axiom,
! [VAR_0] : sum(VAR_0,additive_identity,VAR_0) = true,
file('theBenchmark.p',additive_identity2) ).
cnf(c_8,plain,
sum(A,additive_identity,A) = true,
inference(clausify,[status(thm)],[additive_identity2]) ).
fof(multiplicative_identity2,axiom,
! [VAR_0] : product(VAR_0,multiplicative_identity,VAR_0) = true,
file('theBenchmark.p',multiplicative_identity2) ).
cnf(c_10,plain,
product(A,multiplicative_identity,A) = true,
inference(clausify,[status(thm)],[multiplicative_identity2]) ).
fof(distributivity1,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] : ifeq(product(VAR_0,VAR_1,VAR_2),true,ifeq(product(VAR_0,VAR_3,VAR_4),true,ifeq(product(VAR_0,VAR_5,VAR_6),true,ifeq(sum(VAR_5,VAR_3,VAR_1),true,sum(VAR_6,VAR_4,VAR_2),true),true),true),true) = true,
file('theBenchmark.p',distributivity1) ).
cnf(c_11,plain,
ifeq(product(A,B,C),true,ifeq(product(A,D,E),true,ifeq(product(A,F,V6),true,ifeq(sum(F,D,B),true,sum(V6,E,C),true),true),true),true) = true,
inference(clausify,[status(thm)],[distributivity1]) ).
fof(distributivity7,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] : ifeq(product(VAR_0,VAR_1,VAR_2),true,ifeq(sum(VAR_2,VAR_3,VAR_4),true,ifeq(sum(VAR_1,VAR_3,VAR_5),true,ifeq(sum(VAR_0,VAR_3,VAR_6),true,product(VAR_6,VAR_5,VAR_4),true),true),true),true) = true,
file('theBenchmark.p',distributivity7) ).
cnf(c_17,plain,
ifeq(product(A,B,C),true,ifeq(sum(C,D,E),true,ifeq(sum(B,D,F),true,ifeq(sum(A,D,V6),true,product(V6,F,E),true),true),true),true) = true,
inference(clausify,[status(thm)],[distributivity7]) ).
fof(multiplicative_inverse2,axiom,
! [VAR_0] : product(VAR_0,inverse(VAR_0),additive_identity) = true,
file('theBenchmark.p',multiplicative_inverse2) ).
cnf(c_22,plain,
product(A,inverse(A),additive_identity) = true,
inference(clausify,[status(thm)],[multiplicative_inverse2]) ).
fof(addition_is_well_defined,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : ifeq2(sum(VAR_0,VAR_1,VAR_2),true,ifeq2(sum(VAR_0,VAR_1,VAR_3),true,VAR_3,VAR_2),VAR_2) = VAR_2,
file('theBenchmark.p',addition_is_well_defined) ).
cnf(c_23,plain,
ifeq2(sum(A,B,C),true,ifeq2(sum(A,B,D),true,D,C),C) = C,
inference(clausify,[status(thm)],[addition_is_well_defined]) ).
fof(multiplication_is_well_defined,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : ifeq2(product(VAR_0,VAR_1,VAR_2),true,ifeq2(product(VAR_0,VAR_1,VAR_3),true,VAR_3,VAR_2),VAR_2) = VAR_2,
file('theBenchmark.p',multiplication_is_well_defined) ).
cnf(c_24,plain,
ifeq2(product(A,B,C),true,ifeq2(product(A,B,D),true,D,C),C) = C,
inference(clausify,[status(thm)],[multiplication_is_well_defined]) ).
fof(prove_both_equalities,axiom,
sum(x,x,x) != true,
file('theBenchmark.p',prove_both_equalities) ).
cnf(c_25,plain,
sum(x,x,x) != true,
inference(clausify,[status(thm)],[prove_both_equalities]) ).
cnf(c_11473,plain,
ifeq(true,true,ifeq(product(A,B,C),true,ifeq(product(A,D,E),true,ifeq(sum(D,B,F),true,sum(E,C,multiply(A,F)),true),true),true),true) = true,
inference(paramod,[status(thm)],[c_4,c_11]) ).
cnf(c_30,plain,
ifeq(product(A,B,C),true,ifeq(product(A,D,E),true,ifeq(sum(D,B,F),true,sum(E,C,multiply(A,F)),true),true),true) = true,
inference(paramod,[status(thm)],[c_2,c_11473]) ).
cnf(c_11474,plain,
ifeq(true,true,ifeq(product(A,B,C),true,ifeq(product(A,D,E),true,ifeq(sum(D,B,multiplicative_identity),true,sum(E,C,A),true),true),true),true) = true,
inference(paramod,[status(thm)],[c_10,c_11]) ).
cnf(c_41,plain,
ifeq(product(A,B,C),true,ifeq(product(A,D,E),true,ifeq(sum(D,B,multiplicative_identity),true,sum(E,C,A),true),true),true) = true,
inference(paramod,[status(thm)],[c_2,c_11474]) ).
cnf(c_11475,plain,
ifeq(product(A,B,C),true,ifeq(true,true,ifeq(product(A,D,E),true,ifeq(sum(D,multiplicative_identity,B),true,sum(E,A,C),true),true),true),true) = true,
inference(paramod,[status(thm)],[c_10,c_11]) ).
cnf(c_42,plain,
ifeq(product(A,B,C),true,ifeq(product(A,D,E),true,ifeq(sum(D,multiplicative_identity,B),true,sum(E,A,C),true),true),true) = true,
inference(paramod,[status(thm)],[c_2,c_11475]) ).
cnf(c_11476,plain,
ifeq(product(A,B,additive_identity),true,ifeq(true,true,ifeq(sum(B,C,D),true,ifeq(sum(A,C,E),true,product(E,D,C),true),true),true),true) = true,
inference(paramod,[status(thm)],[c_7,c_17]) ).
cnf(c_126,plain,
ifeq(product(A,B,additive_identity),true,ifeq(sum(B,C,D),true,ifeq(sum(A,C,E),true,product(E,D,C),true),true),true) = true,
inference(paramod,[status(thm)],[c_2,c_11476]) ).
cnf(c_11477,plain,
ifeq2(true,true,ifeq2(sum(A,additive_identity,B),true,B,A),A) = A,
inference(paramod,[status(thm)],[c_8,c_23]) ).
cnf(c_236,plain,
ifeq2(sum(A,additive_identity,B),true,B,A) = A,
inference(paramod,[status(thm)],[c_1,c_11477]) ).
cnf(c_11478,plain,
ifeq2(product(A,B,C),true,ifeq2(true,true,multiply(A,B),C),C) = C,
inference(paramod,[status(thm)],[c_4,c_24]) ).
cnf(c_243,plain,
ifeq2(product(A,B,C),true,multiply(A,B),C) = C,
inference(paramod,[status(thm)],[c_1,c_11478]) ).
cnf(c_11479,plain,
ifeq2(true,true,ifeq2(product(A,multiplicative_identity,B),true,B,A),A) = A,
inference(paramod,[status(thm)],[c_10,c_24]) ).
cnf(c_246,plain,
ifeq2(product(A,multiplicative_identity,B),true,B,A) = A,
inference(paramod,[status(thm)],[c_1,c_11479]) ).
cnf(c_11480,plain,
ifeq(product(A,B,C),true,ifeq(product(A,additive_identity,D),true,ifeq(true,true,sum(D,C,multiply(A,B)),true),true),true) = true,
inference(paramod,[status(thm)],[c_7,c_30]) ).
cnf(c_342,plain,
ifeq(product(A,B,C),true,ifeq(product(A,additive_identity,D),true,sum(D,C,multiply(A,B)),true),true) = true,
inference(paramod,[status(thm)],[c_2,c_11480]) ).
cnf(c_11481,plain,
ifeq2(true,true,multiply(A,inverse(A)),additive_identity) = additive_identity,
inference(paramod,[status(thm)],[c_22,c_243]) ).
cnf(c_470,plain,
multiply(A,inverse(A)) = additive_identity,
inference(paramod,[status(thm)],[c_1,c_11481]) ).
cnf(c_11482,plain,
ifeq(true,true,ifeq(product(A,B,C),true,ifeq(sum(B,multiplicative_identity,multiplicative_identity),true,sum(C,A,A),true),true),true) = true,
inference(paramod,[status(thm)],[c_10,c_41]) ).
cnf(c_488,plain,
ifeq(product(A,B,C),true,ifeq(sum(B,multiplicative_identity,multiplicative_identity),true,sum(C,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_2,c_11482]) ).
cnf(c_11483,plain,
ifeq(product(A,B,C),true,ifeq(true,true,ifeq(sum(multiplicative_identity,multiplicative_identity,B),true,sum(A,A,C),true),true),true) = true,
inference(paramod,[status(thm)],[c_10,c_42]) ).
cnf(c_497,plain,
ifeq(product(A,B,C),true,ifeq(sum(multiplicative_identity,multiplicative_identity,B),true,sum(A,A,C),true),true) = true,
inference(paramod,[status(thm)],[c_2,c_11483]) ).
cnf(c_11484,plain,
ifeq(product(A,additive_identity,additive_identity),true,ifeq(true,true,ifeq(sum(A,B,C),true,product(C,B,B),true),true),true) = true,
inference(paramod,[status(thm)],[c_7,c_126]) ).
cnf(c_1820,plain,
ifeq(product(A,additive_identity,additive_identity),true,ifeq(sum(A,B,C),true,product(C,B,B),true),true) = true,
inference(paramod,[status(thm)],[c_2,c_11484]) ).
cnf(c_11485,plain,
ifeq(true,true,ifeq(sum(multiplicative_identity,multiplicative_identity,multiplicative_identity),true,sum(A,A,A),true),true) = true,
inference(paramod,[status(thm)],[c_10,c_488]) ).
cnf(c_4492,plain,
ifeq(sum(multiplicative_identity,multiplicative_identity,multiplicative_identity),true,sum(A,A,A),true) = true,
inference(paramod,[status(thm)],[c_2,c_11485]) ).
cnf(c_11486,plain,
ifeq(product(A,add(multiplicative_identity,multiplicative_identity),B),true,ifeq(true,true,sum(A,A,B),true),true) = true,
inference(paramod,[status(thm)],[c_3,c_497]) ).
cnf(c_4587,plain,
ifeq(product(A,add(multiplicative_identity,multiplicative_identity),B),true,sum(A,A,B),true) = true,
inference(paramod,[status(thm)],[c_2,c_11486]) ).
cnf(c_11487,plain,
ifeq(true,true,ifeq(product(A,additive_identity,B),true,sum(B,additive_identity,multiply(A,inverse(A))),true),true) = true,
inference(paramod,[status(thm)],[c_22,c_342]) ).
cnf(c_11488,plain,
ifeq(true,true,ifeq(product(A,additive_identity,B),true,sum(B,additive_identity,additive_identity),true),true) = true,
inference(paramod,[status(thm)],[c_470,c_11487]) ).
cnf(c_10052,plain,
ifeq(product(A,additive_identity,B),true,sum(B,additive_identity,additive_identity),true) = true,
inference(paramod,[status(thm)],[c_2,c_11488]) ).
cnf(c_11489,plain,
ifeq(true,true,sum(multiply(A,additive_identity),additive_identity,additive_identity),true) = true,
inference(paramod,[status(thm)],[c_4,c_10052]) ).
cnf(c_10068,plain,
sum(multiply(A,additive_identity),additive_identity,additive_identity) = true,
inference(paramod,[status(thm)],[c_2,c_11489]) ).
cnf(c_11490,plain,
ifeq2(true,true,additive_identity,multiply(A,additive_identity)) = multiply(A,additive_identity),
inference(paramod,[status(thm)],[c_10068,c_236]) ).
cnf(c_11491,plain,
additive_identity = multiply(A,additive_identity),
inference(paramod,[status(thm)],[c_1,c_11490]) ).
cnf(c_10094,plain,
multiply(A,additive_identity) = additive_identity,
inference(copy,[status(thm)],[c_11491]) ).
cnf(c_10252,plain,
product(A,additive_identity,additive_identity) = true,
inference(paramod,[status(thm)],[c_10094,c_4]) ).
cnf(c_11492,plain,
ifeq(true,true,ifeq(sum(A,B,C),true,product(C,B,B),true),true) = true,
inference(paramod,[status(thm)],[c_10252,c_1820]) ).
cnf(c_10301,plain,
ifeq(sum(A,B,C),true,product(C,B,B),true) = true,
inference(paramod,[status(thm)],[c_2,c_11492]) ).
cnf(c_11493,plain,
ifeq(true,true,product(add(A,B),B,B),true) = true,
inference(paramod,[status(thm)],[c_3,c_10301]) ).
cnf(c_10552,plain,
product(add(A,B),B,B) = true,
inference(paramod,[status(thm)],[c_2,c_11493]) ).
cnf(c_11494,plain,
ifeq2(true,true,multiplicative_identity,add(A,multiplicative_identity)) = add(A,multiplicative_identity),
inference(paramod,[status(thm)],[c_10552,c_246]) ).
cnf(c_11495,plain,
multiplicative_identity = add(A,multiplicative_identity),
inference(paramod,[status(thm)],[c_1,c_11494]) ).
cnf(c_10801,plain,
add(A,multiplicative_identity) = multiplicative_identity,
inference(copy,[status(thm)],[c_11495]) ).
cnf(c_11496,plain,
ifeq(true,true,sum(add(A,add(multiplicative_identity,multiplicative_identity)),add(A,add(multiplicative_identity,multiplicative_identity)),add(multiplicative_identity,multiplicative_identity)),true) = true,
inference(paramod,[status(thm)],[c_10552,c_4587]) ).
cnf(c_11497,plain,
ifeq(true,true,sum(add(A,multiplicative_identity),add(A,add(multiplicative_identity,multiplicative_identity)),add(multiplicative_identity,multiplicative_identity)),true) = true,
inference(paramod,[status(thm)],[c_10801,c_11496]) ).
cnf(c_11498,plain,
ifeq(true,true,sum(multiplicative_identity,add(A,add(multiplicative_identity,multiplicative_identity)),add(multiplicative_identity,multiplicative_identity)),true) = true,
inference(paramod,[status(thm)],[c_10801,c_11497]) ).
cnf(c_11499,plain,
ifeq(true,true,sum(multiplicative_identity,add(A,multiplicative_identity),add(multiplicative_identity,multiplicative_identity)),true) = true,
inference(paramod,[status(thm)],[c_10801,c_11498]) ).
cnf(c_11500,plain,
ifeq(true,true,sum(multiplicative_identity,multiplicative_identity,add(multiplicative_identity,multiplicative_identity)),true) = true,
inference(paramod,[status(thm)],[c_10801,c_11499]) ).
cnf(c_11501,plain,
ifeq(true,true,sum(multiplicative_identity,multiplicative_identity,multiplicative_identity),true) = true,
inference(paramod,[status(thm)],[c_10801,c_11500]) ).
cnf(c_10959,plain,
sum(multiplicative_identity,multiplicative_identity,multiplicative_identity) = true,
inference(paramod,[status(thm)],[c_2,c_11501]) ).
cnf(c_11502,plain,
ifeq(true,true,sum(A,A,A),true) = true,
inference(paramod,[status(thm)],[c_10959,c_4492]) ).
cnf(c_11471,plain,
sum(A,A,A) = true,
inference(paramod,[status(thm)],[c_2,c_11502]) ).
cnf(c_11472,plain,
$false,
inference(resolve,[status(thm)],[c_11471,c_25]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO004-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.12/0.40 % Computer : n014.cluster.edu
% 0.12/0.40 % Model : x86_64 x86_64
% 0.12/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40 % Memory : 8046.5625MB
% 0.12/0.40 % OS : Linux 6.8.0-71-generic
% 0.12/0.40 % CPULimit : 300
% 0.12/0.40 % WCLimit : 300
% 0.12/0.40 % DateTime : Sat Sep 26 22:33:16 UTC 2026
% 0.12/0.41 % CPUTime :
% 0.12/0.41 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/0.41 % Process 64448 was started by sandbox2 on n014,
% 0.12/0.41 % Sat Sep 26 22:33:16 2026
% 0.12/0.41 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.12/0.41
% 0.12/0.41 % From the command line: assign(max_seconds, 300).
% 106.16/16.17
% 106.16/16.17 % given #500 (A,wt=40): 207 ifeq(product(A,B,C),true,ifeq(sum(D,E,B),true,ifeq(sum(D,inverse(E),A),true,sum(D,additive_identity,C),true),true),true) = true. [para(21(a,1),16(a,1,3,1)),rewrite([2(17)])].
% 106.16/16.17
% 106.16/16.17 % SZS status Unsatisfiable for theBenchmark
% 106.16/16.17
% 106.16/16.17 % Proof 1 at 6.37 (+ 0.75) seconds.
% 106.16/16.17 % Length of proof is 37.
% 106.16/16.17 % Level of proof is 12.
% 106.16/16.17 % Maximum clause weight is 46.000.
% 106.16/16.17 % Given clauses 800.
% 106.16/16.17
% 106.16/16.17 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------