%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : TOP049-1 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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 03:53:48 PM UTC 2026
% Result : Unsatisfiable 0.22s 0.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : TOP049-1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.48 % Computer : n006.cluster.edu
% 0.18/0.48 % Model : x86_64 x86_64
% 0.18/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.48 % Memory : 8046.5625MB
% 0.18/0.48 % OS : Linux 6.8.0-71-generic
% 0.18/0.48 % CPULimit : 300
% 0.18/0.48 % WCLimit : 300
% 0.18/0.48 % DateTime : Mon Sep 21 12:47:12 UTC 2026
% 0.18/0.49 % CPUTime :
% 0.18/0.51 % Drodi V4.1.1
% 0.22/0.56 % Refutation found
% 0.22/0.56 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.22/0.56 % SZS output start CNFRefutation for theBenchmark
% 0.22/0.56 fof(f1,axiom,(
% 0.22/0.56 (![X]: (product(X,X) = X ))),
% 0.22/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.56 fof(f2,axiom,(
% 0.22/0.56 (![X,Y]: (product(product(X,Y),Y) = X ))),
% 0.22/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.56 fof(f3,axiom,(
% 0.22/0.56 (![X,Y,Z]: (product(product(X,Y),Z) = product(product(X,Z),product(Y,Z)) ))),
% 0.22/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.56 fof(f4,axiom,(
% 0.22/0.56 a1 = product(a9,a7) ),
% 0.22/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.56 fof(f5,axiom,(
% 0.22/0.56 a3 = product(a1,a2) ),
% 0.22/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.56 fof(f6,axiom,(
% 0.22/0.56 a2 = product(a3,a4) ),
% 0.22/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.56 fof(f7,axiom,(
% 0.22/0.56 a5 = product(a2,a10) ),
% 0.22/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.56 fof(f8,axiom,(
% 0.22/0.56 a6 = product(a5,a4) ),
% 0.22/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.56 fof(f9,axiom,(
% 0.22/0.56 a7 = product(a6,a1) ),
% 0.22/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.56 fof(f10,axiom,(
% 0.22/0.56 a8 = product(a7,a4) ),
% 0.22/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.56 fof(f11,axiom,(
% 0.22/0.56 a10 = product(a8,a9) ),
% 0.22/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.56 fof(f12,axiom,(
% 0.22/0.56 a4 = product(a10,a3) ),
% 0.22/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.56 fof(f13,axiom,(
% 0.22/0.56 a9 = product(a4,a8) ),
% 0.22/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.56 fof(f14,negated_conjecture,(
% 0.22/0.56 tuple(a1,a9,a8,a6,a7,a2,a3,a4,a5) != tuple(a2,a10,a9,a7,a8,a3,a4,a5,a6) ),
% 0.22/0.56 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.22/0.56 fof(f15,plain,(
% 0.22/0.56 ![X0]: (product(X0,X0)=X0)),
% 0.22/0.56 inference(cnf_transformation,[status(thm)],[f1])).
% 0.22/0.56 fof(f16,plain,(
% 0.22/0.56 ![X0,X1]: (product(product(X0,X1),X1)=X0)),
% 0.22/0.56 inference(cnf_transformation,[status(thm)],[f2])).
% 0.22/0.56 fof(f17,plain,(
% 0.22/0.56 ![X0,X1,X2]: (product(product(X0,X1),X2)=product(product(X0,X2),product(X1,X2)))),
% 0.22/0.56 inference(cnf_transformation,[status(thm)],[f3])).
% 0.22/0.56 fof(f18,plain,(
% 0.22/0.56 a1=product(a9,a7)),
% 0.22/0.56 inference(cnf_transformation,[status(thm)],[f4])).
% 0.22/0.56 fof(f19,plain,(
% 0.22/0.56 a3=product(a1,a2)),
% 0.22/0.56 inference(cnf_transformation,[status(thm)],[f5])).
% 0.22/0.56 fof(f20,plain,(
% 0.22/0.56 a2=product(a3,a4)),
% 0.22/0.56 inference(cnf_transformation,[status(thm)],[f6])).
% 0.22/0.56 fof(f21,plain,(
% 0.22/0.56 a5=product(a2,a10)),
% 0.22/0.56 inference(cnf_transformation,[status(thm)],[f7])).
% 0.22/0.56 fof(f22,plain,(
% 0.22/0.56 a6=product(a5,a4)),
% 0.22/0.56 inference(cnf_transformation,[status(thm)],[f8])).
% 0.22/0.56 fof(f23,plain,(
% 0.22/0.56 a7=product(a6,a1)),
% 0.22/0.56 inference(cnf_transformation,[status(thm)],[f9])).
% 0.22/0.56 fof(f24,plain,(
% 0.22/0.56 a8=product(a7,a4)),
% 0.22/0.56 inference(cnf_transformation,[status(thm)],[f10])).
% 0.22/0.56 fof(f25,plain,(
% 0.22/0.56 a10=product(a8,a9)),
% 0.22/0.56 inference(cnf_transformation,[status(thm)],[f11])).
% 0.22/0.56 fof(f26,plain,(
% 0.22/0.56 a4=product(a10,a3)),
% 0.22/0.56 inference(cnf_transformation,[status(thm)],[f12])).
% 0.22/0.56 fof(f27,plain,(
% 0.22/0.56 a9=product(a4,a8)),
% 0.22/0.56 inference(cnf_transformation,[status(thm)],[f13])).
% 0.22/0.56 fof(f28,plain,(
% 0.22/0.56 ~tuple(a1,a9,a8,a6,a7,a2,a3,a4,a5)=tuple(a2,a10,a9,a7,a8,a3,a4,a5,a6)),
% 0.22/0.56 inference(cnf_transformation,[status(thm)],[f14])).
% 0.22/0.56 fof(f29,definition,(
% 0.22/0.56 sF0_fnc=tuple(a1,a9,a8,a6,a7,a2,a3,a4,a5)),
% 0.22/0.56 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 0.22/0.56 fof(f30,definition,(
% 0.22/0.56 sF1_fnc=tuple(a2,a10,a9,a7,a8,a3,a4,a5,a6)),
% 0.22/0.56 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 0.22/0.56 fof(f31,plain,(
% 0.22/0.56 ~sF0_fnc=sF1_fnc),
% 0.22/0.56 inference(definition_folding,[],[f28,f30,f29])).
% 0.22/0.56 fof(f33,plain,(
% 0.22/0.56 product(a9,a8)=a4),
% 0.22/0.56 inference(paramodulation,[status(thm)],[f27,f16])).
% 0.22/0.56 fof(f34,plain,(
% 0.22/0.56 product(a4,a3)=a10),
% 0.22/0.56 inference(paramodulation,[status(thm)],[f26,f16])).
% 0.22/0.56 fof(f35,plain,(
% 0.22/0.56 product(a10,a9)=a8),
% 0.22/0.56 inference(paramodulation,[status(thm)],[f25,f16])).
% 0.22/0.56 fof(f36,plain,(
% 0.22/0.56 product(a8,a4)=a7),
% 0.22/0.56 inference(paramodulation,[status(thm)],[f24,f16])).
% 0.22/0.56 fof(f37,plain,(
% 0.22/0.56 product(a7,a1)=a6),
% 0.22/0.56 inference(paramodulation,[status(thm)],[f23,f16])).
% 0.22/0.56 fof(f39,plain,(
% 0.22/0.56 product(a5,a10)=a2),
% 0.22/0.56 inference(paramodulation,[status(thm)],[f21,f16])).
% 0.22/0.56 fof(f40,plain,(
% 0.22/0.56 product(a2,a4)=a3),
% 0.22/0.56 inference(paramodulation,[status(thm)],[f20,f16])).
% 0.22/0.56 fof(f41,plain,(
% 0.22/0.56 product(a3,a2)=a1),
% 0.22/0.56 inference(paramodulation,[status(thm)],[f19,f16])).
% 0.22/0.56 fof(f56,plain,(
% 0.22/0.56 ![X0,X1,X2]: (product(product(product(X0,X1),X2),X1)=product(X0,product(X2,X1)))),
% 0.22/0.56 inference(paramodulation,[status(thm)],[f16,f17])).
% 0.22/0.56 fof(f58,plain,(
% 0.22/0.56 ![X0]: (product(product(a4,X0),a8)=product(a9,product(X0,a8)))),
% 0.22/0.56 inference(paramodulation,[status(thm)],[f27,f17])).
% 0.22/0.56 fof(f75,plain,(
% 0.22/0.56 ![X0]: (product(product(a9,X0),a8)=product(a4,product(X0,a8)))),
% 0.22/0.56 inference(paramodulation,[status(thm)],[f33,f17])).
% 0.22/0.56 fof(f76,plain,(
% 0.22/0.56 ![X0]: (product(product(a9,X0),a7)=product(a1,product(X0,a7)))),
% 0.22/0.56 inference(paramodulation,[status(thm)],[f18,f17])).
% 0.22/0.56 fof(f77,plain,(
% 0.22/0.56 ![X0,X1]: (product(product(X0,X1),X0)=product(X0,product(X1,X0)))),
% 0.22/0.56 inference(paramodulation,[status(thm)],[f15,f17])).
% 0.22/0.56 fof(f116,plain,(
% 0.22/0.56 product(a10,a4)=product(a4,product(a3,a4))),
% 0.22/0.56 inference(paramodulation,[status(thm)],[f34,f77])).
% 0.22/0.56 fof(f117,plain,(
% 0.22/0.56 product(a9,a4)=product(a4,product(a8,a4))),
% 0.22/0.56 inference(paramodulation,[status(thm)],[f27,f77])).
% 0.22/0.56 fof(f118,plain,(
% 0.22/0.56 product(a8,a10)=product(a10,product(a9,a10))),
% 0.22/0.56 inference(paramodulation,[status(thm)],[f35,f77])).
% 0.22/0.56 fof(f120,plain,(
% 0.22/0.56 product(a7,a8)=product(a8,product(a4,a8))),
% 0.22/0.56 inference(paramodulation,[status(thm)],[f36,f77])).
% 0.22/0.56 fof(f128,plain,(
% 0.22/0.56 product(a3,a2)=product(a2,product(a4,a2))),
% 0.22/0.56 inference(paramodulation,[status(thm)],[f40,f77])).
% 0.22/0.56 fof(f134,plain,(
% 0.22/0.56 product(a4,a9)=product(a9,product(a8,a9))),
% 0.22/0.56 inference(paramodulation,[status(thm)],[f33,f77])).
% 0.22/0.56 fof(f147,plain,(
% 0.22/0.56 product(a10,a4)=product(a4,a2)),
% 0.22/0.56 inference(forward_demodulation,[status(thm)],[f20,f116])).
% 0.22/0.56 fof(f148,plain,(
% 0.22/0.56 product(a9,a4)=product(a4,a7)),
% 0.22/0.56 inference(forward_demodulation,[status(thm)],[f36,f117])).
% 0.22/0.56 fof(f149,plain,(
% 0.22/0.56 product(a7,a8)=product(a8,a9)),
% 0.22/0.56 inference(forward_demodulation,[status(thm)],[f27,f120])).
% 0.22/0.56 fof(f150,plain,(
% 0.22/0.56 product(a7,a8)=a10),
% 0.22/0.56 inference(forward_demodulation,[status(thm)],[f25,f149])).
% 0.22/0.56 fof(f155,plain,(
% 0.22/0.56 a1=product(a2,product(a4,a2))),
% 0.22/0.56 inference(forward_demodulation,[status(thm)],[f41,f128])).
% 0.22/0.56 fof(f156,plain,(
% 0.22/0.56 a1=product(a2,product(a10,a4))),
% 0.22/0.56 inference(forward_demodulation,[status(thm)],[f147,f155])).
% 0.22/0.56 fof(f160,plain,(
% 0.22/0.56 product(a4,a9)=product(a9,a10)),
% 0.22/0.56 inference(forward_demodulation,[status(thm)],[f25,f134])).
% 0.22/0.56 fof(f169,plain,(
% 0.22/0.56 ![X0]: (product(product(X0,a7),a8)=product(product(X0,a8),a10))),
% 0.22/0.56 inference(paramodulation,[status(thm)],[f150,f17])).
% 0.22/0.56 fof(f189,plain,(
% 0.22/0.56 product(product(a9,a4),a7)=a4),
% 0.22/0.56 inference(paramodulation,[status(thm)],[f148,f16])).
% 0.22/0.56 fof(f193,plain,(
% 0.22/0.56 product(a1,product(a4,a7))=a4),
% 0.22/0.56 inference(forward_demodulation,[status(thm)],[f76,f189])).
% 0.22/0.56 fof(f194,plain,(
% 0.22/0.56 product(a1,product(a9,a4))=a4),
% 0.22/0.56 inference(forward_demodulation,[status(thm)],[f148,f193])).
% 0.22/0.56 fof(f207,plain,(
% 0.22/0.56 product(a1,product(a10,a4))=a2),
% 0.22/0.56 inference(paramodulation,[status(thm)],[f156,f16])).
% 0.22/0.56 fof(f506,plain,(
% 0.22/0.56 product(a4,product(a9,a4))=a1),
% 0.22/0.56 inference(paramodulation,[status(thm)],[f194,f16])).
% 0.22/0.57 fof(f565,plain,(
% 0.22/0.57 product(a1,a8)=product(a9,product(product(a9,a4),a8))),
% 0.22/0.57 inference(paramodulation,[status(thm)],[f506,f58])).
% 0.22/0.57 fof(f570,plain,(
% 0.22/0.57 product(a1,a4)=product(a4,product(product(a9,a4),a4))),
% 0.22/0.57 inference(paramodulation,[status(thm)],[f506,f77])).
% 0.22/0.57 fof(f574,plain,(
% 0.22/0.57 product(a1,a8)=product(a9,product(a4,product(a4,a8)))),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f75,f565])).
% 0.22/0.57 fof(f575,plain,(
% 0.22/0.57 product(a1,a8)=product(a9,product(a4,a9))),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f27,f574])).
% 0.22/0.57 fof(f576,plain,(
% 0.22/0.57 product(a1,a8)=product(a9,product(a9,a10))),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f160,f575])).
% 0.22/0.57 fof(f581,plain,(
% 0.22/0.57 product(a1,a4)=product(a9,a10)),
% 0.22/0.57 inference(backward_demodulation,[status(thm)],[f582,f160])).
% 0.22/0.57 fof(f582,plain,(
% 0.22/0.57 product(a1,a4)=product(a4,a9)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f16,f570])).
% 0.22/0.57 fof(f584,plain,(
% 0.22/0.57 product(a1,a8)=product(a9,product(a1,a4))),
% 0.22/0.57 inference(backward_demodulation,[status(thm)],[f581,f576])).
% 0.22/0.57 fof(f591,plain,(
% 0.22/0.57 product(a8,a10)=product(a10,product(a1,a4))),
% 0.22/0.57 inference(backward_demodulation,[status(thm)],[f581,f118])).
% 0.22/0.57 fof(f624,plain,(
% 0.22/0.57 ![X0]: (product(product(a9,X0),a10)=product(product(a1,a4),product(X0,a10)))),
% 0.22/0.57 inference(paramodulation,[status(thm)],[f581,f17])).
% 0.22/0.57 fof(f625,plain,(
% 0.22/0.57 product(product(a1,a4),a10)=a9),
% 0.22/0.57 inference(paramodulation,[status(thm)],[f581,f16])).
% 0.22/0.57 fof(f644,plain,(
% 0.22/0.57 product(a9,a4)=product(a1,product(a10,a4))),
% 0.22/0.57 inference(paramodulation,[status(thm)],[f625,f56])).
% 0.22/0.57 fof(f649,plain,(
% 0.22/0.57 product(a9,product(a1,a4))=product(product(a1,a4),product(a10,product(a1,a4)))),
% 0.22/0.57 inference(paramodulation,[status(thm)],[f625,f77])).
% 0.22/0.57 fof(f654,plain,(
% 0.22/0.57 product(a1,a2)=a4),
% 0.22/0.57 inference(backward_demodulation,[status(thm)],[f671,f194])).
% 0.22/0.57 fof(f671,plain,(
% 0.22/0.57 product(a9,a4)=a2),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f207,f644])).
% 0.22/0.57 fof(f673,plain,(
% 0.22/0.57 product(a1,a8)=product(product(a1,a4),product(a10,product(a1,a4)))),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f584,f649])).
% 0.22/0.57 fof(f674,plain,(
% 0.22/0.57 product(a1,a8)=product(product(a1,a4),product(a8,a10))),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f591,f673])).
% 0.22/0.57 fof(f675,plain,(
% 0.22/0.57 product(a1,a8)=product(product(a9,a8),a10)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f624,f674])).
% 0.22/0.57 fof(f676,plain,(
% 0.22/0.57 product(a1,a8)=product(product(a9,a7),a8)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f169,f675])).
% 0.22/0.57 fof(f677,plain,(
% 0.22/0.57 product(a1,a8)=product(a4,product(a7,a8))),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f75,f676])).
% 0.22/0.57 fof(f680,plain,(
% 0.22/0.57 product(a1,a8)=product(a4,a10)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f150,f677])).
% 0.22/0.57 fof(f683,plain,(
% 0.22/0.57 product(product(a1,a3),a10)=a9),
% 0.22/0.57 inference(backward_demodulation,[status(thm)],[f790,f625])).
% 0.22/0.57 fof(f688,plain,(
% 0.22/0.57 product(a1,product(a10,a3))=a2),
% 0.22/0.57 inference(backward_demodulation,[status(thm)],[f790,f207])).
% 0.22/0.57 fof(f690,plain,(
% 0.22/0.57 a1=product(a2,product(a10,a3))),
% 0.22/0.57 inference(backward_demodulation,[status(thm)],[f790,f156])).
% 0.22/0.57 fof(f691,plain,(
% 0.22/0.57 product(a2,a3)=a3),
% 0.22/0.57 inference(backward_demodulation,[status(thm)],[f790,f40])).
% 0.22/0.57 fof(f694,plain,(
% 0.22/0.57 product(a3,a3)=a10),
% 0.22/0.57 inference(backward_demodulation,[status(thm)],[f790,f34])).
% 0.22/0.57 fof(f696,plain,(
% 0.22/0.57 a9=product(a3,a8)),
% 0.22/0.57 inference(backward_demodulation,[status(thm)],[f790,f27])).
% 0.22/0.57 fof(f698,plain,(
% 0.22/0.57 a8=product(a7,a3)),
% 0.22/0.57 inference(backward_demodulation,[status(thm)],[f790,f24])).
% 0.22/0.57 fof(f699,plain,(
% 0.22/0.57 a6=product(a5,a3)),
% 0.22/0.57 inference(backward_demodulation,[status(thm)],[f790,f22])).
% 0.22/0.57 fof(f700,plain,(
% 0.22/0.57 a2=product(a3,a3)),
% 0.22/0.57 inference(backward_demodulation,[status(thm)],[f790,f20])).
% 0.22/0.57 fof(f701,plain,(
% 0.22/0.57 sF1_fnc=tuple(a2,a10,a9,a7,a8,a3,a3,a5,a6)),
% 0.22/0.57 inference(backward_demodulation,[status(thm)],[f790,f30])).
% 0.22/0.57 fof(f702,plain,(
% 0.22/0.57 sF0_fnc=tuple(a1,a9,a8,a6,a7,a2,a3,a3,a5)),
% 0.22/0.57 inference(backward_demodulation,[status(thm)],[f790,f29])).
% 0.22/0.57 fof(f705,plain,(
% 0.22/0.57 product(a1,a8)=product(a3,a10)),
% 0.22/0.57 inference(backward_demodulation,[status(thm)],[f790,f680])).
% 0.22/0.57 fof(f717,plain,(
% 0.22/0.57 product(a8,a10)=product(a10,product(a1,a3))),
% 0.22/0.57 inference(backward_demodulation,[status(thm)],[f790,f591])).
% 0.22/0.57 fof(f790,plain,(
% 0.22/0.57 a3=a4),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f19,f654])).
% 0.22/0.57 fof(f819,plain,(
% 0.22/0.57 product(a1,a4)=a2),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f26,f688])).
% 0.22/0.57 fof(f822,plain,(
% 0.22/0.57 product(a2,a10)=a9),
% 0.22/0.57 inference(backward_demodulation,[status(thm)],[f824,f683])).
% 0.22/0.57 fof(f824,plain,(
% 0.22/0.57 product(a1,a3)=a2),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f790,f819])).
% 0.22/0.57 fof(f826,plain,(
% 0.22/0.57 a1=product(a2,a4)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f26,f690])).
% 0.22/0.57 fof(f828,plain,(
% 0.22/0.57 a1=product(a2,a3)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f790,f826])).
% 0.22/0.57 fof(f868,plain,(
% 0.22/0.57 a1=a3),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f828,f691])).
% 0.22/0.57 fof(f872,plain,(
% 0.22/0.57 a3=a10),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f15,f694])).
% 0.22/0.57 fof(f875,plain,(
% 0.22/0.57 product(a5,a1)=a2),
% 0.22/0.57 inference(backward_demodulation,[status(thm)],[f910,f39])).
% 0.22/0.57 fof(f910,plain,(
% 0.22/0.57 a1=a10),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f868,f872])).
% 0.22/0.57 fof(f912,plain,(
% 0.22/0.57 a9=product(a1,a8)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f868,f696])).
% 0.22/0.57 fof(f916,plain,(
% 0.22/0.57 a8=product(a7,a1)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f868,f698])).
% 0.22/0.57 fof(f922,plain,(
% 0.22/0.57 a8=a6),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f37,f916])).
% 0.22/0.57 fof(f923,plain,(
% 0.22/0.57 a6=product(a5,a1)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f868,f699])).
% 0.22/0.57 fof(f924,plain,(
% 0.22/0.57 a2=a3),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f15,f700])).
% 0.22/0.57 fof(f925,plain,(
% 0.22/0.57 a2=a1),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f868,f924])).
% 0.22/0.57 fof(f926,plain,(
% 0.22/0.57 sF1_fnc=tuple(a1,a10,a9,a7,a8,a3,a3,a5,a6)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f925,f701])).
% 0.22/0.57 fof(f927,plain,(
% 0.22/0.57 sF1_fnc=tuple(a1,a1,a9,a7,a8,a3,a3,a5,a6)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f910,f926])).
% 0.22/0.57 fof(f928,plain,(
% 0.22/0.57 sF1_fnc=tuple(a1,a1,a9,a7,a6,a3,a3,a5,a6)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f922,f927])).
% 0.22/0.57 fof(f929,plain,(
% 0.22/0.57 sF1_fnc=tuple(a1,a1,a9,a7,a6,a1,a3,a5,a6)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f868,f928])).
% 0.22/0.57 fof(f930,plain,(
% 0.22/0.57 sF1_fnc=tuple(a1,a1,a9,a7,a6,a1,a1,a5,a6)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f868,f929])).
% 0.22/0.57 fof(f931,plain,(
% 0.22/0.57 sF0_fnc=tuple(a1,a9,a6,a6,a7,a2,a3,a3,a5)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f922,f702])).
% 0.22/0.57 fof(f932,plain,(
% 0.22/0.57 sF0_fnc=tuple(a1,a9,a6,a6,a7,a1,a3,a3,a5)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f925,f931])).
% 0.22/0.57 fof(f933,plain,(
% 0.22/0.57 sF0_fnc=tuple(a1,a9,a6,a6,a7,a1,a1,a3,a5)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f868,f932])).
% 0.22/0.57 fof(f934,plain,(
% 0.22/0.57 sF0_fnc=tuple(a1,a9,a6,a6,a7,a1,a1,a1,a5)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f868,f933])).
% 0.22/0.57 fof(f941,plain,(
% 0.22/0.57 a9=product(a3,a10)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f912,f705])).
% 0.22/0.57 fof(f942,plain,(
% 0.22/0.57 a9=product(a1,a10)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f868,f941])).
% 0.22/0.57 fof(f943,plain,(
% 0.22/0.57 a9=product(a1,a1)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f910,f942])).
% 0.22/0.57 fof(f949,plain,(
% 0.22/0.57 sF0_fnc=tuple(a1,a1,a6,a6,a7,a1,a1,a1,a5)),
% 0.22/0.57 inference(backward_demodulation,[status(thm)],[f970,f934])).
% 0.22/0.57 fof(f950,plain,(
% 0.22/0.57 sF1_fnc=tuple(a1,a1,a1,a7,a6,a1,a1,a5,a6)),
% 0.22/0.57 inference(backward_demodulation,[status(thm)],[f970,f930])).
% 0.22/0.57 fof(f970,plain,(
% 0.22/0.57 a9=a1),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f15,f943])).
% 0.22/0.57 fof(f1042,plain,(
% 0.22/0.57 product(a6,a10)=product(a10,product(a1,a3))),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f922,f717])).
% 0.22/0.57 fof(f1043,plain,(
% 0.22/0.57 product(a6,a1)=product(a10,product(a1,a3))),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f910,f1042])).
% 0.22/0.57 fof(f1044,plain,(
% 0.22/0.57 a7=product(a10,product(a1,a3))),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f23,f1043])).
% 0.22/0.57 fof(f1045,plain,(
% 0.22/0.57 a7=product(a1,product(a1,a3))),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f910,f1044])).
% 0.22/0.57 fof(f1046,plain,(
% 0.22/0.57 a7=product(a1,a2)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f824,f1045])).
% 0.22/0.57 fof(f1047,plain,(
% 0.22/0.57 a7=product(a1,a1)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f925,f1046])).
% 0.22/0.57 fof(f1057,plain,(
% 0.22/0.57 a7=a1),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f15,f1047])).
% 0.22/0.57 fof(f1501,plain,(
% 0.22/0.57 a5=a9),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f21,f822])).
% 0.22/0.57 fof(f1511,plain,(
% 0.22/0.57 a5=a1),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f970,f1501])).
% 0.22/0.57 fof(f1686,plain,(
% 0.22/0.57 a6=a2),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f923,f875])).
% 0.22/0.57 fof(f1704,plain,(
% 0.22/0.57 a6=a1),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f925,f1686])).
% 0.22/0.57 fof(f1863,plain,(
% 0.22/0.57 sF0_fnc=tuple(a1,a1,a1,a6,a7,a1,a1,a1,a5)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f1704,f949])).
% 0.22/0.57 fof(f1864,plain,(
% 0.22/0.57 sF0_fnc=tuple(a1,a1,a1,a1,a7,a1,a1,a1,a5)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f1704,f1863])).
% 0.22/0.57 fof(f1865,plain,(
% 0.22/0.57 sF0_fnc=tuple(a1,a1,a1,a1,a1,a1,a1,a1,a5)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f1057,f1864])).
% 0.22/0.57 fof(f1866,plain,(
% 0.22/0.57 sF0_fnc=tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f1511,f1865])).
% 0.22/0.57 fof(f1867,plain,(
% 0.22/0.57 sF1_fnc=tuple(a1,a1,a1,a1,a6,a1,a1,a5,a6)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f1057,f950])).
% 0.22/0.57 fof(f1868,plain,(
% 0.22/0.57 sF1_fnc=tuple(a1,a1,a1,a1,a1,a1,a1,a5,a6)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f1704,f1867])).
% 0.22/0.57 fof(f1869,plain,(
% 0.22/0.57 sF1_fnc=tuple(a1,a1,a1,a1,a1,a1,a1,a1,a6)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f1511,f1868])).
% 0.22/0.57 fof(f1870,plain,(
% 0.22/0.57 sF1_fnc=tuple(a1,a1,a1,a1,a1,a1,a1,a1,a1)),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f1704,f1869])).
% 0.22/0.57 fof(f1871,plain,(
% 0.22/0.57 sF1_fnc=sF0_fnc),
% 0.22/0.57 inference(forward_demodulation,[status(thm)],[f1866,f1870])).
% 0.22/0.57 fof(f1872,plain,(
% 0.22/0.57 $false),
% 0.22/0.57 inference(forward_subsumption_resolution,[status(thm)],[f1871,f31])).
% 0.22/0.57 % SZS output end CNFRefutation for theBenchmark.p
% 0.22/0.61 % Elapsed time: 0.102520 seconds
% 0.22/0.61 % CPU time: 0.385636 seconds
% 0.22/0.61 % Total memory used: 14.324 MB
% 0.22/0.61 % Net memory used: 14.268 MB
%------------------------------------------------------------------------------