%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : BOO007-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n026.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 : Fri Sep 25 12:59:33 PM UTC 2026
% Result : Unsatisfiable 56.14s 7.73s
% Output : Proof 56.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 67
% Number of leaves : 20
% Syntax : Number of formulae : 353 ( 325 unt; 0 def)
% Number of atoms : 437 ( 288 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 174 ( 90 ~; 84 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 10 con; 0-4 aty)
% Number of variables : 413 ( 16 sgn 98 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f15,axiom,
( sum(V3,X,V4)
| ~ product(V1,V2,V4)
| ~ product(Y,Z,V3)
| ~ sum(Z,X,V2)
| ~ sum(Y,X,V1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',distributivity8) ).
fof(f15_nnf,plain,
! [Y,X,V1,Z,V2,V3,V4] :
( sum(V3,X,V4)
| ~ product(V1,V2,V4)
| ~ product(Y,Z,V3)
| ~ sum(Z,X,V2)
| ~ sum(Y,X,V1) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [Y,X,V1,Z,V2,V3,V4] :
( sum(V3,X,V4)
| ~ product(V1,V2,V4)
| ~ product(Y,Z,V3)
| ~ sum(Z,X,V2)
| ~ sum(Y,X,V1) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( sum(X5,X1,X6)
| ~ product(X2,X4,X6)
| ~ product(X0,X3,X5)
| ~ sum(X3,X1,X4)
| ~ sum(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(hi15,axiom,
ifeq(sum(X0,X1,X2),true,ifeq(sum(X3,X1,X4),true,ifeq(product(X0,X3,X5),true,ifeq(product(X2,X4,X6),true,sum(X5,X1,X6),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(f0,axiom,
sum(X,Y,add(X,Y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',closure_of_addition) ).
fof(f0_nnf,plain,
! [X,Y] : sum(X,Y,add(X,Y)),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y] : sum(X,Y,add(X,Y)),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
sum(X0,X1,add(X0,X1)),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi0,axiom,
sum(X0,X1,add(X0,X1)) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(f1,axiom,
product(X,Y,multiply(X,Y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',closure_of_multiplication) ).
fof(f1_nnf,plain,
! [X,Y] : product(X,Y,multiply(X,Y)),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Y] : product(X,Y,multiply(X,Y)),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
product(X0,X1,multiply(X0,X1)),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(hi1,axiom,
product(X0,X1,multiply(X0,X1)) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(h5,plain,
sum(multiply(V0,V1),V2,multiply(add(V0,V2),add(V1,V2))) = true,
inference(hyper_resolution,[status(thm)],[hi15,hi0,hi0,hi1,hi1]) ).
cnf(f2,axiom,
( sum(Y,X,Z)
| ~ sum(X,Y,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_addition) ).
fof(f2_nnf,plain,
! [X,Y,Z] :
( sum(Y,X,Z)
| ~ sum(X,Y,Z) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X,Y,Z] :
( sum(Y,X,Z)
| ~ sum(X,Y,Z) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( sum(X1,X0,X2)
| ~ sum(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(hi2,axiom,
ifeq(sum(X0,X1,X2),true,sum(X1,X0,X2),true) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(h1,plain,
sum(V0,V1,add(V1,V0)) = true,
inference(hyper_resolution,[status(thm)],[hi2,hi0]) ).
cnf(f20,axiom,
( U = V
| ~ sum(X,Y,V)
| ~ sum(X,Y,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',addition_is_well_defined) ).
fof(f20_nnf,plain,
! [X,Y,U,V] :
( U = V
| ~ sum(X,Y,V)
| ~ sum(X,Y,U) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [X,Y,U,V] :
( U = V
| ~ sum(X,Y,V)
| ~ sum(X,Y,U) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
( X2 = X3
| ~ sum(X0,X1,X3)
| ~ sum(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(hi20,axiom,
ifeq(sum(X0,X1,X2),true,ifeq(sum(X0,X1,X3),true,X2,X3),X3) = X3,
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(t220,plain,
multiply(add(X1,X2),add(X3,X2)) = add(X2,multiply(X1,X3)),
inference(hyper_resolution,[status(thm)],[hi20,h1,h5]) ).
cnf(t288,plain,
multiply(add(X1,X2),add(X3,X2)) = add(X2,multiply(X1,X3)),
inference(orient,[status(thm)],[t220]) ).
cnf(f12,axiom,
( product(V1,V2,V4)
| ~ sum(X,V3,V4)
| ~ product(Y,Z,V3)
| ~ sum(X,Z,V2)
| ~ sum(X,Y,V1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',distributivity5) ).
fof(f12_nnf,plain,
! [X,Y,V1,Z,V2,V3,V4] :
( product(V1,V2,V4)
| ~ sum(X,V3,V4)
| ~ product(Y,Z,V3)
| ~ sum(X,Z,V2)
| ~ sum(X,Y,V1) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [X,Y,V1,Z,V2,V3,V4] :
( product(V1,V2,V4)
| ~ sum(X,V3,V4)
| ~ product(Y,Z,V3)
| ~ sum(X,Z,V2)
| ~ sum(X,Y,V1) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( product(X2,X4,X6)
| ~ sum(X0,X5,X6)
| ~ product(X1,X3,X5)
| ~ sum(X0,X3,X4)
| ~ sum(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(hi12,axiom,
ifeq(sum(X0,X1,X2),true,ifeq(sum(X0,X3,X4),true,ifeq(product(X1,X3,X5),true,ifeq(sum(X0,X5,X6),true,product(X2,X4,X6),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(h20,plain,
product(add(V0,V1),add(V0,V2),add(V0,multiply(V1,V2))) = true,
inference(hyper_resolution,[status(thm)],[hi12,hi0,hi0,hi1,hi0]) ).
cnf(f4,axiom,
sum(additive_identity,X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_identity1) ).
fof(f4_nnf,plain,
! [X] : sum(additive_identity,X,X),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X] : sum(additive_identity,X,X),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
sum(additive_identity,X0,X0),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(hi4,axiom,
sum(additive_identity,X0,X0) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(h14,plain,
product(V0,V1,add(additive_identity,multiply(V0,V1))) = true,
inference(hyper_resolution,[status(thm)],[hi12,hi4,hi4,hi1,hi0]) ).
cnf(f21,axiom,
( U = V
| ~ product(X,Y,V)
| ~ product(X,Y,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplication_is_well_defined) ).
fof(f21_nnf,plain,
! [X,Y,U,V] :
( U = V
| ~ product(X,Y,V)
| ~ product(X,Y,U) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [X,Y,U,V] :
( U = V
| ~ product(X,Y,V)
| ~ product(X,Y,U) ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
( X2 = X3
| ~ product(X0,X1,X3)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(hi21,axiom,
ifeq(product(X0,X1,X2),true,ifeq(product(X0,X1,X3),true,X2,X3),X3) = X3,
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(t228,plain,
add(additive_identity,multiply(add(X1,X2),add(X1,X3))) = add(X1,multiply(X2,X3)),
inference(hyper_resolution,[status(thm)],[hi21,h14,h20]) ).
cnf(t3,plain,
add(additive_identity,X1) = X1,
inference(hyper_resolution,[status(thm)],[hi20,hi4,hi0]) ).
cnf(t259,plain,
add(additive_identity,X1) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t25853,plain,
multiply(add(X1,X2),add(X1,X3)) = add(X1,multiply(X2,X3)),
inference(step,[status(thm)],[t228,t259]) ).
cnf(t282,plain,
multiply(add(X1,X2),add(X1,X3)) = add(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t25853]) ).
cnf(f17,axiom,
sum(X,inverse(X),multiplicative_identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_inverse2) ).
fof(f17_nnf,plain,
! [X] : sum(X,inverse(X),multiplicative_identity),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [X] : sum(X,inverse(X),multiplicative_identity),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
sum(X0,inverse(X0),multiplicative_identity),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(hi17,axiom,
sum(X0,inverse(X0),multiplicative_identity) = true,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(t11,plain,
add(X1,inverse(X1)) = multiplicative_identity,
inference(hyper_resolution,[status(thm)],[hi20,hi0,hi17]) ).
cnf(t455,plain,
add(X1,inverse(X1)) = multiplicative_identity,
inference(orient,[status(thm)],[t11]) ).
cnf(t457,plain,
add(X1,multiply(inverse(X1),X2)) = multiply(multiplicative_identity,add(X1,X2)),
inference(cp,[status(thm)],[t282,t455]) ).
cnf(f6,axiom,
product(multiplicative_identity,X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplicative_identity1) ).
fof(f6_nnf,plain,
! [X] : product(multiplicative_identity,X,X),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X] : product(multiplicative_identity,X,X),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
product(multiplicative_identity,X0,X0),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(hi6,axiom,
product(multiplicative_identity,X0,X0) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t31,plain,
add(additive_identity,multiply(multiplicative_identity,X1)) = X1,
inference(hyper_resolution,[status(thm)],[hi21,hi6,h14]) ).
cnf(t25851,plain,
multiply(multiplicative_identity,X1) = X1,
inference(step,[status(thm)],[t31,t259]) ).
cnf(t261,plain,
multiply(multiplicative_identity,X1) = X1,
inference(orient,[status(thm)],[t25851]) ).
cnf(t25919,plain,
add(X1,multiply(inverse(X1),X2)) = add(X1,X2),
inference(step,[status(thm)],[t457,t261]) ).
cnf(t3484,plain,
add(X1,multiply(inverse(X1),X2)) = add(X1,X2),
inference(orient,[status(thm)],[t25919]) ).
cnf(f11,axiom,
( product(V3,X,V4)
| ~ sum(V1,V2,V4)
| ~ sum(Y,Z,V3)
| ~ product(Z,X,V2)
| ~ product(Y,X,V1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',distributivity4) ).
fof(f11_nnf,plain,
! [Y,X,V1,Z,V2,V3,V4] :
( product(V3,X,V4)
| ~ sum(V1,V2,V4)
| ~ sum(Y,Z,V3)
| ~ product(Z,X,V2)
| ~ product(Y,X,V1) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [Y,X,V1,Z,V2,V3,V4] :
( product(V3,X,V4)
| ~ sum(V1,V2,V4)
| ~ sum(Y,Z,V3)
| ~ product(Z,X,V2)
| ~ product(Y,X,V1) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( product(X5,X1,X6)
| ~ sum(X2,X4,X6)
| ~ sum(X0,X3,X5)
| ~ product(X3,X1,X4)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(hi11,axiom,
ifeq(product(X0,X1,X2),true,ifeq(product(X3,X1,X4),true,ifeq(sum(X0,X3,X5),true,ifeq(sum(X2,X4,X6),true,product(X5,X1,X6),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(h21,plain,
product(V0,V1,add(multiply(additive_identity,V1),multiply(V0,V1))) = true,
inference(hyper_resolution,[status(thm)],[hi11,hi1,hi1,hi4,hi0]) ).
cnf(f18,axiom,
product(inverse(X),X,additive_identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplicative_inverse1) ).
fof(f18_nnf,plain,
! [X] : product(inverse(X),X,additive_identity),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [X] : product(inverse(X),X,additive_identity),
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
product(inverse(X0),X0,additive_identity),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(hi18,axiom,
product(inverse(X0),X0,additive_identity) = true,
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(t108,plain,
add(multiply(additive_identity,X1),multiply(inverse(X1),X1)) = additive_identity,
inference(hyper_resolution,[status(thm)],[hi21,hi18,h21]) ).
cnf(t212,plain,
add(multiply(additive_identity,X1),multiply(X2,X1)) = add(additive_identity,multiply(X2,X1)),
inference(hyper_resolution,[status(thm)],[hi21,h14,h21]) ).
cnf(t25858,plain,
add(multiply(additive_identity,X1),multiply(X2,X1)) = multiply(X2,X1),
inference(step,[status(thm)],[t212,t259]) ).
cnf(t735,plain,
add(multiply(additive_identity,X1),multiply(X2,X1)) = multiply(X2,X1),
inference(orient,[status(thm)],[t25858]) ).
cnf(t25862,plain,
multiply(inverse(X1),X1) = additive_identity,
inference(step,[status(thm)],[t108,t735]) ).
cnf(t795,plain,
multiply(inverse(X1),X1) = additive_identity,
inference(orient,[status(thm)],[t25862]) ).
cnf(t3486,plain,
add(X1,X1) = add(X1,additive_identity),
inference(cp,[status(thm)],[t3484,t795]) ).
cnf(f5,axiom,
sum(X,additive_identity,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_identity2) ).
fof(f5_nnf,plain,
! [X] : sum(X,additive_identity,X),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X] : sum(X,additive_identity,X),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
sum(X0,additive_identity,X0),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(hi5,axiom,
sum(X0,additive_identity,X0) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t2,plain,
add(X1,additive_identity) = X1,
inference(hyper_resolution,[status(thm)],[hi20,hi0,hi5]) ).
cnf(t256,plain,
add(X1,additive_identity) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t25920,plain,
add(X1,X1) = X1,
inference(step,[status(thm)],[t3486,t256]) ).
cnf(t3530,plain,
add(X1,X1) = X1,
inference(orient,[status(thm)],[t25920]) ).
cnf(t3531,plain,
add(X1,multiply(X1,X2)) = multiply(X1,add(X1,X2)),
inference(cp,[status(thm)],[t282,t3530]) ).
cnf(f14,axiom,
( product(V1,V2,V4)
| ~ sum(V3,X,V4)
| ~ product(Y,Z,V3)
| ~ sum(Z,X,V2)
| ~ sum(Y,X,V1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',distributivity7) ).
fof(f14_nnf,plain,
! [Y,X,V1,Z,V2,V3,V4] :
( product(V1,V2,V4)
| ~ sum(V3,X,V4)
| ~ product(Y,Z,V3)
| ~ sum(Z,X,V2)
| ~ sum(Y,X,V1) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [Y,X,V1,Z,V2,V3,V4] :
( product(V1,V2,V4)
| ~ sum(V3,X,V4)
| ~ product(Y,Z,V3)
| ~ sum(Z,X,V2)
| ~ sum(Y,X,V1) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( product(X2,X4,X6)
| ~ sum(X5,X1,X6)
| ~ product(X0,X3,X5)
| ~ sum(X3,X1,X4)
| ~ sum(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(hi14,axiom,
ifeq(sum(X0,X1,X2),true,ifeq(sum(X3,X1,X4),true,ifeq(product(X0,X3,X5),true,ifeq(sum(X5,X1,X6),true,product(X2,X4,X6),true),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(h7,plain,
product(V0,add(V1,V0),add(multiply(additive_identity,V1),V0)) = true,
inference(hyper_resolution,[status(thm)],[hi14,hi4,hi0,hi1,hi0]) ).
cnf(t204,plain,
add(additive_identity,multiply(X1,add(X2,X1))) = add(multiply(additive_identity,X2),X1),
inference(hyper_resolution,[status(thm)],[hi21,h7,h14]) ).
cnf(t25857,plain,
multiply(X1,add(X2,X1)) = add(multiply(additive_identity,X2),X1),
inference(step,[status(thm)],[t204,t259]) ).
cnf(t690,plain,
add(multiply(additive_identity,X1),X2) = multiply(X2,add(X1,X2)),
inference(orient,[status(thm)],[t25857]) ).
cnf(t797,plain,
multiply(inverse(X1),X1) = add(multiply(additive_identity,X1),additive_identity),
inference(cp,[status(thm)],[t735,t795]) ).
cnf(t25883,plain,
additive_identity = add(multiply(additive_identity,X1),additive_identity),
inference(step,[status(thm)],[t797,t795]) ).
cnf(t25884,plain,
additive_identity = multiply(additive_identity,X1),
inference(step,[status(thm)],[t25883,t256]) ).
cnf(t2882,plain,
multiply(additive_identity,X1) = additive_identity,
inference(orient,[status(thm)],[t25884]) ).
cnf(t25887,plain,
add(additive_identity,X2) = multiply(X2,add(X1,X2)),
inference(step,[status(thm)],[t690,t2882]) ).
cnf(t25888,plain,
X2 = multiply(X2,add(X1,X2)),
inference(step,[status(thm)],[t25887,t259]) ).
cnf(t2889,plain,
X2 = multiply(X2,add(X1,X2)),
inference(rw,[status(thm)],[t25888]) ).
cnf(t3187,plain,
multiply(X1,add(X2,X1)) = X1,
inference(orient,[status(thm)],[t2889]) ).
cnf(t29,plain,
add(X1,X2) = add(X2,X1),
inference(hyper_resolution,[status(thm)],[hi20,hi0,h1]) ).
cnf(t268,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t29]) ).
cnf(t3188,plain,
X1 = multiply(X1,add(X1,X2)),
inference(cp,[status(thm)],[t3187,t268]) ).
cnf(t3196,plain,
multiply(X1,add(X1,X2)) = X1,
inference(orient,[status(thm)],[t3188]) ).
cnf(t25922,plain,
add(X1,multiply(X1,X2)) = X1,
inference(step,[status(thm)],[t3531,t3196]) ).
cnf(t3651,plain,
add(X1,multiply(X1,X2)) = X1,
inference(orient,[status(thm)],[t25922]) ).
cnf(f23,hypothesis,
product(x,y_times_z,x_times__y_times_z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',x_times__y_times_z) ).
fof(f23_nnf,plain,
product(x,y_times_z,x_times__y_times_z),
inference(nnf_transformation,[status(thm)],[f23]) ).
cnf(c23,plain,
product(x,y_times_z,x_times__y_times_z),
inference(cnf_transformation,[status(esa)],[f23_nnf]) ).
cnf(hi23,axiom,
product(x,y_times_z,x_times__y_times_z) = true,
inference(equality_encoding,[status(esa)],[c23]) ).
cnf(t81,plain,
add(multiply(additive_identity,y_times_z),multiply(x,y_times_z)) = x_times__y_times_z,
inference(hyper_resolution,[status(thm)],[hi21,hi23,h21]) ).
cnf(t25865,plain,
multiply(x,y_times_z) = x_times__y_times_z,
inference(step,[status(thm)],[t81,t735]) ).
cnf(t808,plain,
multiply(x,y_times_z) = x_times__y_times_z,
inference(orient,[status(thm)],[t25865]) ).
cnf(t3652,plain,
x = add(x,x_times__y_times_z),
inference(cp,[status(thm)],[t3651,t808]) ).
cnf(t25923,plain,
x = add(x_times__y_times_z,x),
inference(step,[status(thm)],[t3652,t268]) ).
cnf(t3700,plain,
add(x_times__y_times_z,x) = x,
inference(orient,[status(thm)],[t25923]) ).
cnf(t3701,plain,
add(x_times__y_times_z,multiply(x,X1)) = multiply(x,add(x_times__y_times_z,X1)),
inference(cp,[status(thm)],[t282,t3700]) ).
cnf(t5179,plain,
add(x_times__y_times_z,multiply(x,X1)) = multiply(x,add(x_times__y_times_z,X1)),
inference(orient,[status(thm)],[t3701]) ).
cnf(f24,hypothesis,
product(x,y,x_times_y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',x_times_y) ).
fof(f24_nnf,plain,
product(x,y,x_times_y),
inference(nnf_transformation,[status(thm)],[f24]) ).
cnf(c24,plain,
product(x,y,x_times_y),
inference(cnf_transformation,[status(esa)],[f24_nnf]) ).
cnf(hi24,axiom,
product(x,y,x_times_y) = true,
inference(equality_encoding,[status(esa)],[c24]) ).
cnf(t80,plain,
add(multiply(additive_identity,y),multiply(x,y)) = x_times_y,
inference(hyper_resolution,[status(thm)],[hi21,hi24,h21]) ).
cnf(t25867,plain,
multiply(x,y) = x_times_y,
inference(step,[status(thm)],[t80,t735]) ).
cnf(t818,plain,
multiply(x,y) = x_times_y,
inference(orient,[status(thm)],[t25867]) ).
cnf(t5182,plain,
multiply(x,add(x_times__y_times_z,y)) = add(x_times__y_times_z,x_times_y),
inference(cp,[status(thm)],[t5179,t818]) ).
cnf(t25953,plain,
multiply(x,add(y,x_times__y_times_z)) = add(x_times__y_times_z,x_times_y),
inference(step,[status(thm)],[t5182,t268]) ).
cnf(t25954,plain,
multiply(x,add(y,x_times__y_times_z)) = add(x_times_y,x_times__y_times_z),
inference(step,[status(thm)],[t25953,t268]) ).
cnf(t5211,plain,
multiply(x,add(y,x_times__y_times_z)) = add(x_times_y,x_times__y_times_z),
inference(orient,[status(thm)],[t25954]) ).
cnf(f22,hypothesis,
product(y,z,y_times_z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',y_times_z) ).
fof(f22_nnf,plain,
product(y,z,y_times_z),
inference(nnf_transformation,[status(thm)],[f22]) ).
cnf(c22,plain,
product(y,z,y_times_z),
inference(cnf_transformation,[status(esa)],[f22_nnf]) ).
cnf(hi22,axiom,
product(y,z,y_times_z) = true,
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(t83,plain,
add(multiply(additive_identity,z),multiply(y,z)) = y_times_z,
inference(hyper_resolution,[status(thm)],[hi21,hi22,h21]) ).
cnf(t25864,plain,
multiply(y,z) = y_times_z,
inference(step,[status(thm)],[t83,t735]) ).
cnf(t805,plain,
multiply(y,z) = y_times_z,
inference(orient,[status(thm)],[t25864]) ).
cnf(t3654,plain,
y = add(y,y_times_z),
inference(cp,[status(thm)],[t3651,t805]) ).
cnf(t25926,plain,
y = add(y_times_z,y),
inference(step,[status(thm)],[t3654,t268]) ).
cnf(t3736,plain,
add(y_times_z,y) = y,
inference(orient,[status(thm)],[t25926]) ).
cnf(t3749,plain,
add(y,multiply(X1,y_times_z)) = multiply(add(X1,y),y),
inference(cp,[status(thm)],[t288,t3736]) ).
cnf(t5663,plain,
add(y,multiply(X1,y_times_z)) = multiply(add(X1,y),y),
inference(orient,[status(thm)],[t3749]) ).
cnf(t5668,plain,
multiply(add(x,y),y) = add(y,x_times__y_times_z),
inference(cp,[status(thm)],[t5663,t808]) ).
cnf(t25973,plain,
multiply(add(y,x),y) = add(y,x_times__y_times_z),
inference(step,[status(thm)],[t5668,t268]) ).
cnf(t3532,plain,
add(X1,multiply(X2,X1)) = multiply(add(X1,X2),X1),
inference(cp,[status(thm)],[t282,t3530]) ).
cnf(t5080,plain,
add(X1,multiply(X2,X1)) = multiply(add(X1,X2),X1),
inference(orient,[status(thm)],[t3532]) ).
cnf(t5095,plain,
multiply(add(y,x),y) = add(y,x_times_y),
inference(cp,[status(thm)],[t5080,t818]) ).
cnf(t5154,plain,
multiply(add(y,x),y) = add(y,x_times_y),
inference(orient,[status(thm)],[t5095]) ).
cnf(t25974,plain,
add(y,x_times_y) = add(y,x_times__y_times_z),
inference(step,[status(thm)],[t25973,t5154]) ).
cnf(t5687,plain,
add(y,x_times__y_times_z) = add(y,x_times_y),
inference(orient,[status(thm)],[t25974]) ).
cnf(t25975,plain,
multiply(x,add(y,x_times_y)) = add(x_times_y,x_times__y_times_z),
inference(step,[status(thm)],[t5211,t5687]) ).
cnf(t3653,plain,
x = add(x,x_times_y),
inference(cp,[status(thm)],[t3651,t818]) ).
cnf(t25925,plain,
x = add(x_times_y,x),
inference(step,[status(thm)],[t3653,t268]) ).
cnf(t3716,plain,
add(x_times_y,x) = x,
inference(orient,[status(thm)],[t25925]) ).
cnf(t3717,plain,
add(x_times_y,multiply(x,X1)) = multiply(x,add(x_times_y,X1)),
inference(cp,[status(thm)],[t282,t3716]) ).
cnf(t5367,plain,
add(x_times_y,multiply(x,X1)) = multiply(x,add(x_times_y,X1)),
inference(orient,[status(thm)],[t3717]) ).
cnf(t5373,plain,
multiply(x,add(x_times_y,y)) = add(x_times_y,x_times_y),
inference(cp,[status(thm)],[t5367,t818]) ).
cnf(t25962,plain,
multiply(x,add(y,x_times_y)) = add(x_times_y,x_times_y),
inference(step,[status(thm)],[t5373,t268]) ).
cnf(t25963,plain,
multiply(x,add(y,x_times_y)) = x_times_y,
inference(step,[status(thm)],[t25962,t3530]) ).
cnf(t5397,plain,
multiply(x,add(y,x_times_y)) = x_times_y,
inference(orient,[status(thm)],[t25963]) ).
cnf(t25976,plain,
x_times_y = add(x_times_y,x_times__y_times_z),
inference(step,[status(thm)],[t25975,t5397]) ).
cnf(t5702,plain,
x_times_y = add(x_times_y,x_times__y_times_z),
inference(rw,[status(thm)],[t25976]) ).
cnf(t5703,plain,
add(x_times_y,x_times__y_times_z) = x_times_y,
inference(orient,[status(thm)],[t5702]) ).
cnf(t5719,plain,
add(x_times__y_times_z,multiply(x_times_y,X1)) = multiply(x_times_y,add(X1,x_times__y_times_z)),
inference(cp,[status(thm)],[t288,t5703]) ).
cnf(t6563,plain,
add(x_times__y_times_z,multiply(x_times_y,X1)) = multiply(x_times_y,add(X1,x_times__y_times_z)),
inference(orient,[status(thm)],[t5719]) ).
cnf(f25,hypothesis,
product(x_times_y,z,x_times_y__times_z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',x_times_y__times_z) ).
fof(f25_nnf,plain,
product(x_times_y,z,x_times_y__times_z),
inference(nnf_transformation,[status(thm)],[f25]) ).
cnf(c25,plain,
product(x_times_y,z,x_times_y__times_z),
inference(cnf_transformation,[status(esa)],[f25_nnf]) ).
cnf(hi25,axiom,
product(x_times_y,z,x_times_y__times_z) = true,
inference(equality_encoding,[status(esa)],[c25]) ).
cnf(t82,plain,
add(multiply(additive_identity,z),multiply(x_times_y,z)) = x_times_y__times_z,
inference(hyper_resolution,[status(thm)],[hi21,hi25,h21]) ).
cnf(t25863,plain,
multiply(x_times_y,z) = x_times_y__times_z,
inference(step,[status(thm)],[t82,t735]) ).
cnf(t802,plain,
multiply(x_times_y,z) = x_times_y__times_z,
inference(orient,[status(thm)],[t25863]) ).
cnf(t6568,plain,
multiply(x_times_y,add(z,x_times__y_times_z)) = add(x_times__y_times_z,x_times_y__times_z),
inference(cp,[status(thm)],[t6563,t802]) ).
cnf(t26004,plain,
multiply(x_times_y,add(z,x_times__y_times_z)) = add(x_times_y__times_z,x_times__y_times_z),
inference(step,[status(thm)],[t6568,t268]) ).
cnf(t6596,plain,
multiply(x_times_y,add(z,x_times__y_times_z)) = add(x_times_y__times_z,x_times__y_times_z),
inference(orient,[status(thm)],[t26004]) ).
cnf(t3732,plain,
add(x,multiply(x_times_y,X1)) = multiply(x,add(X1,x)),
inference(cp,[status(thm)],[t288,t3716]) ).
cnf(t25934,plain,
add(x,multiply(x_times_y,X1)) = x,
inference(step,[status(thm)],[t3732,t3187]) ).
cnf(t4237,plain,
add(x,multiply(x_times_y,X1)) = x,
inference(orient,[status(thm)],[t25934]) ).
cnf(t4238,plain,
x = add(x,x_times_y__times_z),
inference(cp,[status(thm)],[t4237,t802]) ).
cnf(t25935,plain,
x = add(x_times_y__times_z,x),
inference(step,[status(thm)],[t4238,t268]) ).
cnf(t4260,plain,
add(x_times_y__times_z,x) = x,
inference(orient,[status(thm)],[t25935]) ).
cnf(t4261,plain,
add(x_times_y__times_z,multiply(x,X1)) = multiply(x,add(x_times_y__times_z,X1)),
inference(cp,[status(thm)],[t282,t4260]) ).
cnf(t6197,plain,
add(x_times_y__times_z,multiply(x,X1)) = multiply(x,add(x_times_y__times_z,X1)),
inference(orient,[status(thm)],[t4261]) ).
cnf(t6204,plain,
multiply(x,add(x_times_y__times_z,y_times_z)) = add(x_times_y__times_z,x_times__y_times_z),
inference(cp,[status(thm)],[t6197,t808]) ).
cnf(t25993,plain,
multiply(x,add(y_times_z,x_times_y__times_z)) = add(x_times_y__times_z,x_times__y_times_z),
inference(step,[status(thm)],[t6204,t268]) ).
cnf(t6240,plain,
multiply(x,add(y_times_z,x_times_y__times_z)) = add(x_times_y__times_z,x_times__y_times_z),
inference(orient,[status(thm)],[t25993]) ).
cnf(t286,plain,
add(X1,multiply(X2,X3)) = multiply(add(X1,X2),add(X3,X1)),
inference(cp,[status(thm)],[t282,t268]) ).
cnf(t7895,plain,
multiply(add(X1,X2),add(X3,X1)) = add(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t286]) ).
cnf(t284,plain,
add(X1,multiply(X2,X3)) = multiply(add(X2,X1),add(X1,X3)),
inference(cp,[status(thm)],[t282,t268]) ).
cnf(t5724,plain,
multiply(add(X1,X2),add(X2,X3)) = add(X2,multiply(X1,X3)),
inference(orient,[status(thm)],[t284]) ).
cnf(t459,plain,
add(inverse(X1),multiply(X1,X2)) = multiply(multiplicative_identity,add(X2,inverse(X1))),
inference(cp,[status(thm)],[t288,t455]) ).
cnf(t26042,plain,
add(inverse(X1),multiply(X1,X2)) = add(X2,inverse(X1)),
inference(step,[status(thm)],[t459,t261]) ).
cnf(t9140,plain,
add(inverse(X1),multiply(X1,X2)) = add(X2,inverse(X1)),
inference(orient,[status(thm)],[t26042]) ).
cnf(t3655,plain,
x_times_y = add(x_times_y,x_times_y__times_z),
inference(cp,[status(thm)],[t3651,t802]) ).
cnf(t25932,plain,
x_times_y = add(x_times_y__times_z,x_times_y),
inference(step,[status(thm)],[t3655,t268]) ).
cnf(t3755,plain,
add(x_times_y__times_z,x_times_y) = x_times_y,
inference(orient,[status(thm)],[t25932]) ).
cnf(t3761,plain,
x_times_y__times_z = multiply(x_times_y__times_z,x_times_y),
inference(cp,[status(thm)],[t3196,t3755]) ).
cnf(t3780,plain,
multiply(x_times_y__times_z,x_times_y) = x_times_y__times_z,
inference(orient,[status(thm)],[t3761]) ).
cnf(t9188,plain,
add(x_times_y,inverse(x_times_y__times_z)) = add(inverse(x_times_y__times_z),x_times_y__times_z),
inference(cp,[status(thm)],[t9140,t3780]) ).
cnf(t26045,plain,
add(x_times_y,inverse(x_times_y__times_z)) = add(x_times_y__times_z,inverse(x_times_y__times_z)),
inference(step,[status(thm)],[t9188,t268]) ).
cnf(t26046,plain,
add(x_times_y,inverse(x_times_y__times_z)) = multiplicative_identity,
inference(step,[status(thm)],[t26045,t455]) ).
cnf(t9296,plain,
add(x_times_y,inverse(x_times_y__times_z)) = multiplicative_identity,
inference(orient,[status(thm)],[t26046]) ).
cnf(t9301,plain,
add(inverse(x_times_y__times_z),multiply(x_times_y,X1)) = multiply(multiplicative_identity,add(inverse(x_times_y__times_z),X1)),
inference(cp,[status(thm)],[t5724,t9296]) ).
cnf(t26197,plain,
add(inverse(x_times_y__times_z),multiply(x_times_y,X1)) = add(inverse(x_times_y__times_z),X1),
inference(step,[status(thm)],[t9301,t261]) ).
cnf(t15364,plain,
add(inverse(x_times_y__times_z),multiply(x_times_y,X1)) = add(inverse(x_times_y__times_z),X1),
inference(orient,[status(thm)],[t26197]) ).
cnf(t15382,plain,
add(inverse(x_times_y__times_z),z) = add(inverse(x_times_y__times_z),x_times_y__times_z),
inference(cp,[status(thm)],[t15364,t802]) ).
cnf(t26198,plain,
add(z,inverse(x_times_y__times_z)) = add(inverse(x_times_y__times_z),x_times_y__times_z),
inference(step,[status(thm)],[t15382,t268]) ).
cnf(t26199,plain,
add(z,inverse(x_times_y__times_z)) = add(x_times_y__times_z,inverse(x_times_y__times_z)),
inference(step,[status(thm)],[t26198,t268]) ).
cnf(t26200,plain,
add(z,inverse(x_times_y__times_z)) = multiplicative_identity,
inference(step,[status(thm)],[t26199,t455]) ).
cnf(t15419,plain,
add(z,inverse(x_times_y__times_z)) = multiplicative_identity,
inference(orient,[status(thm)],[t26200]) ).
cnf(t15420,plain,
add(z,multiply(inverse(x_times_y__times_z),X1)) = multiply(multiplicative_identity,add(z,X1)),
inference(cp,[status(thm)],[t282,t15419]) ).
cnf(t26204,plain,
add(z,multiply(inverse(x_times_y__times_z),X1)) = add(z,X1),
inference(step,[status(thm)],[t15420,t261]) ).
cnf(t15543,plain,
add(z,multiply(inverse(x_times_y__times_z),X1)) = add(z,X1),
inference(orient,[status(thm)],[t26204]) ).
cnf(t15545,plain,
add(z,x_times_y__times_z) = add(z,additive_identity),
inference(cp,[status(thm)],[t15543,t795]) ).
cnf(t26205,plain,
add(z,x_times_y__times_z) = z,
inference(step,[status(thm)],[t15545,t256]) ).
cnf(t15583,plain,
add(z,x_times_y__times_z) = z,
inference(orient,[status(thm)],[t26205]) ).
cnf(t15593,plain,
add(x_times_y__times_z,multiply(X1,z)) = multiply(add(x_times_y__times_z,X1),z),
inference(cp,[status(thm)],[t7895,t15583]) ).
cnf(t16415,plain,
add(x_times_y__times_z,multiply(X1,z)) = multiply(add(x_times_y__times_z,X1),z),
inference(orient,[status(thm)],[t15593]) ).
cnf(t16424,plain,
multiply(add(x_times_y__times_z,y),z) = add(x_times_y__times_z,y_times_z),
inference(cp,[status(thm)],[t16415,t805]) ).
cnf(t26218,plain,
multiply(add(y,x_times_y__times_z),z) = add(x_times_y__times_z,y_times_z),
inference(step,[status(thm)],[t16424,t268]) ).
cnf(t26219,plain,
multiply(add(y,x_times_y__times_z),z) = add(y_times_z,x_times_y__times_z),
inference(step,[status(thm)],[t26218,t268]) ).
cnf(t16472,plain,
multiply(add(y,x_times_y__times_z),z) = add(y_times_z,x_times_y__times_z),
inference(orient,[status(thm)],[t26219]) ).
cnf(t4266,plain,
x_times_y__times_z = multiply(x_times_y__times_z,x),
inference(cp,[status(thm)],[t3196,t4260]) ).
cnf(t4277,plain,
multiply(x_times_y__times_z,x) = x_times_y__times_z,
inference(orient,[status(thm)],[t4266]) ).
cnf(t9189,plain,
add(x,inverse(x_times_y__times_z)) = add(inverse(x_times_y__times_z),x_times_y__times_z),
inference(cp,[status(thm)],[t9140,t4277]) ).
cnf(t26047,plain,
add(x,inverse(x_times_y__times_z)) = add(x_times_y__times_z,inverse(x_times_y__times_z)),
inference(step,[status(thm)],[t9189,t268]) ).
cnf(t26048,plain,
add(x,inverse(x_times_y__times_z)) = multiplicative_identity,
inference(step,[status(thm)],[t26047,t455]) ).
cnf(t9364,plain,
add(x,inverse(x_times_y__times_z)) = multiplicative_identity,
inference(orient,[status(thm)],[t26048]) ).
cnf(t9369,plain,
add(inverse(x_times_y__times_z),multiply(x,X1)) = multiply(multiplicative_identity,add(inverse(x_times_y__times_z),X1)),
inference(cp,[status(thm)],[t5724,t9364]) ).
cnf(t26231,plain,
add(inverse(x_times_y__times_z),multiply(x,X1)) = add(inverse(x_times_y__times_z),X1),
inference(step,[status(thm)],[t9369,t261]) ).
cnf(t17094,plain,
add(inverse(x_times_y__times_z),multiply(x,X1)) = add(inverse(x_times_y__times_z),X1),
inference(orient,[status(thm)],[t26231]) ).
cnf(t17121,plain,
add(inverse(x_times_y__times_z),y) = add(inverse(x_times_y__times_z),x_times_y),
inference(cp,[status(thm)],[t17094,t818]) ).
cnf(t26234,plain,
add(y,inverse(x_times_y__times_z)) = add(inverse(x_times_y__times_z),x_times_y),
inference(step,[status(thm)],[t17121,t268]) ).
cnf(t26235,plain,
add(y,inverse(x_times_y__times_z)) = add(x_times_y,inverse(x_times_y__times_z)),
inference(step,[status(thm)],[t26234,t268]) ).
cnf(t26236,plain,
add(y,inverse(x_times_y__times_z)) = multiplicative_identity,
inference(step,[status(thm)],[t26235,t9296]) ).
cnf(t17194,plain,
add(y,inverse(x_times_y__times_z)) = multiplicative_identity,
inference(orient,[status(thm)],[t26236]) ).
cnf(t17195,plain,
add(y,multiply(inverse(x_times_y__times_z),X1)) = multiply(multiplicative_identity,add(y,X1)),
inference(cp,[status(thm)],[t282,t17194]) ).
cnf(t26241,plain,
add(y,multiply(inverse(x_times_y__times_z),X1)) = add(y,X1),
inference(step,[status(thm)],[t17195,t261]) ).
cnf(t17500,plain,
add(y,multiply(inverse(x_times_y__times_z),X1)) = add(y,X1),
inference(orient,[status(thm)],[t26241]) ).
cnf(t17503,plain,
add(y,x_times_y__times_z) = add(y,additive_identity),
inference(cp,[status(thm)],[t17500,t795]) ).
cnf(t26242,plain,
add(y,x_times_y__times_z) = y,
inference(step,[status(thm)],[t17503,t256]) ).
cnf(t17538,plain,
add(y,x_times_y__times_z) = y,
inference(orient,[status(thm)],[t26242]) ).
cnf(t26245,plain,
multiply(y,z) = add(y_times_z,x_times_y__times_z),
inference(step,[status(thm)],[t16472,t17538]) ).
cnf(t26246,plain,
y_times_z = add(y_times_z,x_times_y__times_z),
inference(step,[status(thm)],[t26245,t805]) ).
cnf(t17574,plain,
y_times_z = add(y_times_z,x_times_y__times_z),
inference(rw,[status(thm)],[t26246]) ).
cnf(t17599,plain,
add(y_times_z,x_times_y__times_z) = y_times_z,
inference(orient,[status(thm)],[t17574]) ).
cnf(t26251,plain,
multiply(x,y_times_z) = add(x_times_y__times_z,x_times__y_times_z),
inference(step,[status(thm)],[t6240,t17599]) ).
cnf(t26252,plain,
x_times__y_times_z = add(x_times_y__times_z,x_times__y_times_z),
inference(step,[status(thm)],[t26251,t808]) ).
cnf(t17639,plain,
x_times__y_times_z = add(x_times_y__times_z,x_times__y_times_z),
inference(rw,[status(thm)],[t26252]) ).
cnf(t17653,plain,
add(x_times_y__times_z,x_times__y_times_z) = x_times__y_times_z,
inference(orient,[status(thm)],[t17639]) ).
cnf(t26255,plain,
multiply(x_times_y,add(z,x_times__y_times_z)) = x_times__y_times_z,
inference(step,[status(thm)],[t6596,t17653]) ).
cnf(t17654,plain,
multiply(x_times_y,add(z,x_times__y_times_z)) = x_times__y_times_z,
inference(orient,[status(thm)],[t26255]) ).
cnf(t3742,plain,
y_times_z = multiply(y_times_z,y),
inference(cp,[status(thm)],[t3196,t3736]) ).
cnf(t3776,plain,
multiply(y_times_z,y) = y_times_z,
inference(orient,[status(thm)],[t3742]) ).
cnf(t9192,plain,
add(y,inverse(y_times_z)) = add(inverse(y_times_z),y_times_z),
inference(cp,[status(thm)],[t9140,t3776]) ).
cnf(t26049,plain,
add(y,inverse(y_times_z)) = add(y_times_z,inverse(y_times_z)),
inference(step,[status(thm)],[t9192,t268]) ).
cnf(t26050,plain,
add(y,inverse(y_times_z)) = multiplicative_identity,
inference(step,[status(thm)],[t26049,t455]) ).
cnf(t9431,plain,
add(y,inverse(y_times_z)) = multiplicative_identity,
inference(orient,[status(thm)],[t26050]) ).
cnf(t9436,plain,
add(inverse(y_times_z),multiply(y,X1)) = multiply(multiplicative_identity,add(inverse(y_times_z),X1)),
inference(cp,[status(thm)],[t5724,t9431]) ).
cnf(t26321,plain,
add(inverse(y_times_z),multiply(y,X1)) = add(inverse(y_times_z),X1),
inference(step,[status(thm)],[t9436,t261]) ).
cnf(t22741,plain,
add(inverse(y_times_z),multiply(y,X1)) = add(inverse(y_times_z),X1),
inference(orient,[status(thm)],[t26321]) ).
cnf(t22748,plain,
add(inverse(y_times_z),z) = add(inverse(y_times_z),y_times_z),
inference(cp,[status(thm)],[t22741,t805]) ).
cnf(t26322,plain,
add(z,inverse(y_times_z)) = add(inverse(y_times_z),y_times_z),
inference(step,[status(thm)],[t22748,t268]) ).
cnf(t26323,plain,
add(z,inverse(y_times_z)) = add(y_times_z,inverse(y_times_z)),
inference(step,[status(thm)],[t26322,t268]) ).
cnf(t26324,plain,
add(z,inverse(y_times_z)) = multiplicative_identity,
inference(step,[status(thm)],[t26323,t455]) ).
cnf(t22791,plain,
add(z,inverse(y_times_z)) = multiplicative_identity,
inference(orient,[status(thm)],[t26324]) ).
cnf(t22792,plain,
add(z,multiply(inverse(y_times_z),X1)) = multiply(multiplicative_identity,add(z,X1)),
inference(cp,[status(thm)],[t282,t22791]) ).
cnf(t26327,plain,
add(z,multiply(inverse(y_times_z),X1)) = add(z,X1),
inference(step,[status(thm)],[t22792,t261]) ).
cnf(t22900,plain,
add(z,multiply(inverse(y_times_z),X1)) = add(z,X1),
inference(orient,[status(thm)],[t26327]) ).
cnf(t22902,plain,
add(z,y_times_z) = add(z,additive_identity),
inference(cp,[status(thm)],[t22900,t795]) ).
cnf(t26328,plain,
add(z,y_times_z) = z,
inference(step,[status(thm)],[t22902,t256]) ).
cnf(t23180,plain,
add(z,y_times_z) = z,
inference(orient,[status(thm)],[t26328]) ).
cnf(t23186,plain,
add(z,multiply(X1,y_times_z)) = multiply(add(z,X1),z),
inference(cp,[status(thm)],[t282,t23180]) ).
cnf(t23665,plain,
add(z,multiply(X1,y_times_z)) = multiply(add(z,X1),z),
inference(orient,[status(thm)],[t23186]) ).
cnf(t3706,plain,
x_times__y_times_z = multiply(x_times__y_times_z,x),
inference(cp,[status(thm)],[t3196,t3700]) ).
cnf(t3770,plain,
multiply(x_times__y_times_z,x) = x_times__y_times_z,
inference(orient,[status(thm)],[t3706]) ).
cnf(t9211,plain,
add(x,inverse(x_times__y_times_z)) = add(inverse(x_times__y_times_z),x_times__y_times_z),
inference(cp,[status(thm)],[t9140,t3770]) ).
cnf(t26051,plain,
add(x,inverse(x_times__y_times_z)) = add(x_times__y_times_z,inverse(x_times__y_times_z)),
inference(step,[status(thm)],[t9211,t268]) ).
cnf(t26052,plain,
add(x,inverse(x_times__y_times_z)) = multiplicative_identity,
inference(step,[status(thm)],[t26051,t455]) ).
cnf(t9494,plain,
add(x,inverse(x_times__y_times_z)) = multiplicative_identity,
inference(orient,[status(thm)],[t26052]) ).
cnf(t9499,plain,
add(inverse(x_times__y_times_z),multiply(x,X1)) = multiply(multiplicative_identity,add(inverse(x_times__y_times_z),X1)),
inference(cp,[status(thm)],[t5724,t9494]) ).
cnf(t26356,plain,
add(inverse(x_times__y_times_z),multiply(x,X1)) = add(inverse(x_times__y_times_z),X1),
inference(step,[status(thm)],[t9499,t261]) ).
cnf(t24712,plain,
add(inverse(x_times__y_times_z),multiply(x,X1)) = add(inverse(x_times__y_times_z),X1),
inference(orient,[status(thm)],[t26356]) ).
cnf(t24734,plain,
add(inverse(x_times__y_times_z),y_times_z) = add(inverse(x_times__y_times_z),x_times__y_times_z),
inference(cp,[status(thm)],[t24712,t808]) ).
cnf(t26358,plain,
add(y_times_z,inverse(x_times__y_times_z)) = add(inverse(x_times__y_times_z),x_times__y_times_z),
inference(step,[status(thm)],[t24734,t268]) ).
cnf(t26359,plain,
add(y_times_z,inverse(x_times__y_times_z)) = add(x_times__y_times_z,inverse(x_times__y_times_z)),
inference(step,[status(thm)],[t26358,t268]) ).
cnf(t26360,plain,
add(y_times_z,inverse(x_times__y_times_z)) = multiplicative_identity,
inference(step,[status(thm)],[t26359,t455]) ).
cnf(t24777,plain,
add(y_times_z,inverse(x_times__y_times_z)) = multiplicative_identity,
inference(orient,[status(thm)],[t26360]) ).
cnf(t24778,plain,
add(y_times_z,multiply(inverse(x_times__y_times_z),X1)) = multiply(multiplicative_identity,add(y_times_z,X1)),
inference(cp,[status(thm)],[t282,t24777]) ).
cnf(t26368,plain,
add(y_times_z,multiply(inverse(x_times__y_times_z),X1)) = add(y_times_z,X1),
inference(step,[status(thm)],[t24778,t261]) ).
cnf(t24998,plain,
add(y_times_z,multiply(inverse(x_times__y_times_z),X1)) = add(y_times_z,X1),
inference(orient,[status(thm)],[t26368]) ).
cnf(t25001,plain,
add(y_times_z,x_times__y_times_z) = add(y_times_z,additive_identity),
inference(cp,[status(thm)],[t24998,t795]) ).
cnf(t26369,plain,
add(y_times_z,x_times__y_times_z) = y_times_z,
inference(step,[status(thm)],[t25001,t256]) ).
cnf(t25043,plain,
add(y_times_z,x_times__y_times_z) = y_times_z,
inference(orient,[status(thm)],[t26369]) ).
cnf(t25054,plain,
add(x_times__y_times_z,multiply(X1,y_times_z)) = multiply(add(x_times__y_times_z,X1),y_times_z),
inference(cp,[status(thm)],[t7895,t25043]) ).
cnf(t25660,plain,
add(x_times__y_times_z,multiply(X1,y_times_z)) = multiply(add(x_times__y_times_z,X1),y_times_z),
inference(orient,[status(thm)],[t25054]) ).
cnf(t25671,plain,
multiply(add(x_times__y_times_z,inverse(y_times_z)),y_times_z) = add(x_times__y_times_z,additive_identity),
inference(cp,[status(thm)],[t25660,t795]) ).
cnf(t9435,plain,
add(inverse(y_times_z),multiply(X1,y)) = multiply(add(inverse(y_times_z),X1),multiplicative_identity),
inference(cp,[status(thm)],[t7895,t9431]) ).
cnf(f7,axiom,
product(X,multiplicative_identity,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplicative_identity2) ).
fof(f7_nnf,plain,
! [X] : product(X,multiplicative_identity,X),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X] : product(X,multiplicative_identity,X),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
product(X0,multiplicative_identity,X0),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(hi7,axiom,
product(X0,multiplicative_identity,X0) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t30,plain,
add(additive_identity,multiply(X1,multiplicative_identity)) = X1,
inference(hyper_resolution,[status(thm)],[hi21,hi7,h14]) ).
cnf(t25850,plain,
multiply(X1,multiplicative_identity) = X1,
inference(step,[status(thm)],[t30,t259]) ).
cnf(t260,plain,
multiply(X1,multiplicative_identity) = X1,
inference(orient,[status(thm)],[t25850]) ).
cnf(t26308,plain,
add(inverse(y_times_z),multiply(X1,y)) = add(inverse(y_times_z),X1),
inference(step,[status(thm)],[t9435,t260]) ).
cnf(t22312,plain,
add(inverse(y_times_z),multiply(X1,y)) = add(inverse(y_times_z),X1),
inference(orient,[status(thm)],[t26308]) ).
cnf(t22318,plain,
add(inverse(y_times_z),x) = add(inverse(y_times_z),x_times_y),
inference(cp,[status(thm)],[t22312,t818]) ).
cnf(t26309,plain,
add(x,inverse(y_times_z)) = add(inverse(y_times_z),x_times_y),
inference(step,[status(thm)],[t22318,t268]) ).
cnf(t460,plain,
add(inverse(X1),multiply(X2,X1)) = multiply(add(X2,inverse(X1)),multiplicative_identity),
inference(cp,[status(thm)],[t288,t455]) ).
cnf(t26152,plain,
add(inverse(X1),multiply(X2,X1)) = add(X2,inverse(X1)),
inference(step,[status(thm)],[t460,t260]) ).
cnf(t13790,plain,
add(inverse(X1),multiply(X2,X1)) = add(X2,inverse(X1)),
inference(orient,[status(thm)],[t26152]) ).
cnf(t13893,plain,
add(x,inverse(y_times_z)) = add(inverse(y_times_z),x_times__y_times_z),
inference(cp,[status(thm)],[t13790,t808]) ).
cnf(t26153,plain,
add(x,inverse(y_times_z)) = add(x_times__y_times_z,inverse(y_times_z)),
inference(step,[status(thm)],[t13893,t268]) ).
cnf(t13956,plain,
add(x,inverse(y_times_z)) = add(x_times__y_times_z,inverse(y_times_z)),
inference(orient,[status(thm)],[t26153]) ).
cnf(t26310,plain,
add(x_times__y_times_z,inverse(y_times_z)) = add(inverse(y_times_z),x_times_y),
inference(step,[status(thm)],[t26309,t13956]) ).
cnf(t26311,plain,
add(x_times__y_times_z,inverse(y_times_z)) = add(x_times_y,inverse(y_times_z)),
inference(step,[status(thm)],[t26310,t268]) ).
cnf(t22352,plain,
add(x_times__y_times_z,inverse(y_times_z)) = add(x_times_y,inverse(y_times_z)),
inference(orient,[status(thm)],[t26311]) ).
cnf(t26383,plain,
multiply(add(x_times_y,inverse(y_times_z)),y_times_z) = add(x_times__y_times_z,additive_identity),
inference(step,[status(thm)],[t25671,t22352]) ).
cnf(t26384,plain,
multiply(add(x_times_y,inverse(y_times_z)),y_times_z) = x_times__y_times_z,
inference(step,[status(thm)],[t26383,t256]) ).
cnf(t25720,plain,
multiply(add(x_times_y,inverse(y_times_z)),y_times_z) = x_times__y_times_z,
inference(orient,[status(thm)],[t26384]) ).
cnf(t25722,plain,
multiply(add(z,add(x_times_y,inverse(y_times_z))),z) = add(z,x_times__y_times_z),
inference(cp,[status(thm)],[t23665,t25720]) ).
cnf(t22905,plain,
add(z,add(X1,inverse(y_times_z))) = add(z,inverse(y_times_z)),
inference(cp,[status(thm)],[t22900,t3187]) ).
cnf(t26336,plain,
add(z,add(X1,inverse(y_times_z))) = multiplicative_identity,
inference(step,[status(thm)],[t22905,t22791]) ).
cnf(t23385,plain,
add(z,add(X1,inverse(y_times_z))) = multiplicative_identity,
inference(orient,[status(thm)],[t26336]) ).
cnf(t26385,plain,
multiply(multiplicative_identity,z) = add(z,x_times__y_times_z),
inference(step,[status(thm)],[t25722,t23385]) ).
cnf(t26386,plain,
z = add(z,x_times__y_times_z),
inference(step,[status(thm)],[t26385,t261]) ).
cnf(t25734,plain,
add(z,x_times__y_times_z) = z,
inference(orient,[status(thm)],[t26386]) ).
cnf(t26392,plain,
multiply(x_times_y,z) = x_times__y_times_z,
inference(step,[status(thm)],[t17654,t25734]) ).
cnf(t26393,plain,
x_times_y__times_z = x_times__y_times_z,
inference(step,[status(thm)],[t26392,t802]) ).
cnf(t25779,plain,
x_times_y__times_z = x_times__y_times_z,
inference(rw,[status(thm)],[t26393]) ).
cnf(t25780,plain,
x_times__y_times_z = x_times_y__times_z,
inference(orient,[status(thm)],[t25779]) ).
cnf(f26,negated_conjecture,
x_times__y_times_z != x_times_y__times_z,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_equality) ).
fof(f26_nnf,plain,
x_times__y_times_z != x_times_y__times_z,
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
x_times__y_times_z != x_times_y__times_z,
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c26,plain,
x_times__y_times_z != x_times_y__times_z,
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(goal_0,negated_conjecture,
x_times_y__times_z != x_times__y_times_z,
inference(equality_encoding,[status(esa)],[c26]) ).
cnf(g0_0,plain,
x_times_y__times_z != x_times_y__times_z,
inference(rw,[status(thm)],[goal_0,t25780]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : BOO007-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n026.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Fri Sep 25 06:28:39 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 56.14/7.73 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 56.14/7.73 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------