%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : BOO015-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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 : Thu Sep 24 12:06:45 PM UTC 2026
% Result : Unsatisfiable 265.86s 39.00s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO015-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/5.37 % Computer : n018.cluster.edu
% 0.12/5.37 % Model : x86_64 x86_64
% 0.12/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.37 % Memory : 8046.5625MB
% 0.12/5.37 % OS : Linux 6.8.0-71-generic
% 0.12/5.38 % CPULimit : 300
% 0.12/5.38 % WCLimit : 300
% 0.12/5.38 % DateTime : Mon Sep 21 13:50:21 UTC 2026
% 0.12/5.38 % CPUTime :
% 0.12/5.39 % Drodi V4.1.1
% 265.86/39.00 % Refutation found
% 265.86/39.00 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 265.86/39.00 % SZS output start CNFRefutation for theBenchmark
% 265.86/39.00 fof(f1,axiom,(
% 265.86/39.00 (![X,Y]: (sum(X,Y,add(X,Y)) ))),
% 265.86/39.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 265.86/39.00 fof(f2,axiom,(
% 265.86/39.00 (![X,Y]: (product(X,Y,multiply(X,Y)) ))),
% 265.86/39.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 265.86/39.00 fof(f3,axiom,(
% 265.86/39.00 (![X,Y,Z]: (( ~ sum(X,Y,Z)| sum(Y,X,Z) ) ))),
% 265.86/39.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 265.86/39.00 fof(f4,axiom,(
% 265.86/39.00 (![X,Y,Z]: (( ~ product(X,Y,Z)| product(Y,X,Z) ) ))),
% 265.86/39.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 265.86/39.00 fof(f5,axiom,(
% 265.86/39.00 (![X]: (sum(additive_identity,X,X) ))),
% 265.86/39.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 265.86/39.00 fof(f6,axiom,(
% 265.86/39.00 (![X]: (sum(X,additive_identity,X) ))),
% 265.86/39.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 265.86/39.00 fof(f7,axiom,(
% 265.86/39.00 (![X]: (product(multiplicative_identity,X,X) ))),
% 265.86/39.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 265.86/39.00 fof(f8,axiom,(
% 265.86/39.00 (![X]: (product(X,multiplicative_identity,X) ))),
% 265.86/39.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 265.86/39.00 fof(f9,axiom,(
% 265.86/39.00 (![X,Y,V1,Z,V2,V3,V4]: (( ~ product(X,Y,V1)| ~ product(X,Z,V2)| ~ sum(Y,Z,V3)| ~ product(X,V3,V4)| sum(V1,V2,V4) ) ))),
% 265.86/39.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 265.86/39.00 fof(f10,axiom,(
% 265.86/39.00 (![X,Y,V1,Z,V2,V3,V4]: (( ~ product(X,Y,V1)| ~ product(X,Z,V2)| ~ sum(Y,Z,V3)| ~ sum(V1,V2,V4)| product(X,V3,V4) ) ))),
% 265.86/39.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 265.86/39.00 fof(f11,axiom,(
% 265.86/39.00 (![Y,X,V1,Z,V2,V3,V4]: (( ~ product(Y,X,V1)| ~ product(Z,X,V2)| ~ sum(Y,Z,V3)| ~ product(V3,X,V4)| sum(V1,V2,V4) ) ))),
% 265.86/39.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 265.86/39.00 fof(f12,axiom,(
% 265.86/39.00 (![Y,X,V1,Z,V2,V3,V4]: (( ~ product(Y,X,V1)| ~ product(Z,X,V2)| ~ sum(Y,Z,V3)| ~ sum(V1,V2,V4)| product(V3,X,V4) ) ))),
% 265.86/39.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 265.86/39.00 fof(f13,axiom,(
% 265.86/39.00 (![X,Y,V1,Z,V2,V3,V4]: (( ~ sum(X,Y,V1)| ~ sum(X,Z,V2)| ~ product(Y,Z,V3)| ~ sum(X,V3,V4)| product(V1,V2,V4) ) ))),
% 265.86/39.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 265.86/39.00 fof(f14,axiom,(
% 265.86/39.00 (![X,Y,V1,Z,V2,V3,V4]: (( ~ sum(X,Y,V1)| ~ sum(X,Z,V2)| ~ product(Y,Z,V3)| ~ product(V1,V2,V4)| sum(X,V3,V4) ) ))),
% 265.86/39.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 265.86/39.00 fof(f17,axiom,(
% 265.86/39.00 (![X]: (sum(inverse(X),X,multiplicative_identity) ))),
% 265.86/39.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 265.86/39.00 fof(f18,axiom,(
% 265.86/39.00 (![X]: (sum(X,inverse(X),multiplicative_identity) ))),
% 265.86/39.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 265.86/39.00 fof(f19,axiom,(
% 265.86/39.00 (![X]: (product(inverse(X),X,additive_identity) ))),
% 265.86/39.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 265.86/39.00 fof(f20,axiom,(
% 265.86/39.00 (![X]: (product(X,inverse(X),additive_identity) ))),
% 265.86/39.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 265.86/39.00 fof(f21,axiom,(
% 265.86/39.00 (![X,Y,U,V]: (( ~ sum(X,Y,U)| ~ sum(X,Y,V)| U = V ) ))),
% 265.86/39.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 265.86/39.00 fof(f22,axiom,(
% 265.86/39.00 (![X,Y,U,V]: (( ~ product(X,Y,U)| ~ product(X,Y,V)| U = V ) ))),
% 265.86/39.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 265.86/39.00 fof(f23,negated_conjecture,(
% 265.86/39.00 product(x,y,x_times_y) ),
% 265.86/39.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 265.86/39.00 fof(f24,negated_conjecture,(
% 265.86/39.00 sum(inverse(x),inverse(y),x_inverse_plus_y_inverse) ),
% 265.86/39.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 265.86/39.00 fof(f25,negated_conjecture,(
% 265.86/39.00 inverse(x_times_y) != x_inverse_plus_y_inverse ),
% 265.86/39.00 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 265.86/39.00 fof(f26,plain,(
% 265.86/39.00 ![X0,X1]: (sum(X0,X1,add(X0,X1)))),
% 265.86/39.00 inference(cnf_transformation,[status(thm)],[f1])).
% 265.86/39.00 fof(f27,plain,(
% 265.86/39.00 ![X0,X1]: (product(X0,X1,multiply(X0,X1)))),
% 265.86/39.00 inference(cnf_transformation,[status(thm)],[f2])).
% 265.86/39.00 fof(f28,plain,(
% 265.86/39.00 ![X0,X1,X2]: (~sum(X0,X1,X2)|sum(X1,X0,X2))),
% 265.86/39.00 inference(cnf_transformation,[status(thm)],[f3])).
% 265.86/39.00 fof(f29,plain,(
% 265.86/39.00 ![X0,X1,X2]: (~product(X0,X1,X2)|product(X1,X0,X2))),
% 265.86/39.00 inference(cnf_transformation,[status(thm)],[f4])).
% 265.86/39.00 fof(f30,plain,(
% 265.86/39.00 ![X0]: (sum(additive_identity,X0,X0))),
% 265.86/39.00 inference(cnf_transformation,[status(thm)],[f5])).
% 265.86/39.01 fof(f31,plain,(
% 265.86/39.01 ![X0]: (sum(X0,additive_identity,X0))),
% 265.86/39.01 inference(cnf_transformation,[status(thm)],[f6])).
% 265.86/39.01 fof(f32,plain,(
% 265.86/39.01 ![X0]: (product(multiplicative_identity,X0,X0))),
% 265.86/39.01 inference(cnf_transformation,[status(thm)],[f7])).
% 265.86/39.01 fof(f33,plain,(
% 265.86/39.01 ![X0]: (product(X0,multiplicative_identity,X0))),
% 265.86/39.01 inference(cnf_transformation,[status(thm)],[f8])).
% 265.86/39.01 fof(f34,plain,(
% 265.86/39.01 ![V1,V2,V4]: ((![X,V3]: ((![Y,Z]: ((~product(X,Y,V1)|~product(X,Z,V2))|~sum(Y,Z,V3)))|~product(X,V3,V4)))|sum(V1,V2,V4))),
% 265.86/39.01 inference(miniscoping,[status(thm)],[f9])).
% 265.86/39.01 fof(f35,plain,(
% 265.86/39.01 ![X0,X1,X2,X3,X4,X5,X6]: (~product(X0,X1,X2)|~product(X0,X3,X4)|~sum(X1,X3,X5)|~product(X0,X5,X6)|sum(X2,X4,X6))),
% 265.86/39.01 inference(cnf_transformation,[status(thm)],[f34])).
% 265.86/39.01 fof(f36,plain,(
% 265.86/39.01 ![X,V3,V4]: ((![V1,V2]: ((![Y,Z]: ((~product(X,Y,V1)|~product(X,Z,V2))|~sum(Y,Z,V3)))|~sum(V1,V2,V4)))|product(X,V3,V4))),
% 265.86/39.01 inference(miniscoping,[status(thm)],[f10])).
% 265.86/39.01 fof(f37,plain,(
% 265.86/39.01 ![X0,X1,X2,X3,X4,X5,X6]: (~product(X0,X1,X2)|~product(X0,X3,X4)|~sum(X1,X3,X5)|~sum(X2,X4,X6)|product(X0,X5,X6))),
% 265.86/39.01 inference(cnf_transformation,[status(thm)],[f36])).
% 265.86/39.01 fof(f38,plain,(
% 265.86/39.01 ![V1,V2,V4]: ((![X,V3]: ((![Y,Z]: ((~product(Y,X,V1)|~product(Z,X,V2))|~sum(Y,Z,V3)))|~product(V3,X,V4)))|sum(V1,V2,V4))),
% 265.86/39.01 inference(miniscoping,[status(thm)],[f11])).
% 265.86/39.01 fof(f39,plain,(
% 265.86/39.01 ![X0,X1,X2,X3,X4,X5,X6]: (~product(X0,X1,X2)|~product(X3,X1,X4)|~sum(X0,X3,X5)|~product(X5,X1,X6)|sum(X2,X4,X6))),
% 265.86/39.01 inference(cnf_transformation,[status(thm)],[f38])).
% 265.86/39.01 fof(f40,plain,(
% 265.86/39.01 ![X,V3,V4]: ((![V1,V2]: ((![Y,Z]: ((~product(Y,X,V1)|~product(Z,X,V2))|~sum(Y,Z,V3)))|~sum(V1,V2,V4)))|product(V3,X,V4))),
% 265.86/39.01 inference(miniscoping,[status(thm)],[f12])).
% 265.86/39.01 fof(f41,plain,(
% 265.86/39.01 ![X0,X1,X2,X3,X4,X5,X6]: (~product(X0,X1,X2)|~product(X3,X1,X4)|~sum(X0,X3,X5)|~sum(X2,X4,X6)|product(X5,X1,X6))),
% 265.86/39.01 inference(cnf_transformation,[status(thm)],[f40])).
% 265.86/39.01 fof(f42,plain,(
% 265.86/39.01 ![V1,V2,V4]: ((![X,V3]: ((![Y,Z]: ((~sum(X,Y,V1)|~sum(X,Z,V2))|~product(Y,Z,V3)))|~sum(X,V3,V4)))|product(V1,V2,V4))),
% 265.86/39.01 inference(miniscoping,[status(thm)],[f13])).
% 265.86/39.01 fof(f43,plain,(
% 265.86/39.01 ![X0,X1,X2,X3,X4,X5,X6]: (~sum(X0,X1,X2)|~sum(X0,X3,X4)|~product(X1,X3,X5)|~sum(X0,X5,X6)|product(X2,X4,X6))),
% 265.86/39.01 inference(cnf_transformation,[status(thm)],[f42])).
% 265.86/39.01 fof(f44,plain,(
% 265.86/39.01 ![X,V3,V4]: ((![V1,V2]: ((![Y,Z]: ((~sum(X,Y,V1)|~sum(X,Z,V2))|~product(Y,Z,V3)))|~product(V1,V2,V4)))|sum(X,V3,V4))),
% 265.86/39.01 inference(miniscoping,[status(thm)],[f14])).
% 265.86/39.01 fof(f45,plain,(
% 265.86/39.01 ![X0,X1,X2,X3,X4,X5,X6]: (~sum(X0,X1,X2)|~sum(X0,X3,X4)|~product(X1,X3,X5)|~product(X2,X4,X6)|sum(X0,X5,X6))),
% 265.86/39.01 inference(cnf_transformation,[status(thm)],[f44])).
% 265.86/39.01 fof(f50,plain,(
% 265.86/39.01 ![X0]: (sum(inverse(X0),X0,multiplicative_identity))),
% 265.86/39.01 inference(cnf_transformation,[status(thm)],[f17])).
% 265.86/39.01 fof(f51,plain,(
% 265.86/39.01 ![X0]: (sum(X0,inverse(X0),multiplicative_identity))),
% 265.86/39.01 inference(cnf_transformation,[status(thm)],[f18])).
% 265.86/39.01 fof(f52,plain,(
% 265.86/39.01 ![X0]: (product(inverse(X0),X0,additive_identity))),
% 265.86/39.01 inference(cnf_transformation,[status(thm)],[f19])).
% 265.86/39.01 fof(f53,plain,(
% 265.86/39.01 ![X0]: (product(X0,inverse(X0),additive_identity))),
% 265.86/39.01 inference(cnf_transformation,[status(thm)],[f20])).
% 265.86/39.01 fof(f54,plain,(
% 265.86/39.01 ![U,V]: ((![X,Y]: (~sum(X,Y,U)|~sum(X,Y,V)))|U=V)),
% 265.86/39.01 inference(miniscoping,[status(thm)],[f21])).
% 265.86/39.01 fof(f55,plain,(
% 265.86/39.01 ![X0,X1,X2,X3]: (~sum(X0,X1,X2)|~sum(X0,X1,X3)|X2=X3)),
% 265.86/39.01 inference(cnf_transformation,[status(thm)],[f54])).
% 265.86/39.01 fof(f56,plain,(
% 265.86/39.01 ![U,V]: ((![X,Y]: (~product(X,Y,U)|~product(X,Y,V)))|U=V)),
% 265.86/39.01 inference(miniscoping,[status(thm)],[f22])).
% 265.86/39.01 fof(f57,plain,(
% 265.86/39.01 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(X0,X1,X3)|X2=X3)),
% 265.86/39.01 inference(cnf_transformation,[status(thm)],[f56])).
% 265.86/39.01 fof(f58,plain,(
% 265.86/39.01 product(x,y,x_times_y)),
% 265.86/39.01 inference(cnf_transformation,[status(thm)],[f23])).
% 265.86/39.01 fof(f59,plain,(
% 265.86/39.01 sum(inverse(x),inverse(y),x_inverse_plus_y_inverse)),
% 265.86/39.01 inference(cnf_transformation,[status(thm)],[f24])).
% 265.86/39.01 fof(f60,plain,(
% 265.86/39.01 ~inverse(x_times_y)=x_inverse_plus_y_inverse),
% 265.86/39.01 inference(cnf_transformation,[status(thm)],[f25])).
% 265.86/39.01 fof(f61,plain,(
% 265.86/39.01 sum(inverse(y),inverse(x),x_inverse_plus_y_inverse)),
% 265.86/39.01 inference(resolution,[status(thm)],[f28,f59])).
% 265.86/39.01 fof(f62,plain,(
% 265.86/39.01 product(y,x,x_times_y)),
% 265.86/39.01 inference(resolution,[status(thm)],[f29,f58])).
% 265.86/39.01 fof(f64,plain,(
% 265.86/39.01 ![X0]: (~sum(inverse(x),inverse(y),X0)|x_inverse_plus_y_inverse=X0)),
% 265.86/39.01 inference(resolution,[status(thm)],[f55,f59])).
% 265.86/39.01 fof(f66,plain,(
% 265.86/39.01 ![X0,X1,X2,X3]: (~product(x,X0,X1)|~sum(y,X0,X2)|~product(x,X2,X3)|sum(x_times_y,X1,X3))),
% 265.86/39.01 inference(resolution,[status(thm)],[f35,f58])).
% 265.86/39.01 fof(f69,plain,(
% 265.86/39.01 ![X0,X1]: (~sum(additive_identity,X0,X1)|X0=X1)),
% 265.86/39.01 inference(resolution,[status(thm)],[f30,f55])).
% 265.86/39.01 fof(f71,plain,(
% 265.86/39.01 ![X0,X1]: (~sum(X0,additive_identity,X1)|X0=X1)),
% 265.86/39.01 inference(resolution,[status(thm)],[f31,f55])).
% 265.86/39.01 fof(f76,plain,(
% 265.86/39.01 ![X0,X1,X2,X3,X4]: (~product(X0,X1,X2)|~sum(multiplicative_identity,X1,X3)|~sum(X0,X2,X4)|product(X0,X3,X4))),
% 265.86/39.01 inference(resolution,[status(thm)],[f33,f37])).
% 265.86/39.01 fof(f77,plain,(
% 265.86/39.01 ![X0,X1,X2,X3,X4]: (~product(X0,X1,X2)|~sum(multiplicative_identity,X1,X3)|~product(X0,X3,X4)|sum(X0,X2,X4))),
% 265.86/39.01 inference(resolution,[status(thm)],[f33,f35])).
% 265.86/39.01 fof(f79,plain,(
% 265.86/39.01 ![X0,X1,X2]: (~sum(X0,X1,X2)|add(X0,X1)=X2)),
% 265.86/39.01 inference(resolution,[status(thm)],[f26,f55])).
% 265.86/39.01 fof(f80,plain,(
% 265.86/39.01 ![X0,X1]: (sum(X0,X1,add(X1,X0)))),
% 265.86/39.01 inference(resolution,[status(thm)],[f26,f28])).
% 265.86/39.01 fof(f81,plain,(
% 265.86/39.01 ![X0,X1,X2,X3,X4,X5]: (~product(X0,X1,X2)|~sum(X3,X1,X4)|~sum(multiply(X0,X3),X2,X5)|product(X0,X4,X5))),
% 265.86/39.01 inference(resolution,[status(thm)],[f27,f37])).
% 265.86/39.01 fof(f82,plain,(
% 265.86/39.01 ![X0,X1,X2,X3,X4,X5]: (~product(X0,X1,X2)|~sum(X3,X1,X4)|~product(X0,X4,X5)|sum(multiply(X0,X3),X2,X5))),
% 265.86/39.01 inference(resolution,[status(thm)],[f27,f35])).
% 265.86/39.01 fof(f83,plain,(
% 265.86/39.01 ![X0,X1]: (product(X0,X1,multiply(X1,X0)))),
% 265.86/39.01 inference(resolution,[status(thm)],[f27,f29])).
% 265.86/39.01 fof(f86,plain,(
% 265.86/39.01 ![X0,X1,X2,X3]: (~product(X0,y,X1)|~sum(x,X0,X2)|~product(X2,y,X3)|sum(x_times_y,X1,X3))),
% 265.86/39.01 inference(resolution,[status(thm)],[f39,f58])).
% 265.86/39.01 fof(f88,plain,(
% 265.86/39.01 ![X0,X1,X2,X3,X4,X5]: (~product(X0,X1,X2)|~sum(X3,X0,X4)|~product(X4,X1,X5)|sum(multiply(X3,X1),X2,X5))),
% 265.86/39.01 inference(resolution,[status(thm)],[f39,f27])).
% 265.86/39.01 fof(f92,plain,(
% 265.86/39.01 x_inverse_plus_y_inverse=add(inverse(x),inverse(y))),
% 265.86/39.01 inference(resolution,[status(thm)],[f64,f26])).
% 265.86/39.01 fof(f94,plain,(
% 265.86/39.01 ![X0,X1]: (~sum(y,multiplicative_identity,X0)|~product(x,X0,X1)|sum(x_times_y,x,X1))),
% 265.86/39.01 inference(resolution,[status(thm)],[f66,f33])).
% 265.86/39.01 fof(f95,plain,(
% 265.86/39.01 ![X0,X1,X2]: (~sum(y,X0,X1)|~product(x,X1,X2)|sum(x_times_y,multiply(x,X0),X2))),
% 265.86/39.01 inference(resolution,[status(thm)],[f66,f27])).
% 265.86/39.01 fof(f98,plain,(
% 265.86/39.01 ![X0]: (X0=add(additive_identity,X0))),
% 265.86/39.01 inference(resolution,[status(thm)],[f69,f26])).
% 265.86/39.01 fof(f102,plain,(
% 265.86/39.01 ![X0]: (X0=add(X0,additive_identity))),
% 265.86/39.01 inference(resolution,[status(thm)],[f71,f26])).
% 265.86/39.01 fof(f106,plain,(
% 265.86/39.01 ![X0,X1,X2,X3,X4]: (~product(X0,X1,X2)|~sum(multiplicative_identity,X0,X3)|~sum(X1,X2,X4)|product(X3,X1,X4))),
% 265.86/39.01 inference(resolution,[status(thm)],[f41,f32])).
% 265.86/39.01 fof(f114,plain,(
% 265.86/39.01 ![X0,X1,X2,X3,X4]: (~sum(X0,X1,X2)|~product(additive_identity,X1,X3)|~sum(X0,X3,X4)|product(X0,X2,X4))),
% 265.86/39.01 inference(resolution,[status(thm)],[f43,f31])).
% 265.86/39.01 fof(f116,plain,(
% 265.86/39.01 inverse(additive_identity)=multiplicative_identity),
% 265.86/39.01 inference(resolution,[status(thm)],[f50,f71])).
% 265.86/39.01 fof(f118,plain,(
% 265.86/39.01 ![X0,X1]: (~sum(inverse(X0),X0,X1)|multiplicative_identity=X1)),
% 265.86/39.01 inference(resolution,[status(thm)],[f50,f55])).
% 265.86/39.01 fof(f140,plain,(
% 265.86/39.01 x_inverse_plus_y_inverse=add(inverse(y),inverse(x))),
% 265.86/39.01 inference(resolution,[status(thm)],[f80,f64])).
% 265.86/39.01 fof(f143,plain,(
% 265.86/39.01 ![X0,X1,X2]: (~sum(X0,X1,X2)|add(X1,X0)=X2)),
% 265.86/39.01 inference(resolution,[status(thm)],[f80,f55])).
% 265.86/39.01 fof(f147,plain,(
% 265.86/39.01 ![X0,X1,X2,X3,X4]: (~sum(additive_identity,X0,X1)|~product(X2,X0,X3)|~product(X2,X1,X4)|sum(additive_identity,X3,X4))),
% 265.86/39.01 inference(resolution,[status(thm)],[f45,f30])).
% 265.86/39.01 fof(f192,plain,(
% 265.86/39.01 ![X0,X1]: (add(X0,X1)=add(X1,X0))),
% 265.86/39.01 inference(resolution,[status(thm)],[f79,f80])).
% 265.86/39.01 fof(f194,plain,(
% 265.86/39.01 ![X0,X1]: (~product(inverse(X0),X0,X1)|additive_identity=X1)),
% 265.86/39.01 inference(resolution,[status(thm)],[f57,f52])).
% 265.86/39.01 fof(f195,plain,(
% 265.86/39.01 ![X0,X1]: (~product(multiplicative_identity,X0,X1)|X0=X1)),
% 265.86/39.01 inference(resolution,[status(thm)],[f57,f32])).
% 265.86/39.01 fof(f196,plain,(
% 265.86/39.01 ![X0]: (~product(y,x,X0)|x_times_y=X0)),
% 265.86/39.01 inference(resolution,[status(thm)],[f57,f62])).
% 265.86/39.01 fof(f198,plain,(
% 265.86/39.01 ![X0,X1]: (~product(X0,inverse(X0),X1)|additive_identity=X1)),
% 265.86/39.01 inference(resolution,[status(thm)],[f57,f53])).
% 265.86/39.01 fof(f199,plain,(
% 265.86/39.01 ![X0,X1]: (~product(X0,multiplicative_identity,X1)|X0=X1)),
% 265.86/39.01 inference(resolution,[status(thm)],[f57,f33])).
% 265.86/39.01 fof(f200,plain,(
% 265.86/39.01 ![X0,X1,X2]: (~product(X0,X1,X2)|multiply(X1,X0)=X2)),
% 265.86/39.01 inference(resolution,[status(thm)],[f57,f83])).
% 265.86/39.01 fof(f201,plain,(
% 265.86/39.01 ![X0,X1,X2]: (~product(X0,X1,X2)|multiply(X0,X1)=X2)),
% 265.86/39.01 inference(resolution,[status(thm)],[f57,f27])).
% 265.86/39.01 fof(f244,plain,(
% 265.86/39.01 ![X0]: (X0=multiply(X0,multiplicative_identity))),
% 265.86/39.01 inference(resolution,[status(thm)],[f195,f83])).
% 265.86/39.01 fof(f265,plain,(
% 265.86/39.01 ![X0,X1,X2]: (~sum(multiplicative_identity,inverse(X0),X1)|~sum(X0,additive_identity,X2)|product(X0,X1,X2))),
% 265.86/39.01 inference(resolution,[status(thm)],[f76,f53])).
% 265.86/39.01 fof(f275,plain,(
% 265.86/39.01 ![X0,X1,X2,X3]: (~sum(multiplicative_identity,X0,X1)|~product(X2,X1,X3)|sum(X2,multiply(X0,X2),X3))),
% 265.86/39.01 inference(resolution,[status(thm)],[f77,f83])).
% 265.86/39.01 fof(f279,plain,(
% 265.86/39.01 x_times_y=multiply(y,x)),
% 265.86/39.01 inference(resolution,[status(thm)],[f196,f27])).
% 265.86/39.01 fof(f283,plain,(
% 265.86/39.01 ![X0,X1]: (~sum(x,multiplicative_identity,X0)|~product(X0,y,X1)|sum(x_times_y,y,X1))),
% 265.86/39.01 inference(resolution,[status(thm)],[f86,f32])).
% 265.86/39.01 fof(f308,plain,(
% 265.86/39.01 ![X0,X1,X2,X3]: (~sum(X0,inverse(X1),X2)|~sum(multiply(X1,X0),additive_identity,X3)|product(X1,X2,X3))),
% 265.86/39.01 inference(resolution,[status(thm)],[f81,f53])).
% 265.86/39.01 fof(f310,plain,(
% 265.86/39.01 ![X0,X1,X2,X3,X4]: (~sum(X0,X1,X2)|~sum(multiply(X3,X0),multiply(X1,X3),X4)|product(X3,X2,X4))),
% 265.86/39.01 inference(resolution,[status(thm)],[f81,f83])).
% 265.86/39.01 fof(f319,plain,(
% 265.86/39.01 ![X0,X1,X2,X3,X4]: (~sum(X0,X1,X2)|~product(X3,X2,X4)|sum(multiply(X3,X0),multiply(X1,X3),X4))),
% 265.86/39.01 inference(resolution,[status(thm)],[f82,f83])).
% 265.86/39.01 fof(f338,plain,(
% 265.86/39.01 ![X0]: (additive_identity=multiply(X0,inverse(X0)))),
% 265.86/39.01 inference(resolution,[status(thm)],[f194,f83])).
% 265.86/39.01 fof(f377,plain,(
% 265.86/39.01 ![X0,X1,X2,X3]: (~sum(X0,X1,X2)|~product(X2,inverse(X1),X3)|sum(multiply(X0,inverse(X1)),additive_identity,X3))),
% 265.86/39.01 inference(resolution,[status(thm)],[f88,f53])).
% 265.86/39.01 fof(f380,plain,(
% 265.86/39.01 ![X0,X1,X2,X3,X4]: (~sum(X0,X1,X2)|~product(X2,X3,X4)|sum(multiply(X0,X3),multiply(X1,X3),X4))),
% 265.86/39.01 inference(resolution,[status(thm)],[f88,f27])).
% 265.86/39.01 fof(f408,plain,(
% 265.86/39.01 ![X0,X1]: (multiply(X0,X1)=multiply(X1,X0))),
% 265.86/39.01 inference(resolution,[status(thm)],[f200,f27])).
% 265.86/39.01 fof(f447,plain,(
% 265.86/39.01 ![X0,X1,X2,X3]: (~sum(multiplicative_identity,X0,X1)|~sum(X2,multiply(X2,X0),X3)|product(X1,X2,X3))),
% 265.86/39.01 inference(resolution,[status(thm)],[f106,f83])).
% 265.86/39.01 fof(f684,plain,(
% 265.86/39.01 ![X0,X1,X2,X3]: (~product(additive_identity,X0,X1)|~sum(X2,X1,X3)|product(X2,add(X0,X2),X3))),
% 265.86/39.01 inference(resolution,[status(thm)],[f114,f80])).
% 265.86/39.01 fof(f1115,plain,(
% 265.86/39.01 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(X0,X1,X3)|sum(additive_identity,X2,X3))),
% 265.86/39.01 inference(resolution,[status(thm)],[f147,f30])).
% 265.86/39.01 fof(f1442,plain,(
% 265.86/39.01 ![X0,X1,X2]: (~product(X0,X1,X2)|sum(additive_identity,multiply(X1,X0),X2))),
% 265.86/39.01 inference(resolution,[status(thm)],[f1115,f83])).
% 265.86/39.01 fof(f1502,plain,(
% 265.86/39.01 ![X0,X1]: (sum(additive_identity,multiply(X0,X1),multiply(X1,X0)))),
% 265.86/39.01 inference(resolution,[status(thm)],[f1442,f27])).
% 265.86/39.01 fof(f1545,plain,(
% 265.86/39.01 ![X0,X1]: (sum(multiply(X0,X1),additive_identity,multiply(X1,X0)))),
% 265.86/39.01 inference(resolution,[status(thm)],[f1502,f28])).
% 265.86/39.01 fof(f1666,plain,(
% 265.86/39.01 ![X0]: (~sum(y,multiplicative_identity,X0)|sum(x_times_y,x,multiply(X0,x)))),
% 265.86/39.01 inference(resolution,[status(thm)],[f94,f83])).
% 265.86/39.01 fof(f1670,plain,(
% 265.86/39.01 ![X0,X1]: (~product(x,add(X0,y),X1)|sum(x_times_y,multiply(x,X0),X1))),
% 265.86/39.01 inference(resolution,[status(thm)],[f95,f80])).
% 265.86/39.01 fof(f2683,plain,(
% 265.86/39.01 ![X0,X1]: (~sum(X0,additive_identity,X1)|product(X0,add(inverse(X0),multiplicative_identity),X1))),
% 265.86/39.01 inference(resolution,[status(thm)],[f265,f80])).
% 265.86/39.01 fof(f2943,plain,(
% 265.86/39.01 ![X0,X1,X2]: (~product(X0,add(X1,multiplicative_identity),X2)|sum(X0,multiply(X1,X0),X2))),
% 265.86/39.01 inference(resolution,[status(thm)],[f275,f80])).
% 265.86/39.01 fof(f2965,plain,(
% 265.86/39.01 ~sum(x,multiplicative_identity,multiplicative_identity)|sum(x_times_y,y,y)),
% 265.86/39.01 inference(resolution,[status(thm)],[f283,f32])).
% 265.86/39.01 fof(f3193,plain,(
% 265.86/39.01 ![X0,X1]: (~sum(multiply(X0,additive_identity),additive_identity,X1)|product(X0,inverse(X0),X1))),
% 265.86/39.01 inference(resolution,[status(thm)],[f308,f30])).
% 265.86/39.01 fof(f3196,plain,(
% 265.86/39.01 ![X0,X1]: (~sum(multiply(X0,inverse(inverse(X0))),additive_identity,X1)|product(X0,multiplicative_identity,X1))),
% 265.86/39.01 inference(resolution,[status(thm)],[f308,f50])).
% 265.86/39.01 fof(f3197,plain,(
% 265.86/39.01 ![X0,X1]: (~sum(multiply(X0,X0),additive_identity,X1)|product(X0,multiplicative_identity,X1))),
% 265.86/39.01 inference(resolution,[status(thm)],[f308,f51])).
% 265.86/39.01 fof(f3200,plain,(
% 265.86/39.01 ![X0,X1,X2]: (~sum(multiply(X0,X1),additive_identity,X2)|product(X0,add(inverse(X0),X1),X2))),
% 265.86/39.01 inference(resolution,[status(thm)],[f308,f80])).
% 265.86/39.01 fof(f3377,plain,(
% 265.86/39.01 ![X0,X1]: (~sum(multiply(X0,inverse(y)),multiply(inverse(x),X0),X1)|product(X0,x_inverse_plus_y_inverse,X1))),
% 265.86/39.01 inference(resolution,[status(thm)],[f310,f61])).
% 265.86/39.01 fof(f3717,plain,(
% 265.86/39.01 ![X0,X1,X2]: (~product(X0,multiplicative_identity,X1)|sum(multiply(X0,inverse(X2)),multiply(X2,X0),X1))),
% 265.86/39.01 inference(resolution,[status(thm)],[f319,f50])).
% 265.86/39.01 fof(f4163,plain,(
% 265.86/39.01 ![X0,X1]: (~product(multiplicative_identity,inverse(inverse(X0)),X1)|sum(multiply(X0,inverse(inverse(X0))),additive_identity,X1))),
% 265.86/39.01 inference(resolution,[status(thm)],[f377,f51])).
% 265.86/39.01 fof(f4211,plain,(
% 265.86/39.01 ![X0,X1,X2]: (~product(multiplicative_identity,X0,X1)|sum(multiply(inverse(X2),X0),multiply(X2,X0),X1))),
% 265.86/39.01 inference(resolution,[status(thm)],[f380,f50])).
% 265.86/39.01 fof(f4328,plain,(
% 265.86/39.01 ![X0,X1,X2]: (~sum(X0,multiply(X0,X1),X2)|product(add(X1,multiplicative_identity),X0,X2))),
% 265.86/39.01 inference(resolution,[status(thm)],[f447,f80])).
% 265.86/39.01 fof(f4609,plain,(
% 265.86/39.01 ![X0]: (product(X0,multiplicative_identity,multiply(X0,X0)))),
% 265.86/39.01 inference(resolution,[status(thm)],[f3197,f1545])).
% 265.86/39.01 fof(f4655,plain,(
% 265.86/39.01 ![X0]: (X0=multiply(X0,X0))),
% 265.86/39.01 inference(resolution,[status(thm)],[f4609,f199])).
% 265.86/39.01 fof(f4765,plain,(
% 265.86/39.01 ![X0]: (product(X0,X0,X0))),
% 265.86/39.01 inference(paramodulation,[status(thm)],[f4655,f83])).
% 265.86/39.01 fof(f4932,plain,(
% 265.86/39.01 ![X0,X1]: (~sum(X0,additive_identity,X1)|product(X0,add(inverse(additive_identity),X0),X1))),
% 265.86/39.01 inference(resolution,[status(thm)],[f684,f53])).
% 265.86/39.01 fof(f4934,plain,(
% 265.86/39.01 ![X0,X1,X2]: (~sum(X0,multiply(X1,additive_identity),X2)|product(X0,add(X1,X0),X2))),
% 265.86/39.01 inference(resolution,[status(thm)],[f684,f83])).
% 265.86/39.01 fof(f4938,plain,(
% 265.86/39.01 ![X0,X1]: (~sum(X0,additive_identity,X1)|product(X0,add(multiplicative_identity,X0),X1))),
% 265.86/39.01 inference(forward_demodulation,[status(thm)],[f116,f4932])).
% 265.86/39.01 fof(f6529,plain,(
% 265.86/39.01 sum(x_times_y,x,multiply(add(y,multiplicative_identity),x))),
% 265.86/39.01 inference(resolution,[status(thm)],[f1666,f26])).
% 265.86/39.01 fof(f6956,plain,(
% 265.86/39.01 add(x,x_times_y)=multiply(add(y,multiplicative_identity),x)),
% 265.86/39.01 inference(resolution,[status(thm)],[f6529,f143])).
% 265.86/39.01 fof(f7327,plain,(
% 265.86/39.01 add(x,x_times_y)=multiply(x,add(y,multiplicative_identity))),
% 265.86/39.01 inference(paramodulation,[status(thm)],[f408,f6956])).
% 265.86/39.01 fof(f8511,plain,(
% 265.86/39.01 ![X0]: (product(X0,add(multiplicative_identity,X0),X0))),
% 265.86/39.01 inference(resolution,[status(thm)],[f4938,f31])).
% 265.86/39.01 fof(f8598,plain,(
% 265.86/39.01 ![X0]: (multiply(X0,add(multiplicative_identity,X0))=X0)),
% 265.86/39.01 inference(resolution,[status(thm)],[f8511,f201])).
% 265.86/39.01 fof(f9279,plain,(
% 265.86/39.01 ![X0]: (multiply(X0,add(X0,multiplicative_identity))=X0)),
% 265.86/39.01 inference(paramodulation,[status(thm)],[f192,f8598])).
% 265.86/39.01 fof(f12606,plain,(
% 265.86/39.01 ![X0]: (sum(x_times_y,multiply(x,X0),multiply(add(X0,y),x)))),
% 265.86/39.01 inference(resolution,[status(thm)],[f1670,f83])).
% 265.86/39.01 fof(f17706,plain,(
% 265.86/39.01 ![X0]: (product(X0,add(inverse(X0),multiplicative_identity),X0))),
% 265.86/39.01 inference(resolution,[status(thm)],[f2683,f31])).
% 265.86/39.01 fof(f17868,plain,(
% 265.86/39.01 ![X0]: (multiply(add(inverse(X0),multiplicative_identity),X0)=X0)),
% 265.86/39.01 inference(resolution,[status(thm)],[f17706,f200])).
% 265.86/39.01 fof(f19445,plain,(
% 265.86/39.01 ![X0]: (sum(add(X0,multiplicative_identity),multiply(X0,add(X0,multiplicative_identity)),add(X0,multiplicative_identity)))),
% 265.86/39.01 inference(resolution,[status(thm)],[f2943,f4765])).
% 265.86/39.01 fof(f19467,plain,(
% 265.86/39.01 ![X0]: (sum(add(X0,multiplicative_identity),X0,add(X0,multiplicative_identity)))),
% 265.86/39.01 inference(forward_demodulation,[status(thm)],[f9279,f19445])).
% 265.86/39.01 fof(f20784,plain,(
% 265.86/39.01 ![X0]: (sum(X0,add(X0,multiplicative_identity),add(X0,multiplicative_identity)))),
% 265.86/39.01 inference(resolution,[status(thm)],[f19467,f28])).
% 265.86/39.01 fof(f21934,plain,(
% 265.86/39.01 ![X0]: (product(X0,inverse(X0),multiply(additive_identity,X0)))),
% 265.86/39.01 inference(resolution,[status(thm)],[f3193,f1545])).
% 265.86/39.01 fof(f22256,plain,(
% 265.86/39.01 ![X0]: (additive_identity=multiply(additive_identity,X0))),
% 265.86/39.01 inference(resolution,[status(thm)],[f21934,f198])).
% 265.86/39.01 fof(f22472,plain,(
% 265.86/39.01 ![X0]: (additive_identity=multiply(X0,additive_identity))),
% 265.86/39.01 inference(paramodulation,[status(thm)],[f408,f22256])).
% 265.86/39.01 fof(f22568,plain,(
% 265.86/39.01 ![X0]: (product(X0,multiplicative_identity,multiply(inverse(inverse(X0)),X0)))),
% 265.86/39.01 inference(resolution,[status(thm)],[f3196,f1545])).
% 265.86/39.01 fof(f22584,plain,(
% 265.86/39.01 ![X0,X1]: (product(X0,add(inverse(X0),X1),multiply(X1,X0)))),
% 265.86/39.01 inference(resolution,[status(thm)],[f3200,f1545])).
% 265.86/39.01 fof(f22914,plain,(
% 265.86/39.01 ![X0]: (product(X0,x_inverse_plus_y_inverse,add(multiply(inverse(x),X0),multiply(X0,inverse(y)))))),
% 265.86/39.01 inference(resolution,[status(thm)],[f3377,f80])).
% 265.86/39.01 fof(f27899,plain,(
% 265.86/39.01 ![X0,X1]: (sum(multiply(X0,inverse(X1)),multiply(X1,X0),X0))),
% 265.86/39.01 inference(resolution,[status(thm)],[f3717,f33])).
% 265.86/39.01 fof(f28020,plain,(
% 265.86/39.01 ![X0]: (X0=multiply(inverse(inverse(X0)),X0))),
% 265.86/39.01 inference(resolution,[status(thm)],[f22568,f199])).
% 265.86/39.01 fof(f28273,plain,(
% 265.86/39.01 ![X0]: (X0=multiply(X0,inverse(inverse(X0))))),
% 265.86/39.01 inference(paramodulation,[status(thm)],[f408,f28020])).
% 265.86/39.01 fof(f29869,plain,(
% 265.86/39.01 ![X0,X1]: (multiply(X0,add(inverse(X0),X1))=multiply(X1,X0))),
% 265.86/39.01 inference(resolution,[status(thm)],[f22584,f201])).
% 265.86/39.01 fof(f31740,plain,(
% 265.86/39.01 ![X0,X1]: (~product(multiplicative_identity,inverse(inverse(X0)),X1)|sum(X0,additive_identity,X1))),
% 265.86/39.01 inference(forward_demodulation,[status(thm)],[f28273,f4163])).
% 265.86/39.01 fof(f31741,plain,(
% 265.86/39.01 ![X0]: (sum(X0,additive_identity,inverse(inverse(X0))))),
% 265.86/39.01 inference(resolution,[status(thm)],[f31740,f32])).
% 265.86/39.01 fof(f32040,plain,(
% 265.86/39.01 ![X0]: (X0=inverse(inverse(X0)))),
% 265.86/39.01 inference(resolution,[status(thm)],[f31741,f71])).
% 265.86/39.01 fof(f33509,plain,(
% 265.86/39.01 ![X0,X1]: (sum(multiply(inverse(X0),X1),multiply(X0,X1),X1))),
% 265.86/39.01 inference(resolution,[status(thm)],[f4211,f32])).
% 265.86/39.01 fof(f35013,plain,(
% 265.86/39.01 ![X0,X1]: (add(multiply(X0,X1),multiply(X1,inverse(X0)))=X1)),
% 265.86/39.01 inference(resolution,[status(thm)],[f27899,f143])).
% 265.86/39.01 fof(f35014,plain,(
% 265.86/39.01 ![X0,X1]: (add(multiply(X0,inverse(X1)),multiply(X1,X0))=X0)),
% 265.86/39.01 inference(resolution,[status(thm)],[f27899,f79])).
% 265.86/39.01 fof(f35022,plain,(
% 265.86/39.01 ![X0]: (sum(inverse(X0),multiply(X0,add(inverse(inverse(X0)),multiplicative_identity)),add(inverse(inverse(X0)),multiplicative_identity)))),
% 265.86/39.01 inference(paramodulation,[status(thm)],[f17868,f27899])).
% 265.86/39.01 fof(f35082,plain,(
% 265.86/39.01 ![X0]: (sum(inverse(X0),multiply(X0,add(X0,multiplicative_identity)),add(inverse(inverse(X0)),multiplicative_identity)))),
% 265.86/39.01 inference(forward_demodulation,[status(thm)],[f32040,f35022])).
% 265.86/39.01 fof(f35083,plain,(
% 265.86/39.01 ![X0]: (sum(inverse(X0),X0,add(inverse(inverse(X0)),multiplicative_identity)))),
% 265.86/39.01 inference(forward_demodulation,[status(thm)],[f9279,f35082])).
% 265.86/39.01 fof(f35084,plain,(
% 265.86/39.01 ![X0]: (sum(inverse(X0),X0,add(X0,multiplicative_identity)))),
% 265.86/39.01 inference(forward_demodulation,[status(thm)],[f32040,f35083])).
% 265.86/39.01 fof(f35149,plain,(
% 265.86/39.01 ![X0]: (multiplicative_identity=add(X0,multiplicative_identity))),
% 265.86/39.01 inference(resolution,[status(thm)],[f35084,f118])).
% 265.86/39.01 fof(f35472,plain,(
% 265.86/39.01 add(x,x_times_y)=multiply(x,multiplicative_identity)),
% 265.86/39.01 inference(backward_demodulation,[status(thm)],[f35149,f7327])).
% 265.86/39.01 fof(f35489,plain,(
% 265.86/39.01 ![X0]: (sum(X0,add(X0,multiplicative_identity),multiplicative_identity))),
% 265.86/39.01 inference(backward_demodulation,[status(thm)],[f35149,f20784])).
% 265.86/39.01 fof(f35631,plain,(
% 265.86/39.01 add(x,x_times_y)=x),
% 265.86/39.01 inference(forward_demodulation,[status(thm)],[f244,f35472])).
% 265.86/39.01 fof(f35633,plain,(
% 265.86/39.01 ![X0]: (sum(X0,multiplicative_identity,multiplicative_identity))),
% 265.86/39.01 inference(forward_demodulation,[status(thm)],[f35149,f35489])).
% 265.86/39.01 fof(f35700,plain,(
% 265.86/39.01 sum(x_times_y,y,y)),
% 265.86/39.01 inference(backward_subsumption_resolution,[status(thm)],[f2965,f35633])).
% 265.86/39.01 fof(f36192,plain,(
% 265.86/39.01 ![X0,X1,X2]: (~sum(X0,multiply(X0,X1),X2)|product(multiplicative_identity,X0,X2))),
% 265.86/39.01 inference(forward_demodulation,[status(thm)],[f35149,f4328])).
% 265.86/39.01 fof(f36195,plain,(
% 265.86/39.01 ![X0,X1]: (product(multiplicative_identity,X0,add(multiply(X0,X1),X0)))),
% 265.86/39.01 inference(resolution,[status(thm)],[f36192,f80])).
% 265.86/39.01 fof(f36688,plain,(
% 265.86/39.01 add(y,x_times_y)=y),
% 265.86/39.01 inference(resolution,[status(thm)],[f35700,f143])).
% 265.86/39.01 fof(f38241,plain,(
% 265.86/39.01 ![X0,X1]: (X0=add(multiply(X0,X1),X0))),
% 265.86/39.01 inference(resolution,[status(thm)],[f36195,f195])).
% 265.86/39.01 fof(f38625,plain,(
% 265.86/39.01 ![X0,X1]: (X0=add(X0,multiply(X0,X1)))),
% 265.86/39.01 inference(paramodulation,[status(thm)],[f192,f38241])).
% 265.86/39.01 fof(f38649,plain,(
% 265.86/39.01 ![X0,X1]: (X0=add(multiply(X1,X0),X0))),
% 265.86/39.01 inference(paramodulation,[status(thm)],[f408,f38241])).
% 265.86/39.01 fof(f38770,plain,(
% 265.86/39.01 ![X0,X1]: (X0=add(X0,multiply(X1,X0)))),
% 265.86/39.01 inference(paramodulation,[status(thm)],[f408,f38625])).
% 265.86/39.01 fof(f40456,plain,(
% 265.86/39.01 ![X0,X1,X2]: (~sum(X0,additive_identity,X1)|product(X0,add(X2,X0),X1))),
% 265.86/39.01 inference(forward_demodulation,[status(thm)],[f22472,f4934])).
% 265.86/39.01 fof(f40464,plain,(
% 265.86/39.01 ![X0,X1]: (product(X0,add(X1,X0),X0))),
% 265.86/39.01 inference(resolution,[status(thm)],[f40456,f31])).
% 265.86/39.01 fof(f40623,plain,(
% 265.86/39.01 ![X0,X1]: (multiply(X0,add(X1,X0))=X0)),
% 265.86/39.01 inference(resolution,[status(thm)],[f40464,f201])).
% 265.86/39.01 fof(f40624,plain,(
% 265.86/39.01 ![X0,X1]: (multiply(add(X0,X1),X1)=X1)),
% 265.86/39.01 inference(resolution,[status(thm)],[f40464,f200])).
% 265.86/39.01 fof(f40722,plain,(
% 265.86/39.01 multiply(x_times_y,y)=x_times_y),
% 265.86/39.01 inference(paramodulation,[status(thm)],[f36688,f40623])).
% 265.86/39.01 fof(f40723,plain,(
% 265.86/39.01 multiply(x_times_y,x)=x_times_y),
% 265.86/39.01 inference(paramodulation,[status(thm)],[f35631,f40623])).
% 265.86/39.01 fof(f40743,plain,(
% 265.86/39.01 multiply(inverse(x),x_inverse_plus_y_inverse)=inverse(x)),
% 265.86/39.01 inference(paramodulation,[status(thm)],[f140,f40623])).
% 265.86/39.01 fof(f40744,plain,(
% 265.86/39.01 multiply(inverse(y),x_inverse_plus_y_inverse)=inverse(y)),
% 265.86/39.01 inference(paramodulation,[status(thm)],[f92,f40623])).
% 265.86/39.01 fof(f40753,plain,(
% 265.86/39.01 ![X0,X1]: (multiply(X0,add(X0,X1))=X0)),
% 265.86/39.01 inference(paramodulation,[status(thm)],[f192,f40623])).
% 265.86/39.01 fof(f40952,plain,(
% 265.86/39.01 ![X0,X1]: (multiply(X0,multiply(X0,X1))=multiply(X0,X1))),
% 265.86/39.01 inference(paramodulation,[status(thm)],[f38625,f40624])).
% 265.86/39.01 fof(f47857,plain,(
% 265.86/39.01 ![X0,X1]: (multiply(X0,multiply(X1,X0))=multiply(X0,X1))),
% 265.86/39.01 inference(paramodulation,[status(thm)],[f408,f40952])).
% 265.86/39.01 fof(f67216,plain,(
% 265.86/39.01 ![X0,X1]: (multiply(X0,inverse(X0))=multiply(multiply(X1,inverse(X0)),X0))),
% 265.86/39.01 inference(paramodulation,[status(thm)],[f38770,f29869])).
% 265.86/39.01 fof(f67408,plain,(
% 265.86/39.01 ![X0,X1]: (additive_identity=multiply(multiply(X0,inverse(X1)),X1))),
% 265.86/39.01 inference(forward_demodulation,[status(thm)],[f338,f67216])).
% 265.86/39.01 fof(f67525,plain,(
% 265.86/39.01 ![X0,X1]: (additive_identity=multiply(X0,multiply(X1,inverse(X0))))),
% 265.86/39.01 inference(paramodulation,[status(thm)],[f408,f67408])).
% 265.86/39.01 fof(f67544,plain,(
% 265.86/39.01 ![X0,X1]: (additive_identity=multiply(multiply(X0,X1),inverse(X1)))),
% 265.86/39.01 inference(paramodulation,[status(thm)],[f32040,f67408])).
% 265.86/39.01 fof(f68198,plain,(
% 265.86/39.01 ![X0,X1]: (additive_identity=multiply(inverse(X0),multiply(X1,X0)))),
% 265.86/39.01 inference(paramodulation,[status(thm)],[f32040,f67525])).
% 265.86/39.01 fof(f68956,plain,(
% 265.86/39.01 additive_identity=multiply(x_times_y,inverse(x))),
% 265.86/39.01 inference(paramodulation,[status(thm)],[f40723,f67544])).
% 265.86/39.01 fof(f68957,plain,(
% 265.86/39.01 additive_identity=multiply(x_times_y,inverse(y))),
% 265.86/39.01 inference(paramodulation,[status(thm)],[f40722,f67544])).
% 265.86/39.01 fof(f68986,plain,(
% 265.86/39.01 additive_identity=multiply(inverse(y),inverse(x_inverse_plus_y_inverse))),
% 265.86/39.01 inference(paramodulation,[status(thm)],[f40744,f67544])).
% 265.86/39.01 fof(f69010,plain,(
% 265.86/39.01 ![X0,X1]: (additive_identity=multiply(X0,inverse(add(X0,X1))))),
% 265.86/39.01 inference(paramodulation,[status(thm)],[f40753,f67544])).
% 265.86/39.01 fof(f69326,plain,(
% 265.86/39.01 multiply(inverse(x),additive_identity)=multiply(inverse(x),x_times_y)),
% 265.86/39.01 inference(paramodulation,[status(thm)],[f68956,f47857])).
% 265.86/39.01 fof(f69478,plain,(
% 265.86/39.01 additive_identity=multiply(inverse(x),x_times_y)),
% 265.86/39.01 inference(forward_demodulation,[status(thm)],[f22472,f69326])).
% 265.86/39.01 fof(f73384,plain,(
% 265.86/39.01 additive_identity=multiply(inverse(x_inverse_plus_y_inverse),inverse(x))),
% 265.86/39.01 inference(paramodulation,[status(thm)],[f40743,f68198])).
% 265.86/39.01 fof(f91072,plain,(
% 265.86/39.01 ![X0,X1]: (add(multiply(inverse(X0),X1),multiply(X0,X1))=X1)),
% 265.86/39.01 inference(resolution,[status(thm)],[f33509,f79])).
% 265.86/39.01 fof(f92048,plain,(
% 265.86/39.01 add(additive_identity,multiply(inverse(x_inverse_plus_y_inverse),inverse(inverse(y))))=inverse(x_inverse_plus_y_inverse)),
% 152.99/39.06 inference(paramodulation,[status(thm)],[f68986,f35013])).
% 152.99/39.06 fof(f92112,plain,(
% 152.99/39.06 add(multiply(x,inverse(x_inverse_plus_y_inverse)),additive_identity)=inverse(x_inverse_plus_y_inverse)),
% 152.99/39.06 inference(paramodulation,[status(thm)],[f73384,f35013])).
% 152.99/39.06 fof(f92305,plain,(
% 152.99/39.06 multiply(inverse(x_inverse_plus_y_inverse),inverse(inverse(y)))=inverse(x_inverse_plus_y_inverse)),
% 152.99/39.06 inference(forward_demodulation,[status(thm)],[f98,f92048])).
% 152.99/39.06 fof(f92306,plain,(
% 152.99/39.06 multiply(inverse(x_inverse_plus_y_inverse),y)=inverse(x_inverse_plus_y_inverse)),
% 152.99/39.06 inference(forward_demodulation,[status(thm)],[f32040,f92305])).
% 152.99/39.06 fof(f92370,plain,(
% 152.99/39.06 multiply(x,inverse(x_inverse_plus_y_inverse))=inverse(x_inverse_plus_y_inverse)),
% 152.99/39.06 inference(forward_demodulation,[status(thm)],[f102,f92112])).
% 152.99/39.06 fof(f94956,plain,(
% 152.99/39.06 y=add(inverse(x_inverse_plus_y_inverse),y)),
% 152.99/39.06 inference(paramodulation,[status(thm)],[f92306,f38649])).
% 152.99/39.06 fof(f104715,plain,(
% 152.99/39.06 sum(x_times_y,inverse(x_inverse_plus_y_inverse),multiply(add(inverse(x_inverse_plus_y_inverse),y),x))),
% 152.99/39.06 inference(paramodulation,[status(thm)],[f92370,f12606])).
% 152.99/39.06 fof(f104798,plain,(
% 152.99/39.06 sum(x_times_y,inverse(x_inverse_plus_y_inverse),multiply(y,x))),
% 152.99/39.06 inference(forward_demodulation,[status(thm)],[f94956,f104715])).
% 152.99/39.06 fof(f104799,plain,(
% 152.99/39.06 sum(x_times_y,inverse(x_inverse_plus_y_inverse),x_times_y)),
% 152.99/39.06 inference(forward_demodulation,[status(thm)],[f279,f104798])).
% 152.99/39.06 fof(f105123,plain,(
% 152.99/39.06 add(inverse(x_inverse_plus_y_inverse),x_times_y)=x_times_y),
% 152.99/39.06 inference(resolution,[status(thm)],[f104799,f143])).
% 152.99/39.06 fof(f105211,plain,(
% 152.99/39.06 additive_identity=multiply(inverse(x_inverse_plus_y_inverse),inverse(x_times_y))),
% 152.99/39.06 inference(paramodulation,[status(thm)],[f105123,f69010])).
% 152.99/39.06 fof(f107129,plain,(
% 152.99/39.06 add(multiply(inverse(x_times_y),inverse(inverse(x_inverse_plus_y_inverse))),additive_identity)=inverse(x_times_y)),
% 152.99/39.06 inference(paramodulation,[status(thm)],[f105211,f35014])).
% 152.99/39.06 fof(f107325,plain,(
% 152.99/39.06 multiply(inverse(x_times_y),inverse(inverse(x_inverse_plus_y_inverse)))=inverse(x_times_y)),
% 152.99/39.06 inference(forward_demodulation,[status(thm)],[f102,f107129])).
% 152.99/39.06 fof(f107326,plain,(
% 152.99/39.06 multiply(inverse(x_times_y),x_inverse_plus_y_inverse)=inverse(x_times_y)),
% 152.99/39.06 inference(forward_demodulation,[status(thm)],[f32040,f107325])).
% 152.99/39.06 fof(f190577,plain,(
% 152.99/39.06 product(x_times_y,x_inverse_plus_y_inverse,add(additive_identity,multiply(x_times_y,inverse(y))))),
% 152.99/39.06 inference(paramodulation,[status(thm)],[f69478,f22914])).
% 152.99/39.06 fof(f190970,plain,(
% 152.99/39.06 product(x_times_y,x_inverse_plus_y_inverse,multiply(x_times_y,inverse(y)))),
% 152.99/39.06 inference(forward_demodulation,[status(thm)],[f98,f190577])).
% 152.99/39.06 fof(f190971,plain,(
% 152.99/39.06 product(x_times_y,x_inverse_plus_y_inverse,additive_identity)),
% 152.99/39.06 inference(forward_demodulation,[status(thm)],[f68957,f190970])).
% 152.99/39.06 fof(f191125,plain,(
% 152.99/39.06 multiply(x_times_y,x_inverse_plus_y_inverse)=additive_identity),
% 152.99/39.06 inference(resolution,[status(thm)],[f190971,f201])).
% 152.99/39.06 fof(f191216,plain,(
% 152.99/39.06 add(multiply(inverse(x_times_y),x_inverse_plus_y_inverse),additive_identity)=x_inverse_plus_y_inverse),
% 152.99/39.06 inference(paramodulation,[status(thm)],[f191125,f91072])).
% 152.99/39.06 fof(f191453,plain,(
% 152.99/39.06 multiply(inverse(x_times_y),x_inverse_plus_y_inverse)=x_inverse_plus_y_inverse),
% 152.99/39.06 inference(forward_demodulation,[status(thm)],[f102,f191216])).
% 152.99/39.06 fof(f192901,plain,(
% 152.99/39.06 x_inverse_plus_y_inverse=inverse(x_times_y)),
% 152.99/39.06 inference(backward_demodulation,[status(thm)],[f191453,f107326])).
% 152.99/39.06 fof(f193214,plain,(
% 152.99/39.06 $false),
% 152.99/39.06 inference(forward_subsumption_resolution,[status(thm)],[f192901,f60])).
% 152.99/39.06 % SZS output end CNFRefutation for theBenchmark.p
% 152.99/39.07 % Elapsed time: 33.675475 seconds
% 152.99/39.07 % CPU time: 266.839682 seconds
% 152.99/39.07 % Total memory used: 438.837 MB
% 152.99/39.07 % Net memory used: 378.867 MB
%------------------------------------------------------------------------------