%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : BOO008-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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:43 PM UTC 2026
% Result : Unsatisfiable 228.22s 29.29s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : BOO008-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n020.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Mon Sep 21 13:48:02 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.44 % Drodi V4.1.1
% 228.22/29.29 % Refutation found
% 228.22/29.29 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 228.22/29.29 % SZS output start CNFRefutation for theBenchmark
% 228.22/29.29 fof(f1,axiom,(
% 228.22/29.29 (![X,Y]: (sum(X,Y,add(X,Y)) ))),
% 228.22/29.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 228.22/29.29 fof(f2,axiom,(
% 228.22/29.29 (![X,Y]: (product(X,Y,multiply(X,Y)) ))),
% 228.22/29.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 228.22/29.29 fof(f3,axiom,(
% 228.22/29.29 (![X,Y,Z]: (( ~ sum(X,Y,Z)| sum(Y,X,Z) ) ))),
% 228.22/29.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 228.22/29.29 fof(f4,axiom,(
% 228.22/29.29 (![X,Y,Z]: (( ~ product(X,Y,Z)| product(Y,X,Z) ) ))),
% 228.22/29.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 228.22/29.29 fof(f5,axiom,(
% 228.22/29.29 (![X]: (sum(additive_identity,X,X) ))),
% 228.22/29.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 228.22/29.29 fof(f6,axiom,(
% 228.22/29.29 (![X]: (sum(X,additive_identity,X) ))),
% 228.22/29.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 228.22/29.29 fof(f7,axiom,(
% 228.22/29.29 (![X]: (product(multiplicative_identity,X,X) ))),
% 228.22/29.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 228.22/29.29 fof(f8,axiom,(
% 228.22/29.29 (![X]: (product(X,multiplicative_identity,X) ))),
% 228.22/29.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 228.22/29.29 fof(f9,axiom,(
% 228.22/29.29 (![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) ) ))),
% 228.22/29.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 228.22/29.29 fof(f10,axiom,(
% 228.22/29.29 (![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) ) ))),
% 228.22/29.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 228.22/29.29 fof(f12,axiom,(
% 228.22/29.29 (![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) ) ))),
% 228.22/29.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 228.22/29.29 fof(f13,axiom,(
% 228.22/29.29 (![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) ) ))),
% 228.22/29.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 228.22/29.29 fof(f14,axiom,(
% 228.22/29.29 (![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) ) ))),
% 228.22/29.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 228.22/29.29 fof(f15,axiom,(
% 228.22/29.29 (![Y,X,V1,Z,V2,V3,V4]: (( ~ sum(Y,X,V1)| ~ sum(Z,X,V2)| ~ product(Y,Z,V3)| ~ sum(V3,X,V4)| product(V1,V2,V4) ) ))),
% 228.22/29.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 228.22/29.29 fof(f17,axiom,(
% 228.22/29.29 (![X]: (sum(inverse(X),X,multiplicative_identity) ))),
% 228.22/29.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 228.22/29.29 fof(f18,axiom,(
% 228.22/29.29 (![X]: (sum(X,inverse(X),multiplicative_identity) ))),
% 228.22/29.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 228.22/29.29 fof(f19,axiom,(
% 228.22/29.29 (![X]: (product(inverse(X),X,additive_identity) ))),
% 228.22/29.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 228.22/29.29 fof(f20,axiom,(
% 228.22/29.29 (![X]: (product(X,inverse(X),additive_identity) ))),
% 228.22/29.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 228.22/29.29 fof(f21,axiom,(
% 228.22/29.29 (![X,Y,U,V]: (( ~ sum(X,Y,U)| ~ sum(X,Y,V)| U = V ) ))),
% 228.22/29.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 228.22/29.29 fof(f22,axiom,(
% 228.22/29.29 (![X,Y,U,V]: (( ~ product(X,Y,U)| ~ product(X,Y,V)| U = V ) ))),
% 228.22/29.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 228.22/29.29 fof(f23,hypothesis,(
% 228.22/29.29 sum(y,z,y_plus_z) ),
% 228.22/29.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 228.22/29.29 fof(f24,hypothesis,(
% 228.22/29.29 sum(x,y_plus_z,x__plus_y_plus_z) ),
% 228.22/29.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 228.22/29.29 fof(f25,hypothesis,(
% 228.22/29.29 sum(x,y,x_plus_y) ),
% 228.22/29.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 228.22/29.29 fof(f26,hypothesis,(
% 228.22/29.29 sum(x_plus_y,z,x_plus_y__plus_z) ),
% 228.22/29.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 228.22/29.29 fof(f27,negated_conjecture,(
% 228.22/29.29 x__plus_y_plus_z != x_plus_y__plus_z ),
% 228.22/29.29 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 228.22/29.29 fof(f28,plain,(
% 228.22/29.29 ![X0,X1]: (sum(X0,X1,add(X0,X1)))),
% 228.22/29.29 inference(cnf_transformation,[status(thm)],[f1])).
% 228.22/29.29 fof(f29,plain,(
% 228.22/29.29 ![X0,X1]: (product(X0,X1,multiply(X0,X1)))),
% 228.22/29.29 inference(cnf_transformation,[status(thm)],[f2])).
% 228.22/29.29 fof(f30,plain,(
% 228.22/29.29 ![X0,X1,X2]: (~sum(X0,X1,X2)|sum(X1,X0,X2))),
% 228.22/29.29 inference(cnf_transformation,[status(thm)],[f3])).
% 228.22/29.29 fof(f31,plain,(
% 228.22/29.29 ![X0,X1,X2]: (~product(X0,X1,X2)|product(X1,X0,X2))),
% 228.22/29.29 inference(cnf_transformation,[status(thm)],[f4])).
% 228.22/29.29 fof(f32,plain,(
% 228.22/29.29 ![X0]: (sum(additive_identity,X0,X0))),
% 228.22/29.29 inference(cnf_transformation,[status(thm)],[f5])).
% 228.22/29.29 fof(f33,plain,(
% 228.22/29.29 ![X0]: (sum(X0,additive_identity,X0))),
% 228.22/29.29 inference(cnf_transformation,[status(thm)],[f6])).
% 228.22/29.29 fof(f34,plain,(
% 228.22/29.29 ![X0]: (product(multiplicative_identity,X0,X0))),
% 228.22/29.29 inference(cnf_transformation,[status(thm)],[f7])).
% 228.22/29.29 fof(f35,plain,(
% 228.22/29.29 ![X0]: (product(X0,multiplicative_identity,X0))),
% 228.22/29.29 inference(cnf_transformation,[status(thm)],[f8])).
% 228.22/29.29 fof(f36,plain,(
% 228.22/29.29 ![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))),
% 228.22/29.29 inference(miniscoping,[status(thm)],[f9])).
% 228.22/29.29 fof(f37,plain,(
% 228.22/29.29 ![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))),
% 228.22/29.29 inference(cnf_transformation,[status(thm)],[f36])).
% 228.22/29.29 fof(f38,plain,(
% 228.22/29.29 ![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))),
% 228.22/29.29 inference(miniscoping,[status(thm)],[f10])).
% 228.22/29.29 fof(f39,plain,(
% 228.22/29.29 ![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))),
% 228.22/29.29 inference(cnf_transformation,[status(thm)],[f38])).
% 228.22/29.29 fof(f42,plain,(
% 228.22/29.29 ![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))),
% 228.22/29.29 inference(miniscoping,[status(thm)],[f12])).
% 228.22/29.29 fof(f43,plain,(
% 228.22/29.29 ![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))),
% 228.22/29.29 inference(cnf_transformation,[status(thm)],[f42])).
% 228.22/29.29 fof(f44,plain,(
% 228.22/29.29 ![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))),
% 228.22/29.29 inference(miniscoping,[status(thm)],[f13])).
% 228.22/29.29 fof(f45,plain,(
% 228.22/29.29 ![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))),
% 228.22/29.29 inference(cnf_transformation,[status(thm)],[f44])).
% 228.22/29.29 fof(f46,plain,(
% 228.22/29.29 ![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))),
% 228.22/29.29 inference(miniscoping,[status(thm)],[f14])).
% 228.22/29.29 fof(f47,plain,(
% 228.22/29.29 ![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))),
% 228.22/29.29 inference(cnf_transformation,[status(thm)],[f46])).
% 228.22/29.29 fof(f48,plain,(
% 228.22/29.29 ![V1,V2,V4]: ((![X,V3]: ((![Y,Z]: ((~sum(Y,X,V1)|~sum(Z,X,V2))|~product(Y,Z,V3)))|~sum(V3,X,V4)))|product(V1,V2,V4))),
% 228.22/29.29 inference(miniscoping,[status(thm)],[f15])).
% 228.22/29.29 fof(f49,plain,(
% 228.22/29.29 ![X0,X1,X2,X3,X4,X5,X6]: (~sum(X0,X1,X2)|~sum(X3,X1,X4)|~product(X0,X3,X5)|~sum(X5,X1,X6)|product(X2,X4,X6))),
% 228.22/29.29 inference(cnf_transformation,[status(thm)],[f48])).
% 228.22/29.29 fof(f52,plain,(
% 228.22/29.29 ![X0]: (sum(inverse(X0),X0,multiplicative_identity))),
% 228.22/29.29 inference(cnf_transformation,[status(thm)],[f17])).
% 228.22/29.29 fof(f53,plain,(
% 228.22/29.29 ![X0]: (sum(X0,inverse(X0),multiplicative_identity))),
% 228.22/29.29 inference(cnf_transformation,[status(thm)],[f18])).
% 228.22/29.29 fof(f54,plain,(
% 228.22/29.29 ![X0]: (product(inverse(X0),X0,additive_identity))),
% 228.22/29.29 inference(cnf_transformation,[status(thm)],[f19])).
% 228.22/29.29 fof(f55,plain,(
% 228.22/29.29 ![X0]: (product(X0,inverse(X0),additive_identity))),
% 228.22/29.29 inference(cnf_transformation,[status(thm)],[f20])).
% 228.22/29.29 fof(f56,plain,(
% 228.22/29.29 ![U,V]: ((![X,Y]: (~sum(X,Y,U)|~sum(X,Y,V)))|U=V)),
% 228.22/29.29 inference(miniscoping,[status(thm)],[f21])).
% 228.22/29.29 fof(f57,plain,(
% 228.22/29.29 ![X0,X1,X2,X3]: (~sum(X0,X1,X2)|~sum(X0,X1,X3)|X2=X3)),
% 228.22/29.29 inference(cnf_transformation,[status(thm)],[f56])).
% 228.22/29.29 fof(f58,plain,(
% 228.22/29.29 ![U,V]: ((![X,Y]: (~product(X,Y,U)|~product(X,Y,V)))|U=V)),
% 228.22/29.29 inference(miniscoping,[status(thm)],[f22])).
% 228.22/29.29 fof(f59,plain,(
% 228.22/29.29 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(X0,X1,X3)|X2=X3)),
% 228.22/29.29 inference(cnf_transformation,[status(thm)],[f58])).
% 228.22/29.29 fof(f60,plain,(
% 228.22/29.29 sum(y,z,y_plus_z)),
% 228.22/29.29 inference(cnf_transformation,[status(thm)],[f23])).
% 228.22/29.29 fof(f61,plain,(
% 228.22/29.29 sum(x,y_plus_z,x__plus_y_plus_z)),
% 228.22/29.29 inference(cnf_transformation,[status(thm)],[f24])).
% 228.22/29.29 fof(f62,plain,(
% 228.22/29.29 sum(x,y,x_plus_y)),
% 228.22/29.29 inference(cnf_transformation,[status(thm)],[f25])).
% 228.22/29.29 fof(f63,plain,(
% 228.22/29.29 sum(x_plus_y,z,x_plus_y__plus_z)),
% 228.22/29.29 inference(cnf_transformation,[status(thm)],[f26])).
% 228.22/29.29 fof(f64,plain,(
% 228.22/29.29 ~x__plus_y_plus_z=x_plus_y__plus_z),
% 228.22/29.29 inference(cnf_transformation,[status(thm)],[f27])).
% 228.22/29.29 fof(f65,plain,(
% 228.22/29.29 sum(z,y,y_plus_z)),
% 228.22/29.29 inference(resolution,[status(thm)],[f30,f60])).
% 228.22/29.29 fof(f68,plain,(
% 228.22/29.29 sum(z,x_plus_y,x_plus_y__plus_z)),
% 228.22/29.29 inference(resolution,[status(thm)],[f30,f63])).
% 228.22/29.29 fof(f69,plain,(
% 228.22/29.29 sum(y,x,x_plus_y)),
% 228.22/29.29 inference(resolution,[status(thm)],[f30,f62])).
% 228.22/29.29 fof(f70,plain,(
% 228.22/29.29 sum(y_plus_z,x,x__plus_y_plus_z)),
% 228.22/29.29 inference(resolution,[status(thm)],[f30,f61])).
% 228.22/29.29 fof(f73,plain,(
% 228.22/29.29 ![X0,X1]: (sum(X0,X1,add(X1,X0)))),
% 228.22/29.29 inference(resolution,[status(thm)],[f30,f28])).
% 228.22/29.29 fof(f78,plain,(
% 228.22/29.29 ![X0,X1]: (product(X0,X1,multiply(X1,X0)))),
% 228.22/29.29 inference(resolution,[status(thm)],[f31,f29])).
% 228.22/29.29 fof(f81,plain,(
% 228.22/29.29 ![X0,X1,X2,X3,X4]: (~product(X0,X1,X2)|~sum(inverse(X0),X1,X3)|~product(X0,X3,X4)|sum(additive_identity,X2,X4))),
% 228.22/29.29 inference(resolution,[status(thm)],[f37,f55])).
% 228.22/29.29 fof(f83,plain,(
% 228.22/29.29 ![X0,X1,X2,X3,X4,X5]: (~product(X0,X1,X2)|~sum(X3,X1,X4)|~product(X0,X4,X5)|sum(multiply(X0,X3),X2,X5))),
% 228.22/29.29 inference(resolution,[status(thm)],[f37,f29])).
% 228.22/29.29 fof(f86,plain,(
% 228.22/29.29 ![X0,X1,X2,X3,X4]: (~product(inverse(X0),X1,X2)|~sum(X0,X1,X3)|~sum(additive_identity,X2,X4)|product(inverse(X0),X3,X4))),
% 228.22/29.29 inference(resolution,[status(thm)],[f39,f54])).
% 228.22/29.29 fof(f88,plain,(
% 228.22/29.29 ![X0,X1,X2,X3,X4]: (~product(X0,X1,X2)|~sum(inverse(X0),X1,X3)|~sum(additive_identity,X2,X4)|product(X0,X3,X4))),
% 228.22/29.29 inference(resolution,[status(thm)],[f39,f55])).
% 228.22/29.29 fof(f90,plain,(
% 228.22/29.29 ![X0,X1,X2,X3,X4,X5]: (~product(X0,X1,X2)|~sum(X3,X1,X4)|~sum(multiply(X0,X3),X2,X5)|product(X0,X4,X5))),
% 228.22/29.29 inference(resolution,[status(thm)],[f39,f29])).
% 228.22/29.29 fof(f104,plain,(
% 228.22/29.29 ![X0,X1,X2,X3,X4]: (~product(X0,X1,X2)|~sum(multiplicative_identity,X0,X3)|~sum(X1,X2,X4)|product(X3,X1,X4))),
% 228.22/29.29 inference(resolution,[status(thm)],[f43,f34])).
% 228.22/29.29 fof(f109,plain,(
% 228.22/29.29 ![X0]: (~sum(y_plus_z,x,X0)|x__plus_y_plus_z=X0)),
% 228.22/29.29 inference(resolution,[status(thm)],[f57,f70])).
% 228.22/29.29 fof(f110,plain,(
% 228.22/29.29 ![X0]: (~sum(z,y,X0)|y_plus_z=X0)),
% 228.22/29.29 inference(resolution,[status(thm)],[f57,f65])).
% 228.22/29.29 fof(f112,plain,(
% 228.22/29.29 ![X0]: (~sum(y,x,X0)|x_plus_y=X0)),
% 228.22/29.29 inference(resolution,[status(thm)],[f57,f69])).
% 228.22/29.29 fof(f114,plain,(
% 228.22/29.29 ![X0,X1]: (~sum(inverse(X0),X0,X1)|multiplicative_identity=X1)),
% 228.22/29.29 inference(resolution,[status(thm)],[f57,f52])).
% 228.22/29.29 fof(f115,plain,(
% 228.22/29.29 ![X0,X1]: (~sum(additive_identity,X0,X1)|X0=X1)),
% 228.22/29.29 inference(resolution,[status(thm)],[f57,f32])).
% 228.22/29.29 fof(f116,plain,(
% 228.22/29.29 ![X0]: (~sum(x_plus_y,z,X0)|x_plus_y__plus_z=X0)),
% 228.22/29.29 inference(resolution,[status(thm)],[f57,f63])).
% 228.22/29.29 fof(f121,plain,(
% 228.22/29.29 ![X0,X1,X2]: (~sum(X0,X1,X2)|add(X1,X0)=X2)),
% 228.22/29.29 inference(resolution,[status(thm)],[f57,f73])).
% 228.22/29.29 fof(f122,plain,(
% 228.22/29.29 ![X0,X1,X2]: (~sum(X0,X1,X2)|add(X0,X1)=X2)),
% 228.22/29.29 inference(resolution,[status(thm)],[f57,f28])).
% 228.22/29.29 fof(f124,plain,(
% 228.22/29.29 inverse(additive_identity)=multiplicative_identity),
% 228.22/29.29 inference(resolution,[status(thm)],[f115,f53])).
% 228.22/29.29 fof(f126,plain,(
% 228.22/29.29 ![X0]: (X0=add(X0,additive_identity))),
% 228.22/29.29 inference(resolution,[status(thm)],[f115,f73])).
% 228.22/29.29 fof(f127,plain,(
% 228.22/29.29 ![X0]: (X0=add(additive_identity,X0))),
% 228.22/29.29 inference(resolution,[status(thm)],[f115,f28])).
% 228.22/29.29 fof(f147,plain,(
% 228.22/29.29 ![X0,X1,X2,X3]: (~sum(y,X0,X1)|~product(z,X0,X2)|~sum(y,X2,X3)|product(y_plus_z,X1,X3))),
% 228.22/29.29 inference(resolution,[status(thm)],[f45,f60])).
% 228.22/29.29 fof(f151,plain,(
% 228.22/29.29 ![X0,X1,X2,X3]: (~sum(x,X0,X1)|~product(y,X0,X2)|~sum(x,X2,X3)|product(x_plus_y,X1,X3))),
% 228.22/29.29 inference(resolution,[status(thm)],[f45,f62])).
% 228.22/29.29 fof(f152,plain,(
% 228.22/29.29 ![X0,X1,X2,X3]: (~sum(x,X0,X1)|~product(y_plus_z,X0,X2)|~sum(x,X2,X3)|product(x__plus_y_plus_z,X1,X3))),
% 228.22/29.29 inference(resolution,[status(thm)],[f45,f61])).
% 228.22/29.29 fof(f154,plain,(
% 228.22/29.29 ![X0,X1,X2,X3,X4]: (~sum(X0,X1,X2)|~product(additive_identity,X1,X3)|~sum(X0,X3,X4)|product(X0,X2,X4))),
% 228.22/29.29 inference(resolution,[status(thm)],[f45,f33])).
% 228.22/29.29 fof(f156,plain,(
% 228.22/29.29 ![X0,X1,X2,X3,X4,X5]: (~sum(X0,X1,X2)|~product(X3,X1,X4)|~sum(X0,X4,X5)|product(add(X0,X3),X2,X5))),
% 228.22/29.29 inference(resolution,[status(thm)],[f45,f28])).
% 228.22/29.29 fof(f163,plain,(
% 228.22/29.29 ![X0,X1,X2,X3,X4]: (~sum(additive_identity,X0,X1)|~product(X2,X0,X3)|~product(X2,X1,X4)|sum(additive_identity,X3,X4))),
% 228.22/29.29 inference(resolution,[status(thm)],[f47,f32])).
% 228.22/29.29 fof(f178,plain,(
% 228.22/29.29 ![X0,X1,X2,X3]: (~sum(X0,z,X1)|~product(x_plus_y,X0,X2)|~sum(X2,z,X3)|product(x_plus_y__plus_z,X1,X3))),
% 228.22/29.29 inference(resolution,[status(thm)],[f49,f63])).
% 228.22/29.29 fof(f180,plain,(
% 228.22/29.29 ![X0,X1,X2,X3]: (~sum(X0,y_plus_z,X1)|~product(x,X0,X2)|~sum(X2,y_plus_z,X3)|product(x__plus_y_plus_z,X1,X3))),
% 228.22/29.29 inference(resolution,[status(thm)],[f49,f61])).
% 228.22/29.29 fof(f186,plain,(
% 228.22/29.29 x__plus_y_plus_z=add(x,y_plus_z)),
% 228.22/29.29 inference(resolution,[status(thm)],[f109,f73])).
% 228.22/29.29 fof(f192,plain,(
% 228.22/29.29 x_plus_y__plus_z=add(x_plus_y,z)),
% 228.22/29.29 inference(resolution,[status(thm)],[f116,f28])).
% 228.22/29.29 fof(f211,plain,(
% 228.22/29.29 y_plus_z=add(y,z)),
% 228.22/29.29 inference(resolution,[status(thm)],[f110,f73])).
% 228.22/29.29 fof(f218,plain,(
% 228.22/29.29 x_plus_y=add(x,y)),
% 228.22/29.29 inference(resolution,[status(thm)],[f112,f73])).
% 228.22/29.29 fof(f239,plain,(
% 228.22/29.29 ![X0,X1]: (~product(multiplicative_identity,X0,X1)|X0=X1)),
% 228.22/29.29 inference(resolution,[status(thm)],[f59,f34])).
% 228.22/29.29 fof(f241,plain,(
% 228.22/29.29 ![X0,X1]: (~product(X0,multiplicative_identity,X1)|X0=X1)),
% 228.22/29.29 inference(resolution,[status(thm)],[f59,f35])).
% 228.22/29.29 fof(f242,plain,(
% 228.22/29.29 ![X0,X1,X2]: (~product(X0,X1,X2)|multiply(X1,X0)=X2)),
% 228.22/29.29 inference(resolution,[status(thm)],[f59,f78])).
% 228.22/29.29 fof(f243,plain,(
% 228.22/29.29 ![X0,X1,X2]: (~product(X0,X1,X2)|multiply(X0,X1)=X2)),
% 228.22/29.29 inference(resolution,[status(thm)],[f59,f29])).
% 228.22/29.29 fof(f255,plain,(
% 228.22/29.29 ![X0,X1]: (~product(y_plus_z,y,X0)|~sum(x,X0,X1)|product(x__plus_y_plus_z,x_plus_y,X1))),
% 228.22/29.29 inference(resolution,[status(thm)],[f152,f62])).
% 228.22/29.29 fof(f258,plain,(
% 228.22/29.29 ![X0,X1]: (~product(y_plus_z,additive_identity,X0)|~sum(x,X0,X1)|product(x__plus_y_plus_z,x,X1))),
% 228.22/29.29 inference(resolution,[status(thm)],[f152,f33])).
% 228.22/29.29 fof(f260,plain,(
% 228.22/29.29 ![X0,X1,X2]: (~product(y_plus_z,X0,X1)|~sum(x,X1,X2)|product(x__plus_y_plus_z,add(x,X0),X2))),
% 228.22/29.29 inference(resolution,[status(thm)],[f152,f28])).
% 228.22/29.29 fof(f327,plain,(
% 228.22/29.29 ![X0,X1,X2,X3]: (~sum(inverse(X0),X1,X2)|~product(X0,X2,X3)|sum(additive_identity,multiply(X1,X0),X3))),
% 228.22/29.29 inference(resolution,[status(thm)],[f81,f78])).
% 228.22/29.29 fof(f345,plain,(
% 228.22/29.29 ![X0,X1]: (~product(x_plus_y,y,X0)|~sum(X0,z,X1)|product(x_plus_y__plus_z,y_plus_z,X1))),
% 228.22/29.29 inference(resolution,[status(thm)],[f178,f60])).
% 228.22/29.29 fof(f370,plain,(
% 228.22/29.29 ![X0,X1]: (~product(x,additive_identity,X0)|~sum(X0,y_plus_z,X1)|product(x__plus_y_plus_z,y_plus_z,X1))),
% 228.22/29.29 inference(resolution,[status(thm)],[f180,f32])).
% 228.22/29.29 fof(f373,plain,(
% 228.22/29.29 ![X0,X1,X2]: (~product(x,X0,X1)|~sum(X1,y_plus_z,X2)|product(x__plus_y_plus_z,add(X0,y_plus_z),X2))),
% 228.22/29.29 inference(resolution,[status(thm)],[f180,f28])).
% 228.22/29.29 fof(f422,plain,(
% 228.22/29.29 ![X0,X1]: (add(X0,X1)=add(X1,X0))),
% 228.22/29.29 inference(resolution,[status(thm)],[f121,f28])).
% 228.22/29.29 fof(f427,plain,(
% 228.22/29.29 ![X0,X1,X2,X3,X4]: (~sum(X0,X1,X2)|~product(X3,X2,X4)|sum(multiply(X3,X0),multiply(X1,X3),X4))),
% 228.22/29.29 inference(resolution,[status(thm)],[f83,f78])).
% 228.22/29.29 fof(f428,plain,(
% 228.22/29.29 ![X0,X1,X2,X3,X4]: (~sum(X0,X1,X2)|~product(X3,X2,X4)|sum(multiply(X3,X0),multiply(X3,X1),X4))),
% 228.22/29.29 inference(resolution,[status(thm)],[f83,f29])).
% 228.22/29.29 fof(f434,plain,(
% 228.22/29.29 ![X0,X1,X2,X3]: (~sum(X0,X1,X2)|~sum(additive_identity,multiply(inverse(X0),X1),X3)|product(inverse(X0),X2,X3))),
% 228.22/29.29 inference(resolution,[status(thm)],[f86,f29])).
% 228.22/29.29 fof(f557,plain,(
% 228.22/29.29 ![X0,X1,X2]: (~sum(inverse(X0),multiplicative_identity,X1)|~sum(additive_identity,X0,X2)|product(X0,X1,X2))),
% 228.22/29.29 inference(resolution,[status(thm)],[f88,f35])).
% 228.22/29.29 fof(f571,plain,(
% 228.22/29.29 ![X0,X1,X2,X3,X4]: (~sum(X0,X1,X2)|~sum(multiply(X3,X0),multiply(X1,X3),X4)|product(X3,X2,X4))),
% 228.22/29.29 inference(resolution,[status(thm)],[f90,f78])).
% 228.22/29.29 fof(f652,plain,(
% 228.22/29.29 ![X0,X1]: (multiply(X0,X1)=multiply(X1,X0))),
% 228.22/29.29 inference(resolution,[status(thm)],[f242,f29])).
% 228.22/29.29 fof(f927,plain,(
% 228.22/29.29 ![X0,X1,X2,X3]: (~sum(multiplicative_identity,X0,X1)|~sum(X2,multiply(X2,X0),X3)|product(X1,X2,X3))),
% 228.22/29.29 inference(resolution,[status(thm)],[f104,f78])).
% 228.22/29.29 fof(f949,plain,(
% 228.22/29.29 ![X0]: (~sum(x,multiply(y_plus_z,y),X0)|product(x__plus_y_plus_z,x_plus_y,X0))),
% 228.22/29.29 inference(resolution,[status(thm)],[f255,f29])).
% 228.22/29.29 fof(f1039,plain,(
% 228.22/29.29 ![X0,X1]: (~product(z,additive_identity,X0)|~sum(y,X0,X1)|product(y_plus_z,y,X1))),
% 228.22/29.29 inference(resolution,[status(thm)],[f147,f33])).
% 228.22/29.29 fof(f1062,plain,(
% 228.22/29.29 ![X0]: (~sum(x,multiply(y_plus_z,additive_identity),X0)|product(x__plus_y_plus_z,x,X0))),
% 228.22/29.29 inference(resolution,[status(thm)],[f258,f29])).
% 228.22/29.29 fof(f1100,plain,(
% 228.22/29.29 ![X0,X1]: (~sum(x,multiply(y_plus_z,X0),X1)|product(x__plus_y_plus_z,add(x,X0),X1))),
% 228.22/29.29 inference(resolution,[status(thm)],[f260,f29])).
% 228.22/29.29 fof(f1183,plain,(
% 228.22/29.29 ![X0,X1]: (~product(y,additive_identity,X0)|~sum(x,X0,X1)|product(x_plus_y,x,X1))),
% 228.22/29.29 inference(resolution,[status(thm)],[f151,f33])).
% 228.22/29.29 fof(f1630,plain,(
% 228.22/29.29 ![X0,X1]: (~product(additive_identity,y,X0)|~sum(z,X0,X1)|product(z,y_plus_z,X1))),
% 228.22/29.29 inference(resolution,[status(thm)],[f154,f65])).
% 228.22/29.29 fof(f1632,plain,(
% 228.22/29.29 ![X0,X1]: (~product(additive_identity,x,X0)|~sum(y,X0,X1)|product(y,x_plus_y,X1))),
% 228.22/29.29 inference(resolution,[status(thm)],[f154,f69])).
% 228.22/29.29 fof(f1645,plain,(
% 228.22/29.29 ![X0,X1,X2,X3]: (~product(additive_identity,X0,X1)|~sum(X2,X1,X3)|product(X2,add(X0,X2),X3))),
% 228.22/29.29 inference(resolution,[status(thm)],[f154,f73])).
% 228.22/29.29 fof(f1662,plain,(
% 228.22/29.29 ![X0,X1,X2]: (~product(X0,z,X1)|~sum(x_plus_y,X1,X2)|product(add(x_plus_y,X0),x_plus_y__plus_z,X2))),
% 228.22/29.29 inference(resolution,[status(thm)],[f156,f63])).
% 228.22/29.29 fof(f1913,plain,(
% 228.22/29.29 ![X0,X1,X2,X3]: (~product(X0,X1,X2)|~product(X0,X1,X3)|sum(additive_identity,X2,X3))),
% 228.22/29.29 inference(resolution,[status(thm)],[f163,f32])).
% 228.22/29.29 fof(f2249,plain,(
% 228.22/29.29 ![X0]: (~sum(multiply(y,x_plus_y),z,X0)|product(x_plus_y__plus_z,y_plus_z,X0))),
% 228.22/29.29 inference(resolution,[status(thm)],[f345,f78])).
% 228.22/29.29 fof(f2715,plain,(
% 228.22/29.29 ![X0]: (~sum(multiply(x,additive_identity),y_plus_z,X0)|product(x__plus_y_plus_z,y_plus_z,X0))),
% 228.22/29.29 inference(resolution,[status(thm)],[f370,f29])).
% 228.22/29.29 fof(f2903,plain,(
% 228.22/29.29 ![X0,X1]: (~sum(multiply(X0,x),y_plus_z,X1)|product(x__plus_y_plus_z,add(X0,y_plus_z),X1))),
% 228.22/29.29 inference(resolution,[status(thm)],[f373,f78])).
% 228.22/29.29 fof(f3209,plain,(
% 228.22/29.29 ![X0,X1,X2]: (~product(X0,X1,X2)|sum(additive_identity,multiply(X1,X0),X2))),
% 228.22/29.29 inference(resolution,[status(thm)],[f1913,f78])).
% 228.22/29.29 fof(f3240,plain,(
% 228.22/29.29 ![X0,X1]: (sum(additive_identity,multiply(X0,X1),multiply(X1,X0)))),
% 228.22/29.29 inference(resolution,[status(thm)],[f3209,f29])).
% 228.22/29.29 fof(f3340,plain,(
% 228.22/29.29 ![X0,X1,X2]: (~sum(additive_identity,multiply(X0,X1),X2)|multiply(X1,X0)=X2)),
% 228.22/29.29 inference(resolution,[status(thm)],[f3240,f57])).
% 228.22/29.29 fof(f4086,plain,(
% 228.22/29.29 ![X0,X1]: (~sum(x_plus_y,multiply(X0,z),X1)|product(add(x_plus_y,X0),x_plus_y__plus_z,X1))),
% 228.22/29.29 inference(resolution,[status(thm)],[f1662,f29])).
% 228.22/29.29 fof(f4377,plain,(
% 228.22/29.29 ![X0,X1]: (~product(X0,multiplicative_identity,X1)|sum(additive_identity,multiply(inverse(inverse(X0)),X0),X1))),
% 228.22/29.29 inference(resolution,[status(thm)],[f327,f53])).
% 228.22/29.29 fof(f4378,plain,(
% 228.22/29.29 ![X0,X1]: (~product(X0,inverse(X0),X1)|sum(additive_identity,multiply(additive_identity,X0),X1))),
% 228.22/29.29 inference(resolution,[status(thm)],[f327,f33])).
% 228.22/29.29 fof(f4912,plain,(
% 228.22/29.29 ![X0,X1,X2]: (~product(X0,multiplicative_identity,X1)|sum(multiply(X0,inverse(X2)),multiply(X2,X0),X1))),
% 228.22/29.29 inference(resolution,[status(thm)],[f427,f52])).
% 228.22/29.29 fof(f4952,plain,(
% 228.22/29.29 ![X0,X1,X2,X3]: (~product(X0,add(X1,X2),X3)|sum(multiply(X0,X1),multiply(X0,X2),X3))),
% 228.22/29.29 inference(resolution,[status(thm)],[f428,f28])).
% 228.22/29.29 fof(f5407,plain,(
% 228.22/29.29 ![X0,X1]: (~sum(additive_identity,multiply(inverse(inverse(X0)),X0),X1)|product(inverse(inverse(X0)),multiplicative_identity,X1))),
% 228.22/29.29 inference(resolution,[status(thm)],[f434,f52])).
% 228.22/29.29 fof(f6628,plain,(
% 228.22/29.29 ![X0,X1]: (~sum(additive_identity,X0,X1)|product(X0,add(inverse(X0),multiplicative_identity),X1))),
% 228.22/29.29 inference(resolution,[status(thm)],[f557,f28])).
% 228.22/29.29 fof(f6643,plain,(
% 228.22/29.29 product(x__plus_y_plus_z,x_plus_y,add(x,multiply(y_plus_z,y)))),
% 228.22/29.29 inference(resolution,[status(thm)],[f949,f28])).
% 228.22/29.29 fof(f6710,plain,(
% 228.22/29.29 multiply(x__plus_y_plus_z,x_plus_y)=add(x,multiply(y_plus_z,y))),
% 228.22/29.29 inference(resolution,[status(thm)],[f6643,f243])).
% 228.22/29.29 fof(f7377,plain,(
% 228.22/29.29 ![X0,X1]: (~sum(multiply(X0,z),multiply(x_plus_y,X0),X1)|product(X0,x_plus_y__plus_z,X1))),
% 228.22/29.29 inference(resolution,[status(thm)],[f571,f68])).
% 228.22/29.29 fof(f9240,plain,(
% 228.22/29.29 product(x__plus_y_plus_z,x,add(x,multiply(y_plus_z,additive_identity)))),
% 228.22/29.29 inference(resolution,[status(thm)],[f1062,f28])).
% 228.22/29.29 fof(f9319,plain,(
% 228.22/29.29 multiply(x,x__plus_y_plus_z)=add(x,multiply(y_plus_z,additive_identity))),
% 228.22/29.29 inference(resolution,[status(thm)],[f9240,f242])).
% 228.22/29.29 fof(f10912,plain,(
% 228.22/29.29 ![X0,X1,X2]: (~sum(X0,multiply(X0,X1),X2)|product(add(X1,multiplicative_identity),X0,X2))),
% 228.22/29.29 inference(resolution,[status(thm)],[f927,f73])).
% 228.22/29.29 fof(f11926,plain,(
% 228.22/29.29 ![X0]: (~sum(y,multiply(additive_identity,z),X0)|product(y_plus_z,y,X0))),
% 228.22/29.29 inference(resolution,[status(thm)],[f1039,f78])).
% 228.22/29.29 fof(f12457,plain,(
% 228.22/29.29 ![X0]: (product(x__plus_y_plus_z,add(x,X0),add(x,multiply(y_plus_z,X0))))),
% 228.22/29.29 inference(resolution,[status(thm)],[f1100,f28])).
% 228.22/29.29 fof(f12889,plain,(
% 228.22/29.29 ![X0]: (~sum(x,multiply(additive_identity,y),X0)|product(x_plus_y,x,X0))),
% 228.22/29.29 inference(resolution,[status(thm)],[f1183,f78])).
% 228.22/29.29 fof(f13710,plain,(
% 228.22/29.29 ![X0]: (~sum(z,multiply(y,additive_identity),X0)|product(z,y_plus_z,X0))),
% 228.22/29.29 inference(resolution,[status(thm)],[f1630,f78])).
% 228.22/29.29 fof(f13712,plain,(
% 228.22/29.29 ![X0]: (~sum(y,multiply(x,additive_identity),X0)|product(y,x_plus_y,X0))),
% 228.22/29.29 inference(resolution,[status(thm)],[f1632,f78])).
% 228.22/29.29 fof(f14136,plain,(
% 228.22/29.29 ![X0,X1]: (~sum(X0,additive_identity,X1)|product(X0,add(inverse(additive_identity),X0),X1))),
% 228.22/29.29 inference(resolution,[status(thm)],[f1645,f55])).
% 228.22/29.29 fof(f14142,plain,(
% 228.22/29.29 ![X0,X1]: (~sum(X0,additive_identity,X1)|product(X0,add(multiplicative_identity,X0),X1))),
% 228.22/29.29 inference(forward_demodulation,[status(thm)],[f124,f14136])).
% 228.22/29.29 fof(f14210,plain,(
% 228.22/29.29 product(x_plus_y__plus_z,y_plus_z,add(multiply(y,x_plus_y),z))),
% 228.22/29.29 inference(resolution,[status(thm)],[f2249,f28])).
% 228.22/29.29 fof(f15433,plain,(
% 228.22/29.29 product(x__plus_y_plus_z,y_plus_z,add(multiply(x,additive_identity),y_plus_z))),
% 228.22/29.29 inference(resolution,[status(thm)],[f2715,f28])).
% 228.22/29.29 fof(f16150,plain,(
% 228.22/29.29 ![X0]: (product(x__plus_y_plus_z,add(X0,y_plus_z),add(multiply(X0,x),y_plus_z)))),
% 228.22/29.29 inference(resolution,[status(thm)],[f2903,f28])).
% 228.22/29.29 fof(f18221,plain,(
% 228.22/29.29 multiply(y_plus_z,x_plus_y__plus_z)=add(multiply(y,x_plus_y),z)),
% 228.22/29.29 inference(resolution,[status(thm)],[f14210,f242])).
% 228.22/29.29 fof(f19337,plain,(
% 228.22/29.29 multiply(y_plus_z,x__plus_y_plus_z)=add(multiply(x,additive_identity),y_plus_z)),
% 228.22/29.29 inference(resolution,[status(thm)],[f15433,f242])).
% 228.22/29.29 fof(f20846,plain,(
% 228.22/29.29 ![X0]: (product(add(x_plus_y,X0),x_plus_y__plus_z,add(x_plus_y,multiply(X0,z))))),
% 228.22/29.29 inference(resolution,[status(thm)],[f4086,f28])).
% 228.22/29.29 fof(f29097,plain,(
% 228.22/29.29 ![X0]: (product(X0,add(multiplicative_identity,X0),X0))),
% 228.22/29.29 inference(resolution,[status(thm)],[f14142,f33])).
% 228.22/29.29 fof(f29237,plain,(
% 228.22/29.29 ![X0]: (multiply(X0,add(multiplicative_identity,X0))=X0)),
% 228.22/29.29 inference(resolution,[status(thm)],[f29097,f243])).
% 228.22/29.29 fof(f29492,plain,(
% 228.22/29.29 ![X0]: (multiply(X0,add(X0,multiplicative_identity))=X0)),
% 228.22/29.29 inference(paramodulation,[status(thm)],[f422,f29237])).
% 228.22/29.29 fof(f41227,plain,(
% 228.22/29.29 ![X0]: (product(X0,x_plus_y__plus_z,add(multiply(x_plus_y,X0),multiply(X0,z))))),
% 228.22/29.29 inference(resolution,[status(thm)],[f7377,f73])).
% 228.22/29.29 fof(f49481,plain,(
% 228.22/29.29 ![X0]: (sum(additive_identity,multiply(inverse(inverse(X0)),X0),X0))),
% 228.22/29.29 inference(resolution,[status(thm)],[f4377,f35])).
% 228.22/29.29 fof(f49684,plain,(
% 228.22/29.29 ![X0]: (sum(additive_identity,multiply(additive_identity,X0),additive_identity))),
% 228.22/29.29 inference(resolution,[status(thm)],[f4378,f55])).
% 228.22/29.29 fof(f49767,plain,(
% 228.22/29.29 ![X0]: (multiply(X0,additive_identity)=additive_identity)),
% 228.22/29.29 inference(resolution,[status(thm)],[f49684,f3340])).
% 228.22/29.29 fof(f49779,plain,(
% 228.22/29.29 ![X0]: (multiply(additive_identity,X0)=additive_identity)),
% 228.22/29.29 inference(resolution,[status(thm)],[f49684,f115])).
% 228.22/29.29 fof(f49907,plain,(
% 228.22/29.29 multiply(y_plus_z,x__plus_y_plus_z)=add(additive_identity,y_plus_z)),
% 228.22/29.29 inference(backward_demodulation,[status(thm)],[f49767,f19337])).
% 228.22/29.29 fof(f49924,plain,(
% 228.22/29.29 multiply(x,x__plus_y_plus_z)=add(x,additive_identity)),
% 228.22/29.29 inference(backward_demodulation,[status(thm)],[f49767,f9319])).
% 228.22/29.29 fof(f50073,plain,(
% 228.22/29.29 multiply(y_plus_z,x__plus_y_plus_z)=y_plus_z),
% 228.22/29.29 inference(forward_demodulation,[status(thm)],[f127,f49907])).
% 228.22/29.29 fof(f50075,plain,(
% 228.22/29.29 multiply(x,x__plus_y_plus_z)=x),
% 228.22/29.29 inference(forward_demodulation,[status(thm)],[f126,f49924])).
% 228.22/29.29 fof(f51299,plain,(
% 228.22/29.29 product(x__plus_y_plus_z,y_plus_z,y_plus_z)),
% 228.22/29.29 inference(paramodulation,[status(thm)],[f50073,f78])).
% 228.22/29.29 fof(f51384,plain,(
% 228.22/29.29 product(x__plus_y_plus_z,x,x)),
% 228.22/29.29 inference(paramodulation,[status(thm)],[f50075,f78])).
% 228.22/29.29 fof(f51756,plain,(
% 228.22/29.29 multiply(x__plus_y_plus_z,y_plus_z)=y_plus_z),
% 228.22/29.29 inference(resolution,[status(thm)],[f51299,f243])).
% 228.22/29.29 fof(f51946,plain,(
% 228.22/29.29 multiply(x__plus_y_plus_z,x)=x),
% 228.22/29.29 inference(resolution,[status(thm)],[f51384,f243])).
% 228.22/29.29 fof(f55235,plain,(
% 228.22/29.29 ![X0,X1]: (sum(multiply(X0,inverse(X1)),multiply(X1,X0),X0))),
% 228.22/29.29 inference(resolution,[status(thm)],[f4912,f35])).
% 228.22/29.29 fof(f58138,plain,(
% 228.22/29.29 ![X0]: (product(X0,add(inverse(X0),multiplicative_identity),X0))),
% 228.22/29.29 inference(resolution,[status(thm)],[f6628,f32])).
% 228.22/29.29 fof(f58579,plain,(
% 228.22/29.29 ![X0]: (multiply(add(inverse(X0),multiplicative_identity),X0)=X0)),
% 228.22/29.29 inference(resolution,[status(thm)],[f58138,f242])).
% 228.22/29.29 fof(f70539,plain,(
% 228.22/29.29 ![X0]: (product(inverse(inverse(X0)),multiplicative_identity,X0))),
% 228.22/29.29 inference(resolution,[status(thm)],[f49481,f5407])).
% 228.22/29.29 fof(f72332,plain,(
% 228.22/29.29 ![X0]: (inverse(inverse(X0))=X0)),
% 228.22/29.29 inference(resolution,[status(thm)],[f70539,f241])).
% 228.22/29.29 fof(f79986,plain,(
% 228.22/29.29 ![X0]: (sum(inverse(X0),multiply(X0,add(inverse(inverse(X0)),multiplicative_identity)),add(inverse(inverse(X0)),multiplicative_identity)))),
% 228.22/29.29 inference(paramodulation,[status(thm)],[f58579,f55235])).
% 228.22/29.29 fof(f80081,plain,(
% 228.22/29.29 ![X0]: (sum(inverse(X0),multiply(X0,add(X0,multiplicative_identity)),add(inverse(inverse(X0)),multiplicative_identity)))),
% 228.22/29.29 inference(forward_demodulation,[status(thm)],[f72332,f79986])).
% 228.22/29.29 fof(f80082,plain,(
% 228.22/29.29 ![X0]: (sum(inverse(X0),X0,add(inverse(inverse(X0)),multiplicative_identity)))),
% 228.22/29.29 inference(forward_demodulation,[status(thm)],[f29492,f80081])).
% 228.22/29.29 fof(f80083,plain,(
% 228.22/29.29 ![X0]: (sum(inverse(X0),X0,add(X0,multiplicative_identity)))),
% 228.22/29.29 inference(forward_demodulation,[status(thm)],[f72332,f80082])).
% 228.22/29.29 fof(f80130,plain,(
% 228.22/29.29 ![X0]: (multiplicative_identity=add(X0,multiplicative_identity))),
% 228.22/29.29 inference(resolution,[status(thm)],[f80083,f114])).
% 228.22/29.29 fof(f85410,plain,(
% 228.22/29.29 ![X0,X1,X2]: (~sum(X0,multiply(X0,X1),X2)|product(multiplicative_identity,X0,X2))),
% 228.22/29.29 inference(forward_demodulation,[status(thm)],[f80130,f10912])).
% 228.22/29.29 fof(f85426,plain,(
% 228.22/29.29 ![X0,X1]: (product(multiplicative_identity,X0,add(multiply(X0,X1),X0)))),
% 228.22/29.29 inference(resolution,[status(thm)],[f85410,f73])).
% 228.22/29.29 fof(f85812,plain,(
% 228.22/29.29 ![X0,X1]: (X0=add(multiply(X0,X1),X0))),
% 228.22/29.29 inference(resolution,[status(thm)],[f85426,f239])).
% 228.22/29.29 fof(f86371,plain,(
% 228.22/29.29 ![X0,X1]: (X0=add(X0,multiply(X0,X1)))),
% 228.22/29.29 inference(paramodulation,[status(thm)],[f422,f85812])).
% 228.22/29.29 fof(f86623,plain,(
% 228.22/29.29 ![X0,X1]: (X0=add(X0,multiply(X1,X0)))),
% 228.22/29.29 inference(paramodulation,[status(thm)],[f652,f86371])).
% 228.22/29.29 fof(f94053,plain,(
% 228.22/29.29 ![X0]: (~sum(y,additive_identity,X0)|product(y_plus_z,y,X0))),
% 228.22/29.29 inference(forward_demodulation,[status(thm)],[f49779,f11926])).
% 228.22/29.29 fof(f94054,plain,(
% 228.22/29.29 product(y_plus_z,y,y)),
% 228.22/29.29 inference(resolution,[status(thm)],[f94053,f33])).
% 228.22/29.29 fof(f94182,plain,(
% 228.22/29.29 multiply(y_plus_z,y)=y),
% 228.22/29.29 inference(resolution,[status(thm)],[f94054,f243])).
% 228.22/29.29 fof(f94226,plain,(
% 228.22/29.29 multiply(x__plus_y_plus_z,x_plus_y)=add(x,y)),
% 228.22/29.29 inference(backward_demodulation,[status(thm)],[f94182,f6710])).
% 228.22/29.29 fof(f94370,plain,(
% 228.22/29.29 multiply(x__plus_y_plus_z,x_plus_y)=x_plus_y),
% 228.22/29.29 inference(forward_demodulation,[status(thm)],[f218,f94226])).
% 228.22/29.29 fof(f97073,plain,(
% 228.22/29.29 ![X0]: (~sum(x,additive_identity,X0)|product(x_plus_y,x,X0))),
% 228.22/29.29 inference(forward_demodulation,[status(thm)],[f49779,f12889])).
% 228.22/29.29 fof(f97074,plain,(
% 228.22/29.29 product(x_plus_y,x,x)),
% 228.22/29.29 inference(resolution,[status(thm)],[f97073,f33])).
% 228.22/29.29 fof(f97216,plain,(
% 228.22/29.29 multiply(x_plus_y,x)=x),
% 228.22/29.29 inference(resolution,[status(thm)],[f97074,f243])).
% 228.22/29.29 fof(f97263,plain,(
% 228.22/29.29 product(x__plus_y_plus_z,add(x_plus_y,y_plus_z),add(x,y_plus_z))),
% 228.22/29.29 inference(paramodulation,[status(thm)],[f97216,f16150])).
% 228.22/29.29 fof(f97395,plain,(
% 228.22/29.29 product(x__plus_y_plus_z,add(x_plus_y,y_plus_z),x__plus_y_plus_z)),
% 228.22/29.29 inference(forward_demodulation,[status(thm)],[f186,f97263])).
% 228.22/29.29 fof(f101528,plain,(
% 228.22/29.29 ![X0]: (~sum(z,additive_identity,X0)|product(z,y_plus_z,X0))),
% 228.22/29.29 inference(forward_demodulation,[status(thm)],[f49767,f13710])).
% 228.22/29.29 fof(f101529,plain,(
% 228.22/29.29 product(z,y_plus_z,z)),
% 228.22/29.29 inference(resolution,[status(thm)],[f101528,f33])).
% 228.22/29.29 fof(f101535,plain,(
% 228.22/29.29 ![X0]: (~sum(y,additive_identity,X0)|product(y,x_plus_y,X0))),
% 15.52/29.35 inference(forward_demodulation,[status(thm)],[f49767,f13712])).
% 15.52/29.35 fof(f101536,plain,(
% 15.52/29.35 product(y,x_plus_y,y)),
% 15.52/29.35 inference(resolution,[status(thm)],[f101535,f33])).
% 15.52/29.35 fof(f102313,plain,(
% 15.52/29.35 multiply(y_plus_z,z)=z),
% 15.52/29.35 inference(resolution,[status(thm)],[f101529,f242])).
% 15.52/29.35 fof(f102424,plain,(
% 15.52/29.35 multiply(y,x_plus_y)=y),
% 15.52/29.35 inference(resolution,[status(thm)],[f101536,f243])).
% 15.52/29.35 fof(f103947,plain,(
% 15.52/29.35 multiply(y_plus_z,x_plus_y__plus_z)=add(y,z)),
% 15.52/29.35 inference(backward_demodulation,[status(thm)],[f102424,f18221])).
% 15.52/29.35 fof(f104098,plain,(
% 15.52/29.35 multiply(y_plus_z,x_plus_y__plus_z)=y_plus_z),
% 15.52/29.35 inference(forward_demodulation,[status(thm)],[f211,f103947])).
% 15.52/29.35 fof(f104676,plain,(
% 15.52/29.35 product(x__plus_y_plus_z,add(x,x_plus_y__plus_z),add(x,y_plus_z))),
% 15.52/29.35 inference(paramodulation,[status(thm)],[f104098,f12457])).
% 15.52/29.35 fof(f104803,plain,(
% 15.52/29.35 product(x__plus_y_plus_z,add(x,x_plus_y__plus_z),x__plus_y_plus_z)),
% 15.52/29.35 inference(forward_demodulation,[status(thm)],[f186,f104676])).
% 15.52/29.35 fof(f110018,plain,(
% 15.52/29.35 sum(multiply(x__plus_y_plus_z,x_plus_y),multiply(x__plus_y_plus_z,y_plus_z),x__plus_y_plus_z)),
% 15.52/29.35 inference(resolution,[status(thm)],[f97395,f4952])).
% 15.52/29.35 fof(f110096,plain,(
% 15.52/29.35 sum(x_plus_y,multiply(x__plus_y_plus_z,y_plus_z),x__plus_y_plus_z)),
% 15.52/29.35 inference(forward_demodulation,[status(thm)],[f94370,f110018])).
% 15.52/29.35 fof(f110097,plain,(
% 15.52/29.35 sum(x_plus_y,y_plus_z,x__plus_y_plus_z)),
% 15.52/29.35 inference(forward_demodulation,[status(thm)],[f51756,f110096])).
% 15.52/29.35 fof(f110164,plain,(
% 15.52/29.35 add(x_plus_y,y_plus_z)=x__plus_y_plus_z),
% 15.52/29.35 inference(resolution,[status(thm)],[f110097,f122])).
% 15.52/29.35 fof(f112234,plain,(
% 15.52/29.35 product(x__plus_y_plus_z,x_plus_y__plus_z,add(x_plus_y,multiply(y_plus_z,z)))),
% 15.52/29.35 inference(paramodulation,[status(thm)],[f110164,f20846])).
% 15.52/29.35 fof(f112348,plain,(
% 15.52/29.35 product(x__plus_y_plus_z,x_plus_y__plus_z,add(x_plus_y,z))),
% 15.52/29.35 inference(forward_demodulation,[status(thm)],[f102313,f112234])).
% 15.52/29.35 fof(f112349,plain,(
% 15.52/29.35 product(x__plus_y_plus_z,x_plus_y__plus_z,x_plus_y__plus_z)),
% 15.52/29.35 inference(forward_demodulation,[status(thm)],[f192,f112348])).
% 15.52/29.35 fof(f113879,plain,(
% 15.52/29.35 multiply(x__plus_y_plus_z,x_plus_y__plus_z)=x_plus_y__plus_z),
% 15.52/29.35 inference(resolution,[status(thm)],[f112349,f243])).
% 15.52/29.35 fof(f131573,plain,(
% 15.52/29.35 sum(multiply(x__plus_y_plus_z,x),multiply(x__plus_y_plus_z,x_plus_y__plus_z),x__plus_y_plus_z)),
% 15.52/29.35 inference(resolution,[status(thm)],[f104803,f4952])).
% 15.52/29.35 fof(f131653,plain,(
% 15.52/29.35 sum(x,multiply(x__plus_y_plus_z,x_plus_y__plus_z),x__plus_y_plus_z)),
% 15.52/29.35 inference(forward_demodulation,[status(thm)],[f51946,f131573])).
% 15.52/29.35 fof(f131654,plain,(
% 15.52/29.35 sum(x,x_plus_y__plus_z,x__plus_y_plus_z)),
% 15.52/29.35 inference(forward_demodulation,[status(thm)],[f113879,f131653])).
% 15.52/29.35 fof(f131784,plain,(
% 15.52/29.35 add(x_plus_y__plus_z,x)=x__plus_y_plus_z),
% 15.52/29.35 inference(resolution,[status(thm)],[f131654,f121])).
% 15.52/29.35 fof(f160023,plain,(
% 15.52/29.35 product(x,x_plus_y__plus_z,add(x,multiply(x,z)))),
% 15.52/29.35 inference(paramodulation,[status(thm)],[f97216,f41227])).
% 15.52/29.35 fof(f160515,plain,(
% 15.52/29.35 product(x,x_plus_y__plus_z,x)),
% 15.52/29.35 inference(forward_demodulation,[status(thm)],[f86371,f160023])).
% 15.52/29.35 fof(f165698,plain,(
% 15.52/29.35 multiply(x,x_plus_y__plus_z)=x),
% 15.52/29.35 inference(resolution,[status(thm)],[f160515,f243])).
% 15.52/29.35 fof(f168375,plain,(
% 15.52/29.35 x_plus_y__plus_z=add(x_plus_y__plus_z,x)),
% 15.52/29.35 inference(paramodulation,[status(thm)],[f165698,f86623])).
% 15.52/29.35 fof(f168533,plain,(
% 15.52/29.35 x_plus_y__plus_z=x__plus_y_plus_z),
% 15.52/29.35 inference(forward_demodulation,[status(thm)],[f131784,f168375])).
% 15.52/29.35 fof(f168534,plain,(
% 15.52/29.35 $false),
% 15.52/29.35 inference(forward_subsumption_resolution,[status(thm)],[f168533,f64])).
% 15.52/29.35 % SZS output end CNFRefutation for theBenchmark.p
% 15.52/29.36 % Elapsed time: 28.910267 seconds
% 15.52/29.36 % CPU time: 228.642287 seconds
% 15.52/29.36 % Total memory used: 352.239 MB
% 15.52/29.36 % Net memory used: 295.983 MB
%------------------------------------------------------------------------------