%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : BOO014-3 : TPTP v9.3.1. Bugfixed v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.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:06 AM UTC 2026
% Result : Unsatisfiable 260.66s 33.48s
% Output : CNFRefutation 260.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 25
% Syntax : Number of formulae : 238 ( 131 unt; 0 def)
% Number of atoms : 466 ( 60 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 463 ( 235 ~; 228 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 522 ( 10 sgn 78 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(closure_of_addition,axiom,
! [VAR_0,VAR_1] : sum(VAR_0,VAR_1,add(VAR_0,VAR_1)),
file('theBenchmark.p',closure_of_addition) ).
cnf(c_1,plain,
sum(A,B,add(A,B)),
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)),
file('theBenchmark.p',closure_of_multiplication) ).
cnf(c_2,plain,
product(A,B,multiply(A,B)),
inference(clausify,[status(thm)],[closure_of_multiplication]) ).
fof(commutativity_of_addition,axiom,
! [VAR_0,VAR_1,VAR_2] :
( sum(VAR_1,VAR_0,VAR_2)
| ~ sum(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',commutativity_of_addition) ).
cnf(c_3,plain,
( sum(B,A,C)
| ~ sum(A,B,C) ),
inference(clausify,[status(thm)],[commutativity_of_addition]) ).
fof(commutativity_of_multiplication,axiom,
! [VAR_0,VAR_1,VAR_2] :
( product(VAR_1,VAR_0,VAR_2)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',commutativity_of_multiplication) ).
cnf(c_4,plain,
( product(B,A,C)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[commutativity_of_multiplication]) ).
fof(additive_identity1,axiom,
! [VAR_0] : sum(additive_identity,VAR_0,VAR_0),
file('theBenchmark.p',additive_identity1) ).
cnf(c_5,plain,
sum(additive_identity,A,A),
inference(clausify,[status(thm)],[additive_identity1]) ).
fof(additive_identity2,axiom,
! [VAR_0] : sum(VAR_0,additive_identity,VAR_0),
file('theBenchmark.p',additive_identity2) ).
cnf(c_6,plain,
sum(A,additive_identity,A),
inference(clausify,[status(thm)],[additive_identity2]) ).
fof(multiplicative_identity1,axiom,
! [VAR_0] : product(multiplicative_identity,VAR_0,VAR_0),
file('theBenchmark.p',multiplicative_identity1) ).
cnf(c_7,plain,
product(multiplicative_identity,A,A),
inference(clausify,[status(thm)],[multiplicative_identity1]) ).
fof(multiplicative_identity2,axiom,
! [VAR_0] : product(VAR_0,multiplicative_identity,VAR_0),
file('theBenchmark.p',multiplicative_identity2) ).
cnf(c_8,plain,
product(A,multiplicative_identity,A),
inference(clausify,[status(thm)],[multiplicative_identity2]) ).
fof(distributivity1,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( sum(VAR_2,VAR_4,VAR_6)
| ~ product(VAR_0,VAR_5,VAR_6)
| ~ sum(VAR_1,VAR_3,VAR_5)
| ~ product(VAR_0,VAR_3,VAR_4)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',distributivity1) ).
cnf(c_9,plain,
( sum(C,E,V6)
| ~ product(A,F,V6)
| ~ sum(B,D,F)
| ~ product(A,D,E)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[distributivity1]) ).
fof(distributivity2,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( product(VAR_0,VAR_5,VAR_6)
| ~ sum(VAR_2,VAR_4,VAR_6)
| ~ sum(VAR_1,VAR_3,VAR_5)
| ~ product(VAR_0,VAR_3,VAR_4)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',distributivity2) ).
cnf(c_10,plain,
( product(A,F,V6)
| ~ sum(C,E,V6)
| ~ sum(B,D,F)
| ~ product(A,D,E)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[distributivity2]) ).
fof(distributivity3,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( sum(VAR_2,VAR_4,VAR_6)
| ~ product(VAR_5,VAR_1,VAR_6)
| ~ sum(VAR_0,VAR_3,VAR_5)
| ~ product(VAR_3,VAR_1,VAR_4)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',distributivity3) ).
cnf(c_11,plain,
( sum(C,E,V6)
| ~ product(F,B,V6)
| ~ sum(A,D,F)
| ~ product(D,B,E)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[distributivity3]) ).
fof(distributivity4,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( product(VAR_5,VAR_1,VAR_6)
| ~ sum(VAR_2,VAR_4,VAR_6)
| ~ sum(VAR_0,VAR_3,VAR_5)
| ~ product(VAR_3,VAR_1,VAR_4)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',distributivity4) ).
cnf(c_12,plain,
( product(F,B,V6)
| ~ sum(C,E,V6)
| ~ sum(A,D,F)
| ~ product(D,B,E)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[distributivity4]) ).
fof(distributivity5,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( product(VAR_2,VAR_4,VAR_6)
| ~ sum(VAR_0,VAR_5,VAR_6)
| ~ product(VAR_1,VAR_3,VAR_5)
| ~ sum(VAR_0,VAR_3,VAR_4)
| ~ sum(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',distributivity5) ).
cnf(c_13,plain,
( product(C,E,V6)
| ~ sum(A,F,V6)
| ~ product(B,D,F)
| ~ sum(A,D,E)
| ~ sum(A,B,C) ),
inference(clausify,[status(thm)],[distributivity5]) ).
fof(distributivity6,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( sum(VAR_0,VAR_5,VAR_6)
| ~ product(VAR_2,VAR_4,VAR_6)
| ~ product(VAR_1,VAR_3,VAR_5)
| ~ sum(VAR_0,VAR_3,VAR_4)
| ~ sum(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',distributivity6) ).
cnf(c_14,plain,
( sum(A,F,V6)
| ~ product(C,E,V6)
| ~ product(B,D,F)
| ~ sum(A,D,E)
| ~ sum(A,B,C) ),
inference(clausify,[status(thm)],[distributivity6]) ).
fof(distributivity7,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( product(VAR_2,VAR_4,VAR_6)
| ~ sum(VAR_5,VAR_1,VAR_6)
| ~ product(VAR_0,VAR_3,VAR_5)
| ~ sum(VAR_3,VAR_1,VAR_4)
| ~ sum(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',distributivity7) ).
cnf(c_15,plain,
( product(C,E,V6)
| ~ sum(F,B,V6)
| ~ product(A,D,F)
| ~ sum(D,B,E)
| ~ sum(A,B,C) ),
inference(clausify,[status(thm)],[distributivity7]) ).
fof(additive_inverse1,axiom,
! [VAR_0] : sum(inverse(VAR_0),VAR_0,multiplicative_identity),
file('theBenchmark.p',additive_inverse1) ).
cnf(c_17,plain,
sum(inverse(A),A,multiplicative_identity),
inference(clausify,[status(thm)],[additive_inverse1]) ).
fof(additive_inverse2,axiom,
! [VAR_0] : sum(VAR_0,inverse(VAR_0),multiplicative_identity),
file('theBenchmark.p',additive_inverse2) ).
cnf(c_18,plain,
sum(A,inverse(A),multiplicative_identity),
inference(clausify,[status(thm)],[additive_inverse2]) ).
fof(multiplicative_inverse2,axiom,
! [VAR_0] : product(VAR_0,inverse(VAR_0),additive_identity),
file('theBenchmark.p',multiplicative_inverse2) ).
cnf(c_20,plain,
product(A,inverse(A),additive_identity),
inference(clausify,[status(thm)],[multiplicative_inverse2]) ).
fof(addition_is_well_defined,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( VAR_2 = VAR_3
| ~ sum(VAR_0,VAR_1,VAR_3)
| ~ sum(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',addition_is_well_defined) ).
cnf(c_21,plain,
( C = D
| ~ sum(A,B,D)
| ~ sum(A,B,C) ),
inference(clausify,[status(thm)],[addition_is_well_defined]) ).
fof(multiplication_is_well_defined,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( VAR_2 = VAR_3
| ~ product(VAR_0,VAR_1,VAR_3)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',multiplication_is_well_defined) ).
cnf(c_22,plain,
( C = D
| ~ product(A,B,D)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[multiplication_is_well_defined]) ).
fof(inverse_is_self_cancelling,axiom,
! [VAR_0] : inverse(inverse(VAR_0)) = VAR_0,
file('theBenchmark.p',inverse_is_self_cancelling) ).
cnf(c_23,plain,
inverse(inverse(A)) = A,
inference(clausify,[status(thm)],[inverse_is_self_cancelling]) ).
fof(inverse_is_unique,axiom,
! [VAR_0,VAR_1,VAR_2] :
( VAR_1 = VAR_2
| ~ product(VAR_0,VAR_2,additive_identity)
| ~ product(VAR_0,VAR_1,additive_identity)
| ~ sum(VAR_0,VAR_2,multiplicative_identity)
| ~ sum(VAR_0,VAR_1,multiplicative_identity) ),
file('theBenchmark.p',inverse_is_unique) ).
cnf(c_24,plain,
( B = C
| ~ product(A,C,additive_identity)
| ~ product(A,B,additive_identity)
| ~ sum(A,C,multiplicative_identity)
| ~ sum(A,B,multiplicative_identity) ),
inference(clausify,[status(thm)],[inverse_is_unique]) ).
fof(x_plus_y,axiom,
sum(x,y,x_plus_y),
file('theBenchmark.p',x_plus_y) ).
cnf(c_25,plain,
sum(x,y,x_plus_y),
inference(clausify,[status(thm)],[x_plus_y]) ).
fof(x_inverse_times_y_inverse,axiom,
product(inverse(x),inverse(y),x_inverse_times_y_inverse),
file('theBenchmark.p',x_inverse_times_y_inverse) ).
cnf(c_26,plain,
product(inverse(x),inverse(y),x_inverse_times_y_inverse),
inference(clausify,[status(thm)],[x_inverse_times_y_inverse]) ).
fof(prove_equation,axiom,
inverse(x_plus_y) != x_inverse_times_y_inverse,
file('theBenchmark.p',prove_equation) ).
cnf(c_27,plain,
inverse(x_plus_y) != x_inverse_times_y_inverse,
inference(clausify,[status(thm)],[prove_equation]) ).
cnf(c_28,plain,
sum(A,B,add(B,A)),
inference(resolve,[status(thm)],[c_3,c_1]) ).
cnf(c_29,plain,
product(A,B,multiply(B,A)),
inference(resolve,[status(thm)],[c_4,c_2]) ).
cnf(c_18644,plain,
( sum(A,C,E)
| ~ product(A,D,E)
| ~ sum(multiplicative_identity,B,D)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_9,c_8]) ).
cnf(c_18645,plain,
( sum(C,multiply(C,A),D)
| ~ product(C,B,D)
| ~ sum(multiplicative_identity,A,B) ),
inference(resolve,[status(thm)],[c_18644,c_2]) ).
cnf(c_18646,plain,
( sum(A,multiply(A,additive_identity),B)
| ~ product(A,multiplicative_identity,B) ),
inference(resolve,[status(thm)],[c_18645,c_6]) ).
cnf(c_33,plain,
sum(A,multiply(A,additive_identity),A),
inference(resolve,[status(thm)],[c_18646,c_8]) ).
cnf(c_18647,plain,
( sum(A,C,E)
| ~ product(A,D,E)
| ~ sum(multiplicative_identity,B,D)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_9,c_8]) ).
cnf(c_18648,plain,
( sum(C,multiply(C,A),D)
| ~ product(C,B,D)
| ~ sum(multiplicative_identity,A,B) ),
inference(resolve,[status(thm)],[c_18647,c_2]) ).
cnf(c_18649,plain,
( sum(A,multiply(A,B),C)
| ~ product(A,add(multiplicative_identity,B),C) ),
inference(resolve,[status(thm)],[c_18648,c_1]) ).
cnf(c_36,plain,
sum(A,multiply(A,B),multiply(A,add(multiplicative_identity,B))),
inference(resolve,[status(thm)],[c_18649,c_2]) ).
cnf(c_18650,plain,
( sum(multiply(A,D),C,F)
| ~ product(A,E,F)
| ~ sum(D,B,E)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_9,c_2]) ).
cnf(c_18651,plain,
( sum(multiply(C,A),C,D)
| ~ product(C,B,D)
| ~ sum(A,multiplicative_identity,B) ),
inference(resolve,[status(thm)],[c_18650,c_8]) ).
cnf(c_18652,plain,
( sum(multiply(A,B),A,C)
| ~ product(A,add(B,multiplicative_identity),C) ),
inference(resolve,[status(thm)],[c_18651,c_1]) ).
cnf(c_51,plain,
sum(multiply(A,B),A,multiply(A,add(B,multiplicative_identity))),
inference(resolve,[status(thm)],[c_18652,c_2]) ).
cnf(c_18653,plain,
( product(A,E,F)
| ~ sum(multiply(A,D),C,F)
| ~ sum(D,B,E)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_10,c_2]) ).
cnf(c_18654,plain,
( product(D,C,E)
| ~ sum(multiply(D,A),multiply(D,B),E)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_18653,c_2]) ).
cnf(c_18655,plain,
( product(A,add(B,C),D)
| ~ sum(multiply(A,B),multiply(A,C),D) ),
inference(resolve,[status(thm)],[c_18654,c_1]) ).
cnf(c_93,plain,
product(A,add(B,C),add(multiply(A,B),multiply(A,C))),
inference(resolve,[status(thm)],[c_18655,c_1]) ).
cnf(c_18656,plain,
( product(A,C,E)
| ~ sum(A,D,E)
| ~ product(additive_identity,B,D)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_13,c_6]) ).
cnf(c_18657,plain,
( product(C,add(C,A),D)
| ~ sum(C,B,D)
| ~ product(additive_identity,A,B) ),
inference(resolve,[status(thm)],[c_18656,c_1]) ).
cnf(c_18658,plain,
( product(A,add(A,multiplicative_identity),B)
| ~ sum(A,additive_identity,B) ),
inference(resolve,[status(thm)],[c_18657,c_8]) ).
cnf(c_148,plain,
product(A,add(A,multiplicative_identity),A),
inference(resolve,[status(thm)],[c_18658,c_6]) ).
cnf(c_18659,plain,
( product(add(A,D),C,F)
| ~ sum(A,E,F)
| ~ product(D,B,E)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_13,c_1]) ).
cnf(c_18660,plain,
( product(add(C,A),C,D)
| ~ sum(C,B,D)
| ~ product(A,additive_identity,B) ),
inference(resolve,[status(thm)],[c_18659,c_6]) ).
cnf(c_18661,plain,
( product(add(A,multiplicative_identity),A,B)
| ~ sum(A,additive_identity,B) ),
inference(resolve,[status(thm)],[c_18660,c_7]) ).
cnf(c_158,plain,
product(add(A,multiplicative_identity),A,A),
inference(resolve,[status(thm)],[c_18661,c_6]) ).
cnf(c_18662,plain,
( product(B,C,E)
| ~ sum(D,B,E)
| ~ product(additive_identity,A,D)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_15,c_5]) ).
cnf(c_18663,plain,
( product(B,B,C)
| ~ sum(A,B,C)
| ~ product(additive_identity,additive_identity,A) ),
inference(resolve,[status(thm)],[c_18662,c_5]) ).
cnf(c_18664,plain,
( product(A,A,B)
| ~ sum(multiply(additive_identity,additive_identity),A,B) ),
inference(resolve,[status(thm)],[c_18663,c_2]) ).
cnf(c_195,plain,
product(A,A,add(multiply(additive_identity,additive_identity),A)),
inference(resolve,[status(thm)],[c_18664,c_1]) ).
cnf(c_18665,plain,
( product(B,C,E)
| ~ sum(D,B,E)
| ~ product(additive_identity,A,D)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_15,c_5]) ).
cnf(c_18666,plain,
( product(C,add(A,C),D)
| ~ sum(B,C,D)
| ~ product(additive_identity,A,B) ),
inference(resolve,[status(thm)],[c_18665,c_1]) ).
cnf(c_18667,plain,
( product(A,add(multiplicative_identity,A),B)
| ~ sum(additive_identity,A,B) ),
inference(resolve,[status(thm)],[c_18666,c_8]) ).
cnf(c_196,plain,
product(A,add(multiplicative_identity,A),A),
inference(resolve,[status(thm)],[c_18667,c_5]) ).
cnf(c_18668,plain,
( product(multiplicative_identity,C,E)
| ~ sum(D,B,E)
| ~ product(inverse(B),A,D)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_15,c_17]) ).
cnf(c_18669,plain,
( product(multiplicative_identity,add(B,A),D)
| ~ sum(C,A,D)
| ~ product(inverse(A),B,C) ),
inference(resolve,[status(thm)],[c_18668,c_1]) ).
cnf(c_18670,plain,
( product(multiplicative_identity,add(multiplicative_identity,A),B)
| ~ sum(inverse(A),A,B) ),
inference(resolve,[status(thm)],[c_18669,c_8]) ).
cnf(c_250,plain,
product(multiplicative_identity,add(multiplicative_identity,A),multiplicative_identity),
inference(resolve,[status(thm)],[c_18670,c_17]) ).
cnf(c_18671,plain,
( multiplicative_identity = B
| ~ sum(A,inverse(A),B) ),
inference(resolve,[status(thm)],[c_21,c_18]) ).
cnf(c_18672,plain,
multiplicative_identity = add(A,inverse(A)),
inference(resolve,[status(thm)],[c_18671,c_1]) ).
cnf(c_715,plain,
add(A,inverse(A)) = multiplicative_identity,
inference(copy,[status(thm)],[c_18672]) ).
cnf(c_18673,plain,
( A = B
| ~ sum(additive_identity,A,B) ),
inference(resolve,[status(thm)],[c_21,c_5]) ).
cnf(c_18674,plain,
A = add(additive_identity,A),
inference(resolve,[status(thm)],[c_18673,c_1]) ).
cnf(c_718,plain,
add(additive_identity,A) = A,
inference(copy,[status(thm)],[c_18674]) ).
cnf(c_18675,plain,
( additive_identity = B
| ~ product(A,inverse(A),B) ),
inference(resolve,[status(thm)],[c_22,c_20]) ).
cnf(c_18676,plain,
additive_identity = multiply(A,inverse(A)),
inference(resolve,[status(thm)],[c_18675,c_2]) ).
cnf(c_720,plain,
multiply(A,inverse(A)) = additive_identity,
inference(copy,[status(thm)],[c_18676]) ).
cnf(c_18677,plain,
( A = B
| ~ product(A,multiplicative_identity,B) ),
inference(resolve,[status(thm)],[c_22,c_8]) ).
cnf(c_18678,plain,
A = multiply(A,multiplicative_identity),
inference(resolve,[status(thm)],[c_18677,c_2]) ).
cnf(c_722,plain,
multiply(A,multiplicative_identity) = A,
inference(copy,[status(thm)],[c_18678]) ).
cnf(c_18679,plain,
( A = B
| ~ product(multiplicative_identity,A,B) ),
inference(resolve,[status(thm)],[c_22,c_7]) ).
cnf(c_18680,plain,
A = multiply(multiplicative_identity,A),
inference(resolve,[status(thm)],[c_18679,c_2]) ).
cnf(c_723,plain,
multiply(multiplicative_identity,A) = A,
inference(copy,[status(thm)],[c_18680]) ).
cnf(c_783,plain,
sum(y,x,x_plus_y),
inference(resolve,[status(thm)],[c_3,c_25]) ).
cnf(c_18681,plain,
( add(A,B) = C
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_21,c_1]) ).
cnf(c_854,plain,
add(A,B) = add(B,A),
inference(resolve,[status(thm)],[c_18681,c_28]) ).
cnf(c_18682,plain,
( multiply(A,B) = C
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_22,c_2]) ).
cnf(c_1090,plain,
multiply(A,B) = multiply(B,A),
inference(resolve,[status(thm)],[c_18682,c_29]) ).
cnf(c_18683,plain,
( A = B
| ~ sum(additive_identity,A,B) ),
inference(resolve,[status(thm)],[c_21,c_5]) ).
cnf(c_1408,plain,
multiply(additive_identity,additive_identity) = additive_identity,
inference(resolve,[status(thm)],[c_18683,c_33]) ).
cnf(c_18684,plain,
product(A,A,add(additive_identity,A)),
inference(paramod,[status(thm)],[c_1408,c_195]) ).
cnf(c_1545,plain,
product(A,A,A),
inference(paramod,[status(thm)],[c_718,c_18684]) ).
cnf(c_18685,plain,
( multiply(B,A) = C
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_22,c_29]) ).
cnf(c_1547,plain,
multiply(A,A) = A,
inference(resolve,[status(thm)],[c_18685,c_1545]) ).
cnf(c_18686,plain,
( product(A,E,F)
| ~ sum(multiply(D,A),C,F)
| ~ sum(D,B,E)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_10,c_29]) ).
cnf(c_18687,plain,
( product(B,C,D)
| ~ sum(multiply(A,B),B,D)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_18686,c_1545]) ).
cnf(c_18688,plain,
( product(x,x_plus_y,A)
| ~ sum(multiply(y,x),x,A) ),
inference(resolve,[status(thm)],[c_18687,c_783]) ).
cnf(c_18689,plain,
product(x,x_plus_y,add(x,multiply(y,x))),
inference(resolve,[status(thm)],[c_18688,c_28]) ).
cnf(c_1594,plain,
product(x,x_plus_y,add(x,multiply(x,y))),
inference(paramod,[status(thm)],[c_1090,c_18689]) ).
cnf(c_18690,plain,
( add(B,A) = C
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_21,c_28]) ).
cnf(c_18691,plain,
add(multiply(A,B),A) = multiply(A,add(multiplicative_identity,B)),
inference(resolve,[status(thm)],[c_18690,c_36]) ).
cnf(c_18692,plain,
add(A,multiply(A,B)) = multiply(A,add(multiplicative_identity,B)),
inference(paramod,[status(thm)],[c_854,c_18691]) ).
cnf(c_1661,plain,
multiply(A,add(multiplicative_identity,B)) = add(A,multiply(A,B)),
inference(copy,[status(thm)],[c_18692]) ).
cnf(c_18693,plain,
( add(B,A) = C
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_21,c_28]) ).
cnf(c_18694,plain,
add(A,multiply(A,B)) = multiply(A,add(B,multiplicative_identity)),
inference(resolve,[status(thm)],[c_18693,c_51]) ).
cnf(c_1889,plain,
multiply(A,add(B,multiplicative_identity)) = add(A,multiply(A,B)),
inference(copy,[status(thm)],[c_18694]) ).
cnf(c_18695,plain,
( multiply(B,A) = C
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_22,c_29]) ).
cnf(c_18696,plain,
multiply(add(A,multiplicative_identity),A) = A,
inference(resolve,[status(thm)],[c_18695,c_148]) ).
cnf(c_18697,plain,
multiply(A,add(A,multiplicative_identity)) = A,
inference(paramod,[status(thm)],[c_1090,c_18696]) ).
cnf(c_18698,plain,
add(A,multiply(A,A)) = A,
inference(paramod,[status(thm)],[c_1889,c_18697]) ).
cnf(c_1933,plain,
add(A,A) = A,
inference(paramod,[status(thm)],[c_1547,c_18698]) ).
cnf(c_18699,plain,
( sum(B,C,E)
| ~ product(D,add(B,multiplicative_identity),E)
| ~ sum(B,A,D)
| ~ product(A,add(B,multiplicative_identity),C) ),
inference(resolve,[status(thm)],[c_11,c_148]) ).
cnf(c_18700,plain,
( sum(A,A,C)
| ~ product(B,add(A,multiplicative_identity),C)
| ~ sum(A,A,B) ),
inference(resolve,[status(thm)],[c_18699,c_148]) ).
cnf(c_18701,plain,
( sum(A,A,B)
| ~ product(add(A,A),add(A,multiplicative_identity),B) ),
inference(resolve,[status(thm)],[c_18700,c_28]) ).
cnf(c_18702,plain,
sum(A,A,multiply(add(A,multiplicative_identity),add(A,A))),
inference(resolve,[status(thm)],[c_18701,c_29]) ).
cnf(c_18703,plain,
sum(A,A,multiply(add(A,multiplicative_identity),A)),
inference(paramod,[status(thm)],[c_1933,c_18702]) ).
cnf(c_18704,plain,
sum(A,A,multiply(A,add(A,multiplicative_identity))),
inference(paramod,[status(thm)],[c_1090,c_18703]) ).
cnf(c_18705,plain,
sum(A,A,add(A,multiply(A,A))),
inference(paramod,[status(thm)],[c_1889,c_18704]) ).
cnf(c_18706,plain,
sum(A,A,add(A,A)),
inference(paramod,[status(thm)],[c_1547,c_18705]) ).
cnf(c_2005,plain,
sum(A,A,A),
inference(paramod,[status(thm)],[c_1933,c_18706]) ).
cnf(c_18707,plain,
( sum(A,C,E)
| ~ product(A,D,E)
| ~ sum(add(A,multiplicative_identity),B,D)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_9,c_148]) ).
cnf(c_18708,plain,
( sum(inverse(x),x_inverse_times_y_inverse,B)
| ~ product(inverse(x),A,B)
| ~ sum(add(inverse(x),multiplicative_identity),inverse(y),A) ),
inference(resolve,[status(thm)],[c_18707,c_26]) ).
cnf(c_18709,plain,
( sum(inverse(x),x_inverse_times_y_inverse,A)
| ~ product(inverse(x),add(inverse(y),add(inverse(x),multiplicative_identity)),A) ),
inference(resolve,[status(thm)],[c_18708,c_28]) ).
cnf(c_18710,plain,
sum(inverse(x),x_inverse_times_y_inverse,multiply(add(inverse(y),add(inverse(x),multiplicative_identity)),inverse(x))),
inference(resolve,[status(thm)],[c_18709,c_29]) ).
cnf(c_18711,plain,
sum(inverse(x),x_inverse_times_y_inverse,multiply(add(inverse(y),add(multiplicative_identity,inverse(x))),inverse(x))),
inference(paramod,[status(thm)],[c_854,c_18710]) ).
cnf(c_18712,plain,
sum(inverse(x),x_inverse_times_y_inverse,multiply(add(add(multiplicative_identity,inverse(x)),inverse(y)),inverse(x))),
inference(paramod,[status(thm)],[c_854,c_18711]) ).
cnf(c_2065,plain,
sum(inverse(x),x_inverse_times_y_inverse,multiply(inverse(x),add(add(multiplicative_identity,inverse(x)),inverse(y)))),
inference(paramod,[status(thm)],[c_1090,c_18712]) ).
cnf(c_18713,plain,
( sum(B,C,E)
| ~ product(D,B,E)
| ~ sum(add(B,multiplicative_identity),A,D)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_11,c_158]) ).
cnf(c_18714,plain,
( sum(inverse(y),x_inverse_times_y_inverse,B)
| ~ product(A,inverse(y),B)
| ~ sum(add(inverse(y),multiplicative_identity),inverse(x),A) ),
inference(resolve,[status(thm)],[c_18713,c_26]) ).
cnf(c_18715,plain,
( sum(inverse(y),x_inverse_times_y_inverse,A)
| ~ product(add(inverse(x),add(inverse(y),multiplicative_identity)),inverse(y),A) ),
inference(resolve,[status(thm)],[c_18714,c_28]) ).
cnf(c_18716,plain,
sum(inverse(y),x_inverse_times_y_inverse,multiply(inverse(y),add(inverse(x),add(inverse(y),multiplicative_identity)))),
inference(resolve,[status(thm)],[c_18715,c_29]) ).
cnf(c_2133,plain,
sum(inverse(y),x_inverse_times_y_inverse,multiply(inverse(y),add(inverse(x),add(multiplicative_identity,inverse(y))))),
inference(paramod,[status(thm)],[c_854,c_18716]) ).
cnf(c_18717,plain,
( sum(A,C,E)
| ~ product(A,D,E)
| ~ sum(add(multiplicative_identity,A),B,D)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_9,c_196]) ).
cnf(c_18718,plain,
( sum(A,multiply(A,B),D)
| ~ product(A,C,D)
| ~ sum(add(multiplicative_identity,A),B,C) ),
inference(resolve,[status(thm)],[c_18717,c_2]) ).
cnf(c_18719,plain,
( sum(A,multiply(A,B),C)
| ~ product(A,add(add(multiplicative_identity,A),B),C) ),
inference(resolve,[status(thm)],[c_18718,c_1]) ).
cnf(c_18720,plain,
sum(A,multiply(A,B),multiply(add(add(multiplicative_identity,A),B),A)),
inference(resolve,[status(thm)],[c_18719,c_29]) ).
cnf(c_2444,plain,
sum(A,multiply(A,B),multiply(A,add(add(multiplicative_identity,A),B))),
inference(paramod,[status(thm)],[c_1090,c_18720]) ).
cnf(c_18721,plain,
( multiply(B,A) = C
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_22,c_29]) ).
cnf(c_18722,plain,
multiply(add(multiplicative_identity,A),multiplicative_identity) = multiplicative_identity,
inference(resolve,[status(thm)],[c_18721,c_250]) ).
cnf(c_18723,plain,
multiply(multiplicative_identity,add(multiplicative_identity,A)) = multiplicative_identity,
inference(paramod,[status(thm)],[c_1090,c_18722]) ).
cnf(c_18724,plain,
add(multiplicative_identity,multiply(multiplicative_identity,A)) = multiplicative_identity,
inference(paramod,[status(thm)],[c_1661,c_18723]) ).
cnf(c_2477,plain,
add(multiplicative_identity,A) = multiplicative_identity,
inference(paramod,[status(thm)],[c_723,c_18724]) ).
cnf(c_18725,plain,
sum(A,multiply(A,B),multiply(A,add(multiplicative_identity,B))),
inference(paramod,[status(thm)],[c_2477,c_2444]) ).
cnf(c_18726,plain,
sum(A,multiply(A,B),multiply(A,multiplicative_identity)),
inference(paramod,[status(thm)],[c_2477,c_18725]) ).
cnf(c_2486,plain,
sum(A,multiply(A,B),A),
inference(paramod,[status(thm)],[c_722,c_18726]) ).
cnf(c_18727,plain,
sum(inverse(y),x_inverse_times_y_inverse,multiply(inverse(y),add(inverse(x),multiplicative_identity))),
inference(paramod,[status(thm)],[c_2477,c_2133]) ).
cnf(c_18728,plain,
sum(inverse(y),x_inverse_times_y_inverse,multiply(inverse(y),add(multiplicative_identity,inverse(x)))),
inference(paramod,[status(thm)],[c_854,c_18727]) ).
cnf(c_18729,plain,
sum(inverse(y),x_inverse_times_y_inverse,multiply(inverse(y),multiplicative_identity)),
inference(paramod,[status(thm)],[c_2477,c_18728]) ).
cnf(c_18730,plain,
sum(inverse(y),x_inverse_times_y_inverse,multiply(multiplicative_identity,inverse(y))),
inference(paramod,[status(thm)],[c_1090,c_18729]) ).
cnf(c_2514,plain,
sum(inverse(y),x_inverse_times_y_inverse,inverse(y)),
inference(paramod,[status(thm)],[c_723,c_18730]) ).
cnf(c_18731,plain,
sum(inverse(x),x_inverse_times_y_inverse,multiply(inverse(x),add(multiplicative_identity,inverse(y)))),
inference(paramod,[status(thm)],[c_2477,c_2065]) ).
cnf(c_18732,plain,
sum(inverse(x),x_inverse_times_y_inverse,multiply(inverse(x),multiplicative_identity)),
inference(paramod,[status(thm)],[c_2477,c_18731]) ).
cnf(c_18733,plain,
sum(inverse(x),x_inverse_times_y_inverse,multiply(multiplicative_identity,inverse(x))),
inference(paramod,[status(thm)],[c_1090,c_18732]) ).
cnf(c_2517,plain,
sum(inverse(x),x_inverse_times_y_inverse,inverse(x)),
inference(paramod,[status(thm)],[c_723,c_18733]) ).
cnf(c_18734,plain,
multiply(A,multiplicative_identity) = add(A,multiply(A,B)),
inference(paramod,[status(thm)],[c_2477,c_1661]) ).
cnf(c_18735,plain,
A = add(A,multiply(A,B)),
inference(paramod,[status(thm)],[c_722,c_18734]) ).
cnf(c_2531,plain,
add(A,multiply(A,B)) = A,
inference(copy,[status(thm)],[c_18735]) ).
cnf(c_2547,plain,
product(x,x_plus_y,x),
inference(paramod,[status(thm)],[c_2531,c_1594]) ).
cnf(c_18736,plain,
( product(add(B,D),C,F)
| ~ sum(E,B,F)
| ~ product(D,A,E)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_15,c_28]) ).
cnf(c_18737,plain,
( product(add(D,A),add(D,B),E)
| ~ sum(C,D,E)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_18736,c_28]) ).
cnf(c_18738,plain,
( product(add(A,x),add(A,x_plus_y),B)
| ~ sum(x,A,B) ),
inference(resolve,[status(thm)],[c_18737,c_2547]) ).
cnf(c_18739,plain,
product(add(inverse(x),x),add(inverse(x),x_plus_y),multiplicative_identity),
inference(resolve,[status(thm)],[c_18738,c_18]) ).
cnf(c_18740,plain,
product(add(x,inverse(x)),add(inverse(x),x_plus_y),multiplicative_identity),
inference(paramod,[status(thm)],[c_854,c_18739]) ).
cnf(c_18741,plain,
product(multiplicative_identity,add(inverse(x),x_plus_y),multiplicative_identity),
inference(paramod,[status(thm)],[c_715,c_18740]) ).
cnf(c_2640,plain,
product(multiplicative_identity,add(x_plus_y,inverse(x)),multiplicative_identity),
inference(paramod,[status(thm)],[c_854,c_18741]) ).
cnf(c_18742,plain,
( product(A,C,E)
| ~ sum(A,D,E)
| ~ product(A,B,D)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_13,c_2005]) ).
cnf(c_18743,plain,
( product(y,x_plus_y,B)
| ~ sum(y,A,B)
| ~ product(y,x,A) ),
inference(resolve,[status(thm)],[c_18742,c_783]) ).
cnf(c_18744,plain,
( product(y,x_plus_y,A)
| ~ sum(y,multiply(y,x),A) ),
inference(resolve,[status(thm)],[c_18743,c_2]) ).
cnf(c_3720,plain,
product(y,x_plus_y,y),
inference(resolve,[status(thm)],[c_18744,c_2486]) ).
cnf(c_18745,plain,
( product(add(B,D),C,F)
| ~ sum(E,B,F)
| ~ product(D,A,E)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_15,c_28]) ).
cnf(c_18746,plain,
( product(add(D,A),add(D,B),E)
| ~ sum(C,D,E)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_18745,c_28]) ).
cnf(c_18747,plain,
( product(add(A,y),add(A,x_plus_y),B)
| ~ sum(y,A,B) ),
inference(resolve,[status(thm)],[c_18746,c_3720]) ).
cnf(c_18748,plain,
product(add(inverse(y),y),add(inverse(y),x_plus_y),multiplicative_identity),
inference(resolve,[status(thm)],[c_18747,c_18]) ).
cnf(c_18749,plain,
product(add(y,inverse(y)),add(inverse(y),x_plus_y),multiplicative_identity),
inference(paramod,[status(thm)],[c_854,c_18748]) ).
cnf(c_18750,plain,
product(multiplicative_identity,add(inverse(y),x_plus_y),multiplicative_identity),
inference(paramod,[status(thm)],[c_715,c_18749]) ).
cnf(c_3889,plain,
product(multiplicative_identity,add(x_plus_y,inverse(y)),multiplicative_identity),
inference(paramod,[status(thm)],[c_854,c_18750]) ).
cnf(c_18751,plain,
( sum(multiply(B,D),C,F)
| ~ product(E,B,F)
| ~ sum(D,A,E)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_11,c_29]) ).
cnf(c_18752,plain,
( sum(multiply(D,A),multiply(D,B),E)
| ~ product(C,D,E)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_18751,c_29]) ).
cnf(c_18753,plain,
( sum(multiply(A,inverse(y)),multiply(A,x_inverse_times_y_inverse),B)
| ~ product(inverse(y),A,B) ),
inference(resolve,[status(thm)],[c_18752,c_2514]) ).
cnf(c_18754,plain,
sum(multiply(inverse(inverse(y)),inverse(y)),multiply(inverse(inverse(y)),x_inverse_times_y_inverse),additive_identity),
inference(resolve,[status(thm)],[c_18753,c_20]) ).
cnf(c_18755,plain,
sum(multiply(y,inverse(y)),multiply(inverse(inverse(y)),x_inverse_times_y_inverse),additive_identity),
inference(paramod,[status(thm)],[c_23,c_18754]) ).
cnf(c_18756,plain,
sum(additive_identity,multiply(inverse(inverse(y)),x_inverse_times_y_inverse),additive_identity),
inference(paramod,[status(thm)],[c_720,c_18755]) ).
cnf(c_6850,plain,
sum(additive_identity,multiply(y,x_inverse_times_y_inverse),additive_identity),
inference(paramod,[status(thm)],[c_23,c_18756]) ).
cnf(c_18757,plain,
( sum(multiply(B,D),C,F)
| ~ product(E,B,F)
| ~ sum(D,A,E)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_11,c_29]) ).
cnf(c_18758,plain,
( sum(multiply(D,A),multiply(D,B),E)
| ~ product(C,D,E)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_18757,c_29]) ).
cnf(c_18759,plain,
( sum(multiply(A,inverse(x)),multiply(A,x_inverse_times_y_inverse),B)
| ~ product(inverse(x),A,B) ),
inference(resolve,[status(thm)],[c_18758,c_2517]) ).
cnf(c_18760,plain,
sum(multiply(inverse(inverse(x)),inverse(x)),multiply(inverse(inverse(x)),x_inverse_times_y_inverse),additive_identity),
inference(resolve,[status(thm)],[c_18759,c_20]) ).
cnf(c_18761,plain,
sum(multiply(x,inverse(x)),multiply(inverse(inverse(x)),x_inverse_times_y_inverse),additive_identity),
inference(paramod,[status(thm)],[c_23,c_18760]) ).
cnf(c_18762,plain,
sum(additive_identity,multiply(inverse(inverse(x)),x_inverse_times_y_inverse),additive_identity),
inference(paramod,[status(thm)],[c_720,c_18761]) ).
cnf(c_7851,plain,
sum(additive_identity,multiply(x,x_inverse_times_y_inverse),additive_identity),
inference(paramod,[status(thm)],[c_23,c_18762]) ).
cnf(c_18763,plain,
( product(add(D,A),C,F)
| ~ sum(A,E,F)
| ~ product(D,B,E)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_13,c_28]) ).
cnf(c_18764,plain,
( product(add(A,D),add(B,D),E)
| ~ sum(D,C,E)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_18763,c_28]) ).
cnf(c_18765,plain,
( product(add(B,A),add(C,A),D)
| ~ sum(A,multiply(B,C),D) ),
inference(resolve,[status(thm)],[c_18764,c_2]) ).
cnf(c_18766,plain,
product(add(y,additive_identity),add(x_inverse_times_y_inverse,additive_identity),additive_identity),
inference(resolve,[status(thm)],[c_18765,c_6850]) ).
cnf(c_18767,plain,
product(add(additive_identity,y),add(x_inverse_times_y_inverse,additive_identity),additive_identity),
inference(paramod,[status(thm)],[c_854,c_18766]) ).
cnf(c_18768,plain,
product(y,add(x_inverse_times_y_inverse,additive_identity),additive_identity),
inference(paramod,[status(thm)],[c_718,c_18767]) ).
cnf(c_18769,plain,
product(y,add(additive_identity,x_inverse_times_y_inverse),additive_identity),
inference(paramod,[status(thm)],[c_854,c_18768]) ).
cnf(c_14703,plain,
product(y,x_inverse_times_y_inverse,additive_identity),
inference(paramod,[status(thm)],[c_718,c_18769]) ).
cnf(c_18770,plain,
( product(C,x_inverse_times_y_inverse,D)
| ~ sum(additive_identity,B,D)
| ~ sum(y,A,C)
| ~ product(A,x_inverse_times_y_inverse,B) ),
inference(resolve,[status(thm)],[c_12,c_14703]) ).
cnf(c_18771,plain,
( product(B,x_inverse_times_y_inverse,C)
| ~ sum(additive_identity,multiply(A,x_inverse_times_y_inverse),C)
| ~ sum(y,A,B) ),
inference(resolve,[status(thm)],[c_18770,c_2]) ).
cnf(c_18772,plain,
( product(x_plus_y,x_inverse_times_y_inverse,A)
| ~ sum(additive_identity,multiply(x,x_inverse_times_y_inverse),A) ),
inference(resolve,[status(thm)],[c_18771,c_783]) ).
cnf(c_15111,plain,
product(x_plus_y,x_inverse_times_y_inverse,additive_identity),
inference(resolve,[status(thm)],[c_18772,c_7851]) ).
cnf(c_18773,plain,
( inverse(A) = B
| ~ product(A,B,additive_identity)
| ~ product(A,inverse(A),additive_identity)
| ~ sum(A,B,multiplicative_identity) ),
inference(resolve,[status(thm)],[c_24,c_18]) ).
cnf(c_18774,plain,
( inverse(A) = B
| ~ product(A,B,additive_identity)
| ~ sum(A,B,multiplicative_identity) ),
inference(resolve,[status(thm)],[c_18773,c_20]) ).
cnf(c_18775,plain,
( inverse(x_plus_y) = x_inverse_times_y_inverse
| ~ sum(x_plus_y,x_inverse_times_y_inverse,multiplicative_identity) ),
inference(resolve,[status(thm)],[c_18774,c_15111]) ).
cnf(c_15443,plain,
~ sum(x_plus_y,x_inverse_times_y_inverse,multiplicative_identity),
inference(resolve,[status(thm)],[c_18775,c_27]) ).
cnf(c_18776,plain,
( sum(A,E,F)
| ~ product(add(D,A),C,F)
| ~ product(D,B,E)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_14,c_28]) ).
cnf(c_18777,plain,
( sum(D,C,E)
| ~ product(add(A,D),add(B,D),E)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_18776,c_28]) ).
cnf(c_18778,plain,
( sum(A,x_inverse_times_y_inverse,B)
| ~ product(add(inverse(x),A),add(inverse(y),A),B) ),
inference(resolve,[status(thm)],[c_18777,c_26]) ).
cnf(c_18779,plain,
~ product(add(inverse(x),x_plus_y),add(inverse(y),x_plus_y),multiplicative_identity),
inference(resolve,[status(thm)],[c_18778,c_15443]) ).
cnf(c_18780,plain,
~ product(add(x_plus_y,inverse(x)),add(inverse(y),x_plus_y),multiplicative_identity),
inference(paramod,[status(thm)],[c_854,c_18779]) ).
cnf(c_17684,plain,
~ product(add(x_plus_y,inverse(x)),add(x_plus_y,inverse(y)),multiplicative_identity),
inference(paramod,[status(thm)],[c_854,c_18780]) ).
cnf(c_18781,plain,
( add(multiply(A,B),multiply(A,C)) = D
| ~ product(A,add(B,C),D) ),
inference(resolve,[status(thm)],[c_22,c_93]) ).
cnf(c_18782,plain,
add(multiply(multiplicative_identity,x_plus_y),multiply(multiplicative_identity,inverse(x))) = multiplicative_identity,
inference(resolve,[status(thm)],[c_18781,c_2640]) ).
cnf(c_18783,plain,
add(x_plus_y,multiply(multiplicative_identity,inverse(x))) = multiplicative_identity,
inference(paramod,[status(thm)],[c_723,c_18782]) ).
cnf(c_18605,plain,
add(x_plus_y,inverse(x)) = multiplicative_identity,
inference(paramod,[status(thm)],[c_723,c_18783]) ).
cnf(c_18642,plain,
~ product(multiplicative_identity,add(x_plus_y,inverse(y)),multiplicative_identity),
inference(paramod,[status(thm)],[c_18605,c_17684]) ).
cnf(c_18643,plain,
$false,
inference(resolve,[status(thm)],[c_18642,c_3889]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : BOO014-3 : TPTP v9.3.1. Bugfixed v2.2.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n013.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Sat Sep 26 22:35:37 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.19/0.45 % Process 3710639 was started by sandbox on n013,
% 0.19/0.45 % Sat Sep 26 22:35:37 2026
% 0.19/0.45 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.19/0.46
% 0.19/0.46 % From the command line: assign(max_seconds, 300).
% 260.66/33.48
% 260.66/33.48 % SZS status Unsatisfiable for theBenchmark
% 260.66/33.48
% 260.66/33.48 % Proof 1 at 24.66 (+ 7.63) seconds.
% 260.66/33.48 % Length of proof is 73.
% 260.66/33.48 % Level of proof is 12.
% 260.66/33.48 % Maximum clause weight is 20.000.
% 260.66/33.48 % Given clauses 270.
% 260.66/33.48
% 260.66/33.48 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------