%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : KLE169-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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:58:26 PM UTC 2026
% Result : Unsatisfiable 3.24s 0.84s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE169-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n004.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 20 22:48:20 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 3.24/0.84 % Refutation found
% 3.24/0.84 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 3.24/0.84 % SZS output start CNFRefutation for theBenchmark
% 3.24/0.84 fof(f1,axiom,(
% 3.24/0.84 (![A,B,C]: (ifeq3(A,A,B,C) = B ))),
% 3.24/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.24/0.84 fof(f2,axiom,(
% 3.24/0.84 (![A,B,C]: (ifeq2(A,A,B,C) = B ))),
% 3.24/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.24/0.84 fof(f4,axiom,(
% 3.24/0.84 (![A,B]: (addition(A,B) = addition(B,A) ))),
% 3.24/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.24/0.84 fof(f5,axiom,(
% 3.24/0.84 (![A,B,C]: (addition(A,addition(B,C)) = addition(addition(A,B),C) ))),
% 3.24/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.24/0.84 fof(f7,axiom,(
% 3.24/0.84 (![A]: (addition(A,A) = A ))),
% 3.24/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.24/0.84 fof(f10,axiom,(
% 3.24/0.84 (![A]: (multiplication(one,A) = A ))),
% 3.24/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.24/0.84 fof(f11,axiom,(
% 3.24/0.84 (![A,B,C]: (multiplication(A,addition(B,C)) = addition(multiplication(A,B),multiplication(A,C)) ))),
% 3.24/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.24/0.84 fof(f12,axiom,(
% 3.24/0.84 (![A,B,C]: (multiplication(addition(A,B),C) = addition(multiplication(A,C),multiplication(B,C)) ))),
% 3.24/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.24/0.84 fof(f15,axiom,(
% 3.24/0.84 (![A,B]: (ifeq2(leq(A,B),true,addition(A,B),B) = B ))),
% 3.24/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.24/0.84 fof(f16,axiom,(
% 3.24/0.84 (![A,B]: (ifeq3(addition(A,B),B,leq(A,B),true) = true ))),
% 3.24/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.24/0.84 fof(f17,axiom,(
% 3.24/0.84 (![A]: (leq(addition(one,multiplication(A,star(A))),star(A)) = true ))),
% 3.24/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.24/0.84 fof(f21,axiom,(
% 3.24/0.84 sigma = addition(a,b) ),
% 3.24/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.24/0.84 fof(f22,negated_conjecture,(
% 3.24/0.84 leq(multiplication(a,multiplication(b,a)),multiplication(star(sigma),multiplication(a,multiplication(sigma,a)))) != true ),
% 3.24/0.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 3.24/0.84 fof(f23,plain,(
% 3.24/0.84 ![X0,X1,X2]: (ifeq3(X0,X0,X1,X2)=X1)),
% 3.24/0.84 inference(cnf_transformation,[status(thm)],[f1])).
% 3.24/0.84 fof(f24,plain,(
% 3.24/0.84 ![X0,X1,X2]: (ifeq2(X0,X0,X1,X2)=X1)),
% 3.24/0.84 inference(cnf_transformation,[status(thm)],[f2])).
% 3.24/0.84 fof(f26,plain,(
% 3.24/0.84 ![X0,X1]: (addition(X0,X1)=addition(X1,X0))),
% 3.24/0.84 inference(cnf_transformation,[status(thm)],[f4])).
% 3.24/0.84 fof(f27,plain,(
% 3.24/0.84 ![X0,X1,X2]: (addition(X0,addition(X1,X2))=addition(addition(X0,X1),X2))),
% 3.24/0.84 inference(cnf_transformation,[status(thm)],[f5])).
% 3.24/0.84 fof(f29,plain,(
% 3.24/0.84 ![X0]: (addition(X0,X0)=X0)),
% 3.24/0.84 inference(cnf_transformation,[status(thm)],[f7])).
% 3.24/0.84 fof(f32,plain,(
% 3.24/0.84 ![X0]: (multiplication(one,X0)=X0)),
% 3.24/0.84 inference(cnf_transformation,[status(thm)],[f10])).
% 3.24/0.84 fof(f33,plain,(
% 3.24/0.84 ![X0,X1,X2]: (multiplication(X0,addition(X1,X2))=addition(multiplication(X0,X1),multiplication(X0,X2)))),
% 3.24/0.84 inference(cnf_transformation,[status(thm)],[f11])).
% 3.24/0.84 fof(f34,plain,(
% 3.24/0.84 ![X0,X1,X2]: (multiplication(addition(X0,X1),X2)=addition(multiplication(X0,X2),multiplication(X1,X2)))),
% 3.24/0.84 inference(cnf_transformation,[status(thm)],[f12])).
% 3.24/0.84 fof(f37,plain,(
% 3.24/0.84 ![X0,X1]: (ifeq2(leq(X0,X1),true,addition(X0,X1),X1)=X1)),
% 3.24/0.84 inference(cnf_transformation,[status(thm)],[f15])).
% 3.24/0.84 fof(f38,plain,(
% 3.24/0.84 ![X0,X1]: (ifeq3(addition(X0,X1),X1,leq(X0,X1),true)=true)),
% 3.24/0.84 inference(cnf_transformation,[status(thm)],[f16])).
% 3.24/0.84 fof(f39,plain,(
% 3.24/0.84 ![X0]: (leq(addition(one,multiplication(X0,star(X0))),star(X0))=true)),
% 3.24/0.84 inference(cnf_transformation,[status(thm)],[f17])).
% 3.24/0.84 fof(f43,plain,(
% 3.24/0.84 sigma=addition(a,b)),
% 3.24/0.84 inference(cnf_transformation,[status(thm)],[f21])).
% 3.24/0.84 fof(f44,plain,(
% 3.24/0.84 ~leq(multiplication(a,multiplication(b,a)),multiplication(star(sigma),multiplication(a,multiplication(sigma,a))))=true),
% 3.24/0.84 inference(cnf_transformation,[status(thm)],[f22])).
% 3.24/0.84 fof(f45,definition,(
% 3.24/0.84 sF2_fnc=multiplication(b,a)),
% 3.24/0.84 introduced(definition,[new_symbols(definition,[sF2_fnc])],[function_definition])).
% 3.24/0.84 fof(f46,definition,(
% 3.24/0.84 sF1_fnc=multiplication(a,sF2_fnc)),
% 3.24/0.84 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 3.24/0.84 fof(f47,definition,(
% 3.24/0.84 sF4_fnc=star(sigma)),
% 3.24/0.84 introduced(definition,[new_symbols(definition,[sF4_fnc])],[function_definition])).
% 3.24/0.84 fof(f48,definition,(
% 3.24/0.84 sF6_fnc=multiplication(sigma,a)),
% 3.24/0.84 introduced(definition,[new_symbols(definition,[sF6_fnc])],[function_definition])).
% 3.24/0.84 fof(f49,definition,(
% 3.24/0.84 sF5_fnc=multiplication(a,sF6_fnc)),
% 3.24/0.84 introduced(definition,[new_symbols(definition,[sF5_fnc])],[function_definition])).
% 3.24/0.84 fof(f50,definition,(
% 3.24/0.84 sF3_fnc=multiplication(sF4_fnc,sF5_fnc)),
% 3.24/0.84 introduced(definition,[new_symbols(definition,[sF3_fnc])],[function_definition])).
% 3.24/0.84 fof(f51,definition,(
% 3.24/0.84 sF0_fnc=leq(sF1_fnc,sF3_fnc)),
% 3.24/0.84 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 3.24/0.84 fof(f52,plain,(
% 3.24/0.84 ~sF0_fnc=true),
% 3.24/0.84 inference(definition_folding,[],[f44,f51,f50,f49,f48,f47,f46,f45])).
% 3.24/0.84 fof(f114,plain,(
% 3.24/0.84 ![X0]: (addition(a,addition(b,X0))=addition(sigma,X0))),
% 3.24/0.84 inference(paramodulation,[status(thm)],[f43,f27])).
% 3.24/0.84 fof(f118,plain,(
% 3.24/0.84 ![X0,X1]: (addition(X0,addition(X0,X1))=addition(X0,X1))),
% 3.24/0.84 inference(paramodulation,[status(thm)],[f29,f27])).
% 3.24/0.84 fof(f133,plain,(
% 3.24/0.84 ![X0]: (multiplication(a,addition(sF6_fnc,X0))=addition(sF5_fnc,multiplication(a,X0)))),
% 3.24/0.84 inference(paramodulation,[status(thm)],[f49,f33])).
% 3.24/0.84 fof(f268,plain,(
% 3.24/0.84 ![X0]: (multiplication(addition(sF4_fnc,X0),sF5_fnc)=addition(sF3_fnc,multiplication(X0,sF5_fnc)))),
% 3.24/0.84 inference(paramodulation,[status(thm)],[f50,f34])).
% 3.24/0.84 fof(f270,plain,(
% 3.24/0.84 ![X0]: (multiplication(addition(sigma,X0),a)=addition(sF6_fnc,multiplication(X0,a)))),
% 3.24/0.84 inference(paramodulation,[status(thm)],[f48,f34])).
% 3.24/0.84 fof(f336,plain,(
% 3.24/0.84 ![X0,X1]: (ifeq2(leq(X0,X1),true,addition(X1,X0),X1)=X1)),
% 3.24/0.84 inference(paramodulation,[status(thm)],[f26,f37])).
% 3.24/0.84 fof(f344,plain,(
% 3.24/0.84 ![X0,X1]: (ifeq3(addition(X0,X1),addition(X0,X1),leq(X0,addition(X0,X1)),true)=true)),
% 3.24/0.84 inference(paramodulation,[status(thm)],[f118,f38])).
% 3.24/0.84 fof(f353,plain,(
% 3.24/0.84 ![X0,X1]: (leq(X0,addition(X0,X1))=true)),
% 3.24/0.84 inference(forward_demodulation,[status(thm)],[f23,f344])).
% 3.24/0.84 fof(f395,plain,(
% 3.24/0.84 addition(a,b)=addition(sigma,b)),
% 3.24/0.84 inference(paramodulation,[status(thm)],[f29,f114])).
% 3.24/0.84 fof(f402,plain,(
% 3.24/0.84 sigma=addition(sigma,b)),
% 3.24/0.84 inference(forward_demodulation,[status(thm)],[f43,f395])).
% 3.24/0.84 fof(f451,plain,(
% 3.24/0.84 ![X0]: (ifeq2(true,true,addition(addition(one,multiplication(X0,star(X0))),star(X0)),star(X0))=star(X0))),
% 3.24/0.84 inference(paramodulation,[status(thm)],[f39,f37])).
% 3.24/0.84 fof(f456,plain,(
% 3.24/0.84 ![X0]: (addition(addition(one,multiplication(X0,star(X0))),star(X0))=star(X0))),
% 3.24/0.84 inference(forward_demodulation,[status(thm)],[f24,f451])).
% 3.24/0.84 fof(f458,plain,(
% 3.24/0.84 ![X0]: (addition(one,addition(multiplication(X0,star(X0)),star(X0)))=star(X0))),
% 3.24/0.84 inference(forward_demodulation,[status(thm)],[f27,f456])).
% 3.24/0.84 fof(f630,plain,(
% 3.24/0.84 ![X0,X1]: (leq(X0,addition(X1,X0))=true)),
% 3.24/0.84 inference(paramodulation,[status(thm)],[f26,f353])).
% 3.24/0.84 fof(f647,plain,(
% 3.24/0.84 ![X0,X1,X2]: (leq(X0,addition(X1,addition(X2,X0)))=true)),
% 3.24/0.84 inference(paramodulation,[status(thm)],[f27,f630])).
% 3.24/0.84 fof(f1009,plain,(
% 3.24/0.84 multiplication(sigma,a)=addition(sF6_fnc,multiplication(b,a))),
% 3.24/0.84 inference(paramodulation,[status(thm)],[f402,f270])).
% 3.24/0.84 fof(f1027,plain,(
% 3.24/0.84 sF6_fnc=addition(sF6_fnc,multiplication(b,a))),
% 3.24/0.84 inference(forward_demodulation,[status(thm)],[f48,f1009])).
% 3.24/0.84 fof(f1028,plain,(
% 3.24/0.84 sF6_fnc=addition(sF6_fnc,sF2_fnc)),
% 3.24/0.84 inference(forward_demodulation,[status(thm)],[f45,f1027])).
% 3.24/0.84 fof(f1077,plain,(
% 3.24/0.84 multiplication(a,sF6_fnc)=addition(sF5_fnc,multiplication(a,sF2_fnc))),
% 3.24/0.84 inference(paramodulation,[status(thm)],[f1028,f133])).
% 3.24/0.84 fof(f1089,plain,(
% 3.24/0.84 sF5_fnc=addition(sF5_fnc,multiplication(a,sF2_fnc))),
% 3.24/0.84 inference(forward_demodulation,[status(thm)],[f49,f1077])).
% 3.24/0.84 fof(f1090,plain,(
% 3.24/0.84 sF5_fnc=addition(sF5_fnc,sF1_fnc)),
% 3.24/0.84 inference(forward_demodulation,[status(thm)],[f46,f1089])).
% 3.24/0.84 fof(f2600,plain,(
% 3.24/0.84 ![X0]: (leq(sF1_fnc,addition(X0,sF5_fnc))=true)),
% 3.24/0.84 inference(paramodulation,[status(thm)],[f1090,f647])).
% 3.24/0.84 fof(f6999,plain,(
% 3.24/0.84 ![X0]: (leq(one,star(X0))=true)),
% 3.24/0.84 inference(paramodulation,[status(thm)],[f458,f353])).
% 3.24/0.84 fof(f7457,plain,(
% 3.24/0.84 leq(one,sF4_fnc)=true),
% 3.24/0.84 inference(paramodulation,[status(thm)],[f47,f6999])).
% 3.24/0.84 fof(f7468,plain,(
% 3.24/0.84 ifeq2(true,true,addition(sF4_fnc,one),sF4_fnc)=sF4_fnc),
% 3.24/0.84 inference(paramodulation,[status(thm)],[f7457,f336])).
% 3.24/0.86 fof(f7474,plain,(
% 3.24/0.86 addition(sF4_fnc,one)=sF4_fnc),
% 3.24/0.86 inference(forward_demodulation,[status(thm)],[f24,f7468])).
% 3.24/0.86 fof(f7866,plain,(
% 3.24/0.86 multiplication(sF4_fnc,sF5_fnc)=addition(sF3_fnc,multiplication(one,sF5_fnc))),
% 3.24/0.86 inference(paramodulation,[status(thm)],[f7474,f268])).
% 3.24/0.86 fof(f7897,plain,(
% 3.24/0.86 sF3_fnc=addition(sF3_fnc,multiplication(one,sF5_fnc))),
% 3.24/0.86 inference(forward_demodulation,[status(thm)],[f50,f7866])).
% 3.24/0.86 fof(f7899,plain,(
% 3.24/0.86 sF3_fnc=addition(sF3_fnc,sF5_fnc)),
% 3.24/0.86 inference(forward_demodulation,[status(thm)],[f32,f7897])).
% 3.24/0.86 fof(f7939,plain,(
% 3.24/0.86 leq(sF1_fnc,sF3_fnc)=true),
% 3.24/0.86 inference(paramodulation,[status(thm)],[f7899,f2600])).
% 3.24/0.86 fof(f7964,plain,(
% 3.24/0.86 sF0_fnc=true),
% 3.24/0.86 inference(backward_demodulation,[status(thm)],[f7939,f51])).
% 3.24/0.86 fof(f7972,plain,(
% 3.24/0.86 $false),
% 3.24/0.86 inference(forward_subsumption_resolution,[status(thm)],[f7964,f52])).
% 3.24/0.86 % SZS output end CNFRefutation for theBenchmark.p
% 3.24/0.88 % Elapsed time: 0.503715 seconds
% 3.24/0.88 % CPU time: 3.720529 seconds
% 3.24/0.88 % Total memory used: 72.039 MB
% 3.24/0.88 % Net memory used: 70.930 MB
%------------------------------------------------------------------------------