%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP700-10 : 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 : 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:37:11 PM UTC 2026
% Result : Unsatisfiable 1.69s 0.67s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP700-10 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n018.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 20:36:15 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 1.69/0.67 % Refutation found
% 1.69/0.67 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 1.69/0.67 % SZS output start CNFRefutation for theBenchmark
% 1.69/0.67 fof(f3,axiom,(
% 1.69/0.67 (![A,B]: (mult(rd(A,B),B) = A ))),
% 1.69/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.69/0.67 fof(f4,axiom,(
% 1.69/0.67 (![A,B]: (rd(mult(A,B),B) = A ))),
% 1.69/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.69/0.67 fof(f5,axiom,(
% 1.69/0.67 (![A]: (mult(A,unit) = A ))),
% 1.69/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.69/0.67 fof(f6,axiom,(
% 1.69/0.67 (![A]: (mult(unit,A) = A ))),
% 1.69/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.69/0.67 fof(f7,axiom,(
% 1.69/0.67 (![A,B,C]: (mult(mult(mult(A,B),A),mult(A,C)) = mult(A,mult(mult(mult(B,A),A),C)) ))),
% 1.69/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.69/0.67 fof(f9,negated_conjecture,(
% 1.69/0.67 (![X1]: (tuple(mult(X1,x0),mult(x0,X1)) != tuple(unit,unit) ))),
% 1.69/0.67 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.69/0.67 fof(f12,plain,(
% 1.69/0.67 ![X0,X1]: (mult(rd(X0,X1),X1)=X0)),
% 1.69/0.67 inference(cnf_transformation,[status(thm)],[f3])).
% 1.69/0.67 fof(f13,plain,(
% 1.69/0.67 ![X0,X1]: (rd(mult(X0,X1),X1)=X0)),
% 1.69/0.67 inference(cnf_transformation,[status(thm)],[f4])).
% 1.69/0.67 fof(f14,plain,(
% 1.69/0.67 ![X0]: (mult(X0,unit)=X0)),
% 1.69/0.67 inference(cnf_transformation,[status(thm)],[f5])).
% 1.69/0.67 fof(f15,plain,(
% 1.69/0.67 ![X0]: (mult(unit,X0)=X0)),
% 1.69/0.67 inference(cnf_transformation,[status(thm)],[f6])).
% 1.69/0.67 fof(f16,plain,(
% 1.69/0.67 ![X0,X1,X2]: (mult(mult(mult(X0,X1),X0),mult(X0,X2))=mult(X0,mult(mult(mult(X1,X0),X0),X2)))),
% 1.69/0.67 inference(cnf_transformation,[status(thm)],[f7])).
% 1.69/0.67 fof(f18,plain,(
% 1.69/0.67 ![X0]: (~tuple(mult(X0,x0),mult(x0,X0))=tuple(unit,unit))),
% 1.69/0.67 inference(cnf_transformation,[status(thm)],[f9])).
% 1.69/0.67 fof(f19,definition,(
% 1.69/0.67 ![X0]: (sF1_fnc(X0)=mult(X0,x0))),
% 1.69/0.67 introduced(definition,[new_symbols(definition,[sF1_fnc(X0)])],[function_definition])).
% 1.69/0.67 fof(f20,definition,(
% 1.69/0.67 ![X0]: (sF2_fnc(X0)=mult(x0,X0))),
% 1.69/0.67 introduced(definition,[new_symbols(definition,[sF2_fnc(X0)])],[function_definition])).
% 1.69/0.67 fof(f21,definition,(
% 1.69/0.67 ![X0]: (sF0_fnc(X0)=tuple(sF1_fnc(X0),sF2_fnc(X0)))),
% 1.69/0.67 introduced(definition,[new_symbols(definition,[sF0_fnc(X0)])],[function_definition])).
% 1.69/0.67 fof(f22,definition,(
% 1.69/0.67 sF3_fnc=tuple(unit,unit)),
% 1.69/0.67 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 1.69/0.67 fof(f23,plain,(
% 1.69/0.67 ![X0]: (~sF0_fnc(X0)=sF3_fnc)),
% 1.69/0.67 inference(definition_folding,[],[f18,f22,f21,f20,f19])).
% 1.69/0.67 fof(f26,plain,(
% 1.69/0.67 sF2_fnc(unit)=x0),
% 1.69/0.67 inference(paramodulation,[status(thm)],[f20,f14])).
% 1.69/0.67 fof(f29,plain,(
% 1.69/0.67 sF1_fnc(unit)=x0),
% 1.69/0.67 inference(paramodulation,[status(thm)],[f19,f15])).
% 1.69/0.67 fof(f37,plain,(
% 1.69/0.67 ![X0,X1]: (mult(sF1_fnc(mult(x0,X0)),mult(x0,X1))=mult(x0,mult(mult(mult(X0,x0),x0),X1)))),
% 1.69/0.67 inference(paramodulation,[status(thm)],[f19,f16])).
% 1.69/0.67 fof(f52,plain,(
% 1.69/0.67 ![X0,X1]: (mult(sF1_fnc(sF2_fnc(X0)),mult(x0,X1))=mult(x0,mult(mult(mult(X0,x0),x0),X1)))),
% 1.69/0.67 inference(forward_demodulation,[status(thm)],[f20,f37])).
% 1.69/0.67 fof(f53,plain,(
% 1.69/0.67 ![X0,X1]: (mult(sF1_fnc(sF2_fnc(X0)),sF2_fnc(X1))=mult(x0,mult(mult(mult(X0,x0),x0),X1)))),
% 1.69/0.67 inference(forward_demodulation,[status(thm)],[f20,f52])).
% 1.69/0.67 fof(f54,plain,(
% 1.69/0.67 ![X0,X1]: (mult(sF1_fnc(sF2_fnc(X0)),sF2_fnc(X1))=sF2_fnc(mult(mult(mult(X0,x0),x0),X1)))),
% 1.69/0.67 inference(forward_demodulation,[status(thm)],[f20,f53])).
% 1.69/0.67 fof(f55,plain,(
% 1.69/0.67 ![X0,X1]: (mult(sF1_fnc(sF2_fnc(X0)),sF2_fnc(X1))=sF2_fnc(mult(sF1_fnc(mult(X0,x0)),X1)))),
% 1.69/0.67 inference(forward_demodulation,[status(thm)],[f19,f54])).
% 1.69/0.67 fof(f56,plain,(
% 1.69/0.67 ![X0,X1]: (mult(sF1_fnc(sF2_fnc(X0)),sF2_fnc(X1))=sF2_fnc(mult(sF1_fnc(sF1_fnc(X0)),X1)))),
% 1.69/0.67 inference(forward_demodulation,[status(thm)],[f19,f55])).
% 1.69/0.67 fof(f161,plain,(
% 1.69/0.67 ![X0]: (sF1_fnc(rd(X0,x0))=X0)),
% 1.69/0.67 inference(paramodulation,[status(thm)],[f19,f12])).
% 1.69/0.67 fof(f174,plain,(
% 1.69/0.67 ![X0]: (rd(X0,X0)=unit)),
% 1.69/0.67 inference(paramodulation,[status(thm)],[f15,f13])).
% 1.69/0.67 fof(f175,plain,(
% 1.69/0.67 ![X0]: (rd(sF2_fnc(X0),X0)=x0)),
% 1.69/0.67 inference(paramodulation,[status(thm)],[f20,f13])).
% 1.69/0.67 fof(f178,plain,(
% 1.69/0.67 ![X0]: (rd(sF1_fnc(X0),x0)=X0)),
% 1.69/0.67 inference(paramodulation,[status(thm)],[f19,f13])).
% 1.69/0.67 fof(f195,plain,(
% 1.69/0.67 ![X0]: (mult(sF1_fnc(sF2_fnc(X0)),x0)=sF2_fnc(mult(sF1_fnc(sF1_fnc(X0)),unit)))),
% 1.69/0.67 inference(paramodulation,[status(thm)],[f26,f56])).
% 1.69/0.67 fof(f203,plain,(
% 1.69/0.68 ![X0]: (sF1_fnc(sF1_fnc(sF2_fnc(X0)))=sF2_fnc(mult(sF1_fnc(sF1_fnc(X0)),unit)))),
% 1.69/0.68 inference(forward_demodulation,[status(thm)],[f19,f195])).
% 1.69/0.68 fof(f204,plain,(
% 1.69/0.68 ![X0]: (sF1_fnc(sF1_fnc(sF2_fnc(X0)))=sF2_fnc(sF1_fnc(sF1_fnc(X0))))),
% 1.69/0.68 inference(forward_demodulation,[status(thm)],[f14,f203])).
% 1.69/0.68 fof(f217,plain,(
% 1.69/0.68 ![X0]: (sF0_fnc(rd(X0,x0))=tuple(X0,sF2_fnc(rd(X0,x0))))),
% 1.69/0.68 inference(paramodulation,[status(thm)],[f161,f21])).
% 1.69/0.68 fof(f903,plain,(
% 1.69/0.68 ![X0]: (sF1_fnc(sF1_fnc(sF2_fnc(rd(X0,x0))))=sF2_fnc(sF1_fnc(X0)))),
% 1.69/0.68 inference(paramodulation,[status(thm)],[f161,f204])).
% 1.69/0.68 fof(f1763,plain,(
% 1.69/0.68 ![X0]: (rd(sF2_fnc(sF1_fnc(X0)),x0)=sF1_fnc(sF2_fnc(rd(X0,x0))))),
% 1.69/0.68 inference(paramodulation,[status(thm)],[f903,f178])).
% 1.69/0.68 fof(f3941,plain,(
% 1.69/0.68 rd(sF2_fnc(x0),x0)=sF1_fnc(sF2_fnc(rd(unit,x0)))),
% 1.69/0.68 inference(paramodulation,[status(thm)],[f29,f1763])).
% 1.69/0.68 fof(f3954,plain,(
% 1.69/0.68 x0=sF1_fnc(sF2_fnc(rd(unit,x0)))),
% 1.69/0.68 inference(forward_demodulation,[status(thm)],[f175,f3941])).
% 1.69/0.68 fof(f3974,plain,(
% 1.69/0.68 rd(x0,x0)=sF2_fnc(rd(unit,x0))),
% 1.69/0.68 inference(paramodulation,[status(thm)],[f3954,f178])).
% 1.69/0.68 fof(f4002,plain,(
% 1.69/0.68 unit=sF2_fnc(rd(unit,x0))),
% 1.69/0.68 inference(forward_demodulation,[status(thm)],[f174,f3974])).
% 1.69/0.68 fof(f4005,plain,(
% 1.69/0.68 sF0_fnc(rd(unit,x0))=tuple(unit,unit)),
% 1.69/0.68 inference(paramodulation,[status(thm)],[f4002,f217])).
% 1.69/0.68 fof(f4019,plain,(
% 1.69/0.68 sF0_fnc(rd(unit,x0))=sF3_fnc),
% 1.69/0.68 inference(forward_demodulation,[status(thm)],[f22,f4005])).
% 1.69/0.68 fof(f4020,plain,(
% 1.69/0.68 $false),
% 1.69/0.68 inference(forward_subsumption_resolution,[status(thm)],[f4019,f23])).
% 1.69/0.68 % SZS output end CNFRefutation for theBenchmark.p
% 1.69/0.71 % Elapsed time: 0.334023 seconds
% 1.69/0.71 % CPU time: 2.500922 seconds
% 1.69/0.71 % Total memory used: 98.804 MB
% 1.69/0.71 % Net memory used: 98.478 MB
%------------------------------------------------------------------------------