%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : BOO017-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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:46 PM UTC 2026
% Result : Unsatisfiable 109.24s 29.46s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO017-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/15.63 % CPULimit : 300
% 0.09/15.63 % WCLimit : 300
% 0.09/15.63 % DateTime : Mon Sep 21 13:48:30 UTC 2026
% 0.09/15.63 % CPUTime :
% 0.09/15.64 % Drodi V4.1.1
% 109.24/29.46 % Refutation found
% 109.24/29.46 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 109.24/29.46 % SZS output start CNFRefutation for theBenchmark
% 109.24/29.46 fof(f1,axiom,(
% 109.24/29.46 (![A,B,C]: (ifeq2(A,A,B,C) = B ))),
% 109.24/29.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 109.24/29.46 fof(f2,axiom,(
% 109.24/29.46 (![A,B,C]: (ifeq(A,A,B,C) = B ))),
% 109.24/29.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 109.24/29.46 fof(f3,axiom,(
% 109.24/29.46 (![X,Y]: (sum(X,Y,add(X,Y)) = true ))),
% 109.24/29.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 109.24/29.46 fof(f4,axiom,(
% 109.24/29.46 (![X,Y]: (product(X,Y,multiply(X,Y)) = true ))),
% 109.24/29.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 109.24/29.46 fof(f5,axiom,(
% 109.24/29.46 (![X,Y,Z]: (ifeq(sum(X,Y,Z),true,sum(Y,X,Z),true) = true ))),
% 109.24/29.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 109.24/29.46 fof(f6,axiom,(
% 109.24/29.46 (![X,Y,Z]: (ifeq(product(X,Y,Z),true,product(Y,X,Z),true) = true ))),
% 109.24/29.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 109.24/29.46 fof(f8,axiom,(
% 109.24/29.46 (![X]: (sum(X,additive_identity,X) = true ))),
% 109.24/29.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 109.24/29.46 fof(f9,axiom,(
% 109.24/29.46 (![X]: (product(multiplicative_identity,X,X) = true ))),
% 109.24/29.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 109.24/29.46 fof(f10,axiom,(
% 109.24/29.46 (![X]: (product(X,multiplicative_identity,X) = true ))),
% 109.24/29.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 109.24/29.46 fof(f13,axiom,(
% 109.24/29.46 (![V3,X,V4,Z,V2,Y,V1]: (ifeq(product(V3,X,V4),true,ifeq(product(Z,X,V2),true,ifeq(product(Y,X,V1),true,ifeq(sum(Y,Z,V3),true,sum(V1,V2,V4),true),true),true),true) = true ))),
% 109.24/29.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 109.24/29.46 fof(f14,axiom,(
% 109.24/29.46 (![Z,X,V2,Y,V1,V4,V3]: (ifeq(product(Z,X,V2),true,ifeq(product(Y,X,V1),true,ifeq(sum(V1,V2,V4),true,ifeq(sum(Y,Z,V3),true,product(V3,X,V4),true),true),true),true) = true ))),
% 109.24/29.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 109.24/29.46 fof(f16,axiom,(
% 109.24/29.46 (![V1,V2,V4,Y,Z,V3,X]: (ifeq(product(V1,V2,V4),true,ifeq(product(Y,Z,V3),true,ifeq(sum(X,Z,V2),true,ifeq(sum(X,Y,V1),true,sum(X,V3,V4),true),true),true),true) = true ))),
% 109.24/29.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 109.24/29.46 fof(f19,axiom,(
% 109.24/29.46 (![X]: (sum(inverse(X),X,multiplicative_identity) = true ))),
% 109.24/29.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 109.24/29.46 fof(f20,axiom,(
% 109.24/29.46 (![X]: (sum(X,inverse(X),multiplicative_identity) = true ))),
% 109.24/29.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 109.24/29.46 fof(f21,axiom,(
% 109.24/29.46 (![X]: (product(inverse(X),X,additive_identity) = true ))),
% 109.24/29.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 109.24/29.46 fof(f22,axiom,(
% 109.24/29.46 (![X]: (product(X,inverse(X),additive_identity) = true ))),
% 109.24/29.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 109.24/29.46 fof(f23,axiom,(
% 109.24/29.46 (![X,Y,V,U]: (ifeq2(sum(X,Y,V),true,ifeq2(sum(X,Y,U),true,U,V),V) = V ))),
% 109.24/29.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 109.24/29.46 fof(f24,axiom,(
% 109.24/29.46 (![X,Y,V,U]: (ifeq2(product(X,Y,V),true,ifeq2(product(X,Y,U),true,U,V),V) = V ))),
% 109.24/29.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 109.24/29.46 fof(f25,hypothesis,(
% 109.24/29.46 sum(x,y,z) = true ),
% 109.24/29.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 109.24/29.46 fof(f26,negated_conjecture,(
% 109.24/29.46 product(x,z,x) != true ),
% 109.24/29.46 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 109.24/29.46 fof(f27,plain,(
% 109.24/29.46 ![X0,X1,X2]: (ifeq2(X0,X0,X1,X2)=X1)),
% 109.24/29.46 inference(cnf_transformation,[status(thm)],[f1])).
% 109.24/29.46 fof(f28,plain,(
% 109.24/29.46 ![X0,X1,X2]: (ifeq(X0,X0,X1,X2)=X1)),
% 109.24/29.46 inference(cnf_transformation,[status(thm)],[f2])).
% 109.24/29.46 fof(f29,plain,(
% 109.24/29.46 ![X0,X1]: (sum(X0,X1,add(X0,X1))=true)),
% 109.24/29.46 inference(cnf_transformation,[status(thm)],[f3])).
% 109.24/29.46 fof(f30,plain,(
% 109.24/29.46 ![X0,X1]: (product(X0,X1,multiply(X0,X1))=true)),
% 109.24/29.46 inference(cnf_transformation,[status(thm)],[f4])).
% 109.24/29.46 fof(f31,plain,(
% 109.24/29.46 ![X0,X1,X2]: (ifeq(sum(X0,X1,X2),true,sum(X1,X0,X2),true)=true)),
% 109.24/29.46 inference(cnf_transformation,[status(thm)],[f5])).
% 109.24/29.46 fof(f32,plain,(
% 109.24/29.46 ![X0,X1,X2]: (ifeq(product(X0,X1,X2),true,product(X1,X0,X2),true)=true)),
% 109.24/29.46 inference(cnf_transformation,[status(thm)],[f6])).
% 109.24/29.46 fof(f34,plain,(
% 109.24/29.46 ![X0]: (sum(X0,additive_identity,X0)=true)),
% 109.24/29.46 inference(cnf_transformation,[status(thm)],[f8])).
% 109.24/29.46 fof(f35,plain,(
% 109.24/29.46 ![X0]: (product(multiplicative_identity,X0,X0)=true)),
% 109.24/29.46 inference(cnf_transformation,[status(thm)],[f9])).
% 109.24/29.46 fof(f36,plain,(
% 109.24/29.46 ![X0]: (product(X0,multiplicative_identity,X0)=true)),
% 109.24/29.46 inference(cnf_transformation,[status(thm)],[f10])).
% 109.24/29.46 fof(f39,plain,(
% 109.24/29.46 ![X0,X1,X2,X3,X4,X5,X6]: (ifeq(product(X0,X1,X2),true,ifeq(product(X3,X1,X4),true,ifeq(product(X5,X1,X6),true,ifeq(sum(X5,X3,X0),true,sum(X6,X4,X2),true),true),true),true)=true)),
% 109.24/29.46 inference(cnf_transformation,[status(thm)],[f13])).
% 109.24/29.46 fof(f40,plain,(
% 109.24/29.46 ![X0,X1,X2,X3,X4,X5,X6]: (ifeq(product(X0,X1,X2),true,ifeq(product(X3,X1,X4),true,ifeq(sum(X4,X2,X5),true,ifeq(sum(X3,X0,X6),true,product(X6,X1,X5),true),true),true),true)=true)),
% 109.24/29.46 inference(cnf_transformation,[status(thm)],[f14])).
% 109.24/29.46 fof(f42,plain,(
% 109.24/29.46 ![X0,X1,X2,X3,X4,X5,X6]: (ifeq(product(X0,X1,X2),true,ifeq(product(X3,X4,X5),true,ifeq(sum(X6,X4,X1),true,ifeq(sum(X6,X3,X0),true,sum(X6,X5,X2),true),true),true),true)=true)),
% 109.24/29.46 inference(cnf_transformation,[status(thm)],[f16])).
% 109.24/29.46 fof(f45,plain,(
% 109.24/29.46 ![X0]: (sum(inverse(X0),X0,multiplicative_identity)=true)),
% 109.24/29.46 inference(cnf_transformation,[status(thm)],[f19])).
% 109.24/29.46 fof(f46,plain,(
% 109.24/29.46 ![X0]: (sum(X0,inverse(X0),multiplicative_identity)=true)),
% 109.24/29.46 inference(cnf_transformation,[status(thm)],[f20])).
% 109.24/29.46 fof(f47,plain,(
% 109.24/29.46 ![X0]: (product(inverse(X0),X0,additive_identity)=true)),
% 109.24/29.46 inference(cnf_transformation,[status(thm)],[f21])).
% 109.24/29.46 fof(f48,plain,(
% 109.24/29.46 ![X0]: (product(X0,inverse(X0),additive_identity)=true)),
% 109.24/29.46 inference(cnf_transformation,[status(thm)],[f22])).
% 109.24/29.46 fof(f49,plain,(
% 109.24/29.46 ![X0,X1,X2,X3]: (ifeq2(sum(X0,X1,X2),true,ifeq2(sum(X0,X1,X3),true,X3,X2),X2)=X2)),
% 109.24/29.46 inference(cnf_transformation,[status(thm)],[f23])).
% 109.24/29.46 fof(f50,plain,(
% 109.24/29.46 ![X0,X1,X2,X3]: (ifeq2(product(X0,X1,X2),true,ifeq2(product(X0,X1,X3),true,X3,X2),X2)=X2)),
% 109.24/29.46 inference(cnf_transformation,[status(thm)],[f24])).
% 109.24/29.46 fof(f51,plain,(
% 109.24/29.46 sum(x,y,z)=true),
% 109.24/29.46 inference(cnf_transformation,[status(thm)],[f25])).
% 109.24/29.46 fof(f52,plain,(
% 109.24/29.46 ~product(x,z,x)=true),
% 109.24/29.46 inference(cnf_transformation,[status(thm)],[f26])).
% 109.24/29.46 fof(f71,plain,(
% 109.24/29.46 ![X0,X1,X2,X3,X4]: (ifeq(product(X0,X1,X2),true,ifeq(true,true,ifeq(product(X3,X1,X4),true,ifeq(sum(X3,multiplicative_identity,X0),true,sum(X4,X1,X2),true),true),true),true)=true)),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f35,f39])).
% 109.24/29.46 fof(f72,plain,(
% 109.24/29.46 ![X0,X1,X2,X3,X4]: (ifeq(true,true,ifeq(product(X0,X1,X2),true,ifeq(product(X3,X1,X4),true,ifeq(sum(X3,X0,multiplicative_identity),true,sum(X4,X2,X1),true),true),true),true)=true)),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f35,f39])).
% 109.24/29.46 fof(f74,plain,(
% 109.24/29.46 ![X0,X1,X2,X3,X4]: (ifeq(true,true,ifeq(product(X0,X1,X2),true,ifeq(sum(X3,X1,X4),true,ifeq(sum(X3,X0,multiplicative_identity),true,sum(X3,X2,X4),true),true),true),true)=true)),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f35,f42])).
% 109.24/29.46 fof(f91,plain,(
% 109.24/29.46 ![X0,X1,X2,X3,X4]: (ifeq(product(X0,X1,X2),true,ifeq(product(X3,X1,X4),true,ifeq(sum(X3,multiplicative_identity,X0),true,sum(X4,X1,X2),true),true),true)=true)),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f28,f71])).
% 109.24/29.46 fof(f92,plain,(
% 109.24/29.46 ![X0,X1,X2,X3,X4]: (ifeq(product(X0,X1,X2),true,ifeq(product(X3,X1,X4),true,ifeq(sum(X3,X0,multiplicative_identity),true,sum(X4,X2,X1),true),true),true)=true)),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f28,f72])).
% 109.24/29.46 fof(f94,plain,(
% 109.24/29.46 ![X0,X1,X2,X3,X4]: (ifeq(product(X0,X1,X2),true,ifeq(sum(X3,X1,X4),true,ifeq(sum(X3,X0,multiplicative_identity),true,sum(X3,X2,X4),true),true),true)=true)),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f28,f74])).
% 109.24/29.46 fof(f259,plain,(
% 109.24/29.46 ![X0,X1,X2,X3,X4,X5]: (ifeq(product(X0,X1,X2),true,ifeq(true,true,ifeq(sum(multiply(X3,X1),X2,X4),true,ifeq(sum(X3,X0,X5),true,product(X5,X1,X4),true),true),true),true)=true)),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f30,f40])).
% 109.24/29.46 fof(f275,plain,(
% 109.24/29.46 ![X0,X1]: (ifeq(true,true,product(X0,X1,multiply(X1,X0)),true)=true)),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f30,f32])).
% 109.24/29.46 fof(f290,plain,(
% 109.24/29.46 ![X0,X1,X2,X3,X4,X5]: (ifeq(product(X0,X1,X2),true,ifeq(sum(multiply(X3,X1),X2,X4),true,ifeq(sum(X3,X0,X5),true,product(X5,X1,X4),true),true),true)=true)),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f28,f259])).
% 109.24/29.46 fof(f304,plain,(
% 109.24/29.46 ![X0,X1]: (product(X0,X1,multiply(X1,X0))=true)),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f28,f275])).
% 109.24/29.46 fof(f513,plain,(
% 109.24/29.46 ![X0,X1,X2]: (ifeq2(product(X0,X1,X2),true,ifeq2(true,true,multiply(X1,X0),X2),X2)=X2)),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f304,f50])).
% 109.24/29.46 fof(f525,plain,(
% 109.24/29.46 ![X0,X1,X2]: (ifeq2(product(X0,X1,X2),true,multiply(X1,X0),X2)=X2)),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f27,f513])).
% 109.24/29.46 fof(f550,plain,(
% 109.24/29.46 ![X0]: (ifeq2(true,true,multiply(multiplicative_identity,X0),X0)=X0)),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f36,f525])).
% 109.24/29.46 fof(f559,plain,(
% 109.24/29.46 ![X0]: (multiply(multiplicative_identity,X0)=X0)),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f27,f550])).
% 109.24/29.46 fof(f788,plain,(
% 109.24/29.46 ifeq(true,true,sum(y,x,z),true)=true),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f51,f31])).
% 109.24/29.46 fof(f790,plain,(
% 109.24/29.46 ![X0,X1]: (ifeq(true,true,sum(X0,X1,add(X1,X0)),true)=true)),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f29,f31])).
% 109.24/29.46 fof(f804,plain,(
% 109.24/29.46 sum(y,x,z)=true),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f28,f788])).
% 109.24/29.46 fof(f806,plain,(
% 109.24/29.46 ![X0,X1]: (sum(X0,X1,add(X1,X0))=true)),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f28,f790])).
% 109.24/29.46 fof(f1526,plain,(
% 109.24/29.46 ![X0,X1,X2,X3]: (ifeq(product(X0,X1,X2),true,ifeq(product(inverse(X0),X1,X3),true,ifeq(true,true,sum(X3,X2,X1),true),true),true)=true)),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f45,f92])).
% 109.24/29.46 fof(f1574,plain,(
% 109.24/29.46 ![X0,X1,X2,X3]: (ifeq(product(X0,X1,X2),true,ifeq(product(inverse(X0),X1,X3),true,sum(X3,X2,X1),true),true)=true)),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f28,f1526])).
% 109.24/29.46 fof(f1608,plain,(
% 109.24/29.46 ![X0,X1]: (ifeq(true,true,ifeq(product(inverse(inverse(X0)),X0,X1),true,sum(X1,additive_identity,X0),true),true)=true)),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f47,f1574])).
% 109.24/29.46 fof(f1626,plain,(
% 109.24/29.46 ![X0,X1]: (ifeq(product(inverse(inverse(X0)),X0,X1),true,sum(X1,additive_identity,X0),true)=true)),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f28,f1608])).
% 109.24/29.46 fof(f1655,plain,(
% 109.24/29.46 ![X0]: (ifeq(true,true,sum(multiply(X0,inverse(inverse(X0))),additive_identity,X0),true)=true)),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f304,f1626])).
% 109.24/29.46 fof(f1667,plain,(
% 109.24/29.46 ![X0]: (sum(multiply(X0,inverse(inverse(X0))),additive_identity,X0)=true)),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f28,f1655])).
% 109.24/29.46 fof(f1800,plain,(
% 109.24/29.46 ![X0,X1,X2,X3]: (ifeq(product(add(multiplicative_identity,X0),X1,X2),true,ifeq(product(X0,X1,X3),true,ifeq(true,true,sum(X3,X1,X2),true),true),true)=true)),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f806,f91])).
% 109.24/29.46 fof(f1851,plain,(
% 109.24/29.46 ![X0,X1,X2,X3]: (ifeq(product(add(multiplicative_identity,X0),X1,X2),true,ifeq(product(X0,X1,X3),true,sum(X3,X1,X2),true),true)=true)),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f28,f1800])).
% 109.24/29.46 fof(f1931,plain,(
% 109.24/29.46 ![X0,X1,X2,X3]: (ifeq(product(inverse(X0),X1,X2),true,ifeq(product(X0,X1,X3),true,ifeq(true,true,sum(X3,X2,X1),true),true),true)=true)),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f46,f92])).
% 109.24/29.46 fof(f1994,plain,(
% 109.24/29.46 ![X0,X1,X2,X3]: (ifeq(product(inverse(X0),X1,X2),true,ifeq(product(X0,X1,X3),true,sum(X3,X2,X1),true),true)=true)),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f28,f1931])).
% 109.24/29.46 fof(f2037,plain,(
% 109.24/29.46 ![X0,X1]: (ifeq2(true,true,ifeq2(sum(X0,additive_identity,X1),true,X1,X0),X0)=X0)),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f34,f49])).
% 109.24/29.46 fof(f2040,plain,(
% 109.24/29.46 ![X0,X1]: (ifeq2(sum(inverse(X0),X0,X1),true,ifeq2(true,true,multiplicative_identity,X1),X1)=X1)),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f45,f49])).
% 109.24/29.46 fof(f2045,plain,(
% 109.24/29.46 ![X0,X1]: (ifeq2(sum(X0,additive_identity,X1),true,ifeq2(true,true,X0,X1),X1)=X1)),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f34,f49])).
% 109.24/29.46 fof(f2053,plain,(
% 109.24/29.46 ![X0,X1]: (ifeq2(sum(X0,additive_identity,X1),true,X1,X0)=X0)),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f27,f2037])).
% 109.24/29.46 fof(f2056,plain,(
% 109.24/29.46 ![X0,X1]: (ifeq2(sum(inverse(X0),X0,X1),true,multiplicative_identity,X1)=X1)),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f27,f2040])).
% 109.24/29.46 fof(f2061,plain,(
% 109.24/29.46 ![X0,X1]: (ifeq2(sum(X0,additive_identity,X1),true,X0,X1)=X1)),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f27,f2045])).
% 109.24/29.46 fof(f2154,plain,(
% 109.24/29.46 ![X0,X1]: (ifeq(true,true,ifeq(product(X0,X0,X1),true,sum(X1,additive_identity,X0),true),true)=true)),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f47,f1994])).
% 109.24/29.46 fof(f2155,plain,(
% 109.24/29.46 ![X0,X1]: (ifeq(true,true,ifeq(product(X0,inverse(inverse(X0)),X1),true,sum(X1,additive_identity,inverse(inverse(X0))),true),true)=true)),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f48,f1994])).
% 109.24/29.46 fof(f2180,plain,(
% 109.24/29.46 ![X0,X1]: (ifeq(product(X0,X0,X1),true,sum(X1,additive_identity,X0),true)=true)),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f28,f2154])).
% 109.24/29.46 fof(f2181,plain,(
% 109.24/29.46 ![X0,X1]: (ifeq(product(X0,inverse(inverse(X0)),X1),true,sum(X1,additive_identity,inverse(inverse(X0))),true)=true)),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f28,f2155])).
% 109.24/29.46 fof(f2200,plain,(
% 109.24/29.46 ![X0]: (ifeq(true,true,sum(multiply(X0,X0),additive_identity,X0),true)=true)),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f304,f2180])).
% 109.24/29.46 fof(f2216,plain,(
% 109.24/29.46 ![X0]: (sum(multiply(X0,X0),additive_identity,X0)=true)),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f28,f2200])).
% 109.24/29.46 fof(f2257,plain,(
% 109.24/29.46 ![X0,X1,X2,X3]: (ifeq(product(X0,X1,X2),true,ifeq(sum(inverse(X0),X1,X3),true,ifeq(true,true,sum(inverse(X0),X2,X3),true),true),true)=true)),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f45,f94])).
% 109.24/29.46 fof(f2288,plain,(
% 109.24/29.46 ![X0,X1,X2,X3]: (ifeq(product(X0,X1,X2),true,ifeq(sum(inverse(X0),X1,X3),true,sum(inverse(X0),X2,X3),true),true)=true)),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f28,f2257])).
% 109.24/29.46 fof(f2322,plain,(
% 109.24/29.46 ![X0]: (ifeq(true,true,sum(multiply(X0,inverse(inverse(X0))),additive_identity,inverse(inverse(X0))),true)=true)),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f30,f2181])).
% 109.24/29.46 fof(f2331,plain,(
% 109.24/29.46 ![X0]: (sum(multiply(X0,inverse(inverse(X0))),additive_identity,inverse(inverse(X0)))=true)),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f28,f2322])).
% 109.24/29.46 fof(f2415,plain,(
% 109.24/29.46 ![X0,X1,X2]: (ifeq(product(X0,X1,X2),true,ifeq(true,true,sum(inverse(X0),X2,add(X1,inverse(X0))),true),true)=true)),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f806,f2288])).
% 109.24/29.46 fof(f2436,plain,(
% 109.24/29.46 ![X0,X1,X2]: (ifeq(product(X0,X1,X2),true,sum(inverse(X0),X2,add(X1,inverse(X0))),true)=true)),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f28,f2415])).
% 109.24/29.46 fof(f2481,plain,(
% 109.24/29.46 ![X0]: (ifeq(true,true,sum(inverse(X0),X0,add(multiplicative_identity,inverse(X0))),true)=true)),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f36,f2436])).
% 109.24/29.46 fof(f2494,plain,(
% 109.24/29.46 ![X0]: (sum(inverse(X0),X0,add(multiplicative_identity,inverse(X0)))=true)),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f28,f2481])).
% 109.24/29.46 fof(f2909,plain,(
% 109.24/29.46 ![X0,X1,X2]: (ifeq(true,true,ifeq(product(X0,X1,X2),true,sum(X2,X1,multiply(add(multiplicative_identity,X0),X1)),true),true)=true)),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f30,f1851])).
% 109.24/29.46 fof(f2938,plain,(
% 109.24/29.46 ![X0,X1,X2]: (ifeq(product(X0,X1,X2),true,sum(X2,X1,multiply(add(multiplicative_identity,X0),X1)),true)=true)),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f28,f2909])).
% 109.24/29.46 fof(f3394,plain,(
% 109.24/29.46 ![X0]: (ifeq2(true,true,X0,multiply(X0,X0))=multiply(X0,X0))),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f2216,f2053])).
% 109.24/29.46 fof(f3472,plain,(
% 109.24/29.46 ![X0]: (X0=multiply(X0,X0))),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f27,f3394])).
% 109.24/29.46 fof(f3638,plain,(
% 109.24/29.46 ![X0]: (product(X0,X0,X0)=true)),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f3472,f304])).
% 109.24/29.46 fof(f6237,plain,(
% 109.24/29.46 ![X0]: (ifeq2(true,true,multiply(X0,inverse(inverse(X0))),X0)=X0)),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f1667,f2061])).
% 109.24/29.46 fof(f6336,plain,(
% 109.24/29.46 ![X0]: (sum(X0,additive_identity,inverse(inverse(X0)))=true)),
% 109.24/29.46 inference(backward_demodulation,[status(thm)],[f6340,f2331])).
% 109.24/29.46 fof(f6340,plain,(
% 109.24/29.46 ![X0]: (multiply(X0,inverse(inverse(X0)))=X0)),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f27,f6237])).
% 109.24/29.46 fof(f6881,plain,(
% 109.24/29.46 ![X0]: (ifeq2(true,true,X0,inverse(inverse(X0)))=inverse(inverse(X0)))),
% 109.24/29.46 inference(paramodulation,[status(thm)],[f6336,f2061])).
% 109.24/29.46 fof(f7113,plain,(
% 109.24/29.46 ![X0]: (X0=inverse(inverse(X0)))),
% 109.24/29.46 inference(forward_demodulation,[status(thm)],[f27,f6881])).
% 109.24/29.46 fof(f15385,plain,(
% 109.24/29.46 ![X0]: (ifeq2(true,true,multiplicative_identity,add(multiplicative_identity,inverse(X0)))=add(multiplicative_identity,inverse(X0)))),
% 110.21/29.54 inference(paramodulation,[status(thm)],[f2494,f2056])).
% 110.21/29.54 fof(f15560,plain,(
% 110.21/29.54 ![X0]: (multiplicative_identity=add(multiplicative_identity,inverse(X0)))),
% 110.21/29.54 inference(forward_demodulation,[status(thm)],[f27,f15385])).
% 110.21/29.54 fof(f15849,plain,(
% 110.21/29.54 ![X0]: (multiplicative_identity=add(multiplicative_identity,X0))),
% 110.21/29.54 inference(paramodulation,[status(thm)],[f7113,f15560])).
% 110.21/29.54 fof(f16093,plain,(
% 110.21/29.54 ![X0,X1,X2]: (ifeq(product(X0,X1,X2),true,sum(X2,X1,multiply(multiplicative_identity,X1)),true)=true)),
% 110.21/29.54 inference(backward_demodulation,[status(thm)],[f15849,f2938])).
% 110.21/29.54 fof(f16265,plain,(
% 110.21/29.54 ![X0,X1,X2]: (ifeq(product(X0,X1,X2),true,sum(X2,X1,X1),true)=true)),
% 110.21/29.54 inference(forward_demodulation,[status(thm)],[f559,f16093])).
% 110.21/29.54 fof(f16296,plain,(
% 110.21/29.54 ![X0,X1]: (ifeq(true,true,sum(multiply(X0,X1),X1,X1),true)=true)),
% 110.21/29.54 inference(paramodulation,[status(thm)],[f30,f16265])).
% 110.21/29.54 fof(f16330,plain,(
% 110.21/29.54 ![X0,X1]: (sum(multiply(X0,X1),X1,X1)=true)),
% 110.21/29.54 inference(forward_demodulation,[status(thm)],[f28,f16296])).
% 110.21/29.54 fof(f21037,plain,(
% 110.21/29.54 ![X0,X1,X2,X3]: (ifeq(product(X0,X1,X1),true,ifeq(true,true,ifeq(sum(X2,X0,X3),true,product(X3,X1,X1),true),true),true)=true)),
% 110.21/29.54 inference(paramodulation,[status(thm)],[f16330,f290])).
% 110.21/29.54 fof(f21093,plain,(
% 110.21/29.54 ![X0,X1,X2,X3]: (ifeq(product(X0,X1,X1),true,ifeq(sum(X2,X0,X3),true,product(X3,X1,X1),true),true)=true)),
% 110.21/29.54 inference(forward_demodulation,[status(thm)],[f28,f21037])).
% 110.21/29.54 fof(f22050,plain,(
% 110.21/29.54 ![X0]: (ifeq(product(x,X0,X0),true,ifeq(true,true,product(z,X0,X0),true),true)=true)),
% 110.21/29.54 inference(paramodulation,[status(thm)],[f804,f21093])).
% 110.21/29.54 fof(f22089,plain,(
% 110.21/29.54 ![X0]: (ifeq(product(x,X0,X0),true,product(z,X0,X0),true)=true)),
% 110.21/29.54 inference(forward_demodulation,[status(thm)],[f28,f22050])).
% 110.21/29.54 fof(f22102,plain,(
% 110.21/29.54 ifeq(true,true,product(z,x,x),true)=true),
% 110.21/29.54 inference(paramodulation,[status(thm)],[f3638,f22089])).
% 110.21/29.54 fof(f22104,plain,(
% 110.21/29.54 product(z,x,x)=true),
% 110.21/29.54 inference(forward_demodulation,[status(thm)],[f28,f22102])).
% 110.21/29.54 fof(f22776,plain,(
% 110.21/29.54 ifeq(true,true,product(x,z,x),true)=true),
% 110.21/29.54 inference(paramodulation,[status(thm)],[f22104,f32])).
% 110.21/29.54 fof(f22901,plain,(
% 110.21/29.54 product(x,z,x)=true),
% 110.21/29.54 inference(forward_demodulation,[status(thm)],[f28,f22776])).
% 110.21/29.54 fof(f22902,plain,(
% 110.21/29.54 $false),
% 110.21/29.54 inference(forward_subsumption_resolution,[status(thm)],[f22901,f52])).
% 110.21/29.54 % SZS output end CNFRefutation for theBenchmark.p
% 21.45/30.08 % Elapsed time: 14.428295 seconds
% 21.45/30.08 % CPU time: 113.289140 seconds
% 21.45/30.08 % Total memory used: 1.115 GB
% 21.45/30.08 % Net memory used: 1.089 GB
%------------------------------------------------------------------------------