%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG030-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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 11:49:29 AM UTC 2026
% Result : Unsatisfiable 0.09s 0.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG030-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n001.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 12:59:15 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.09/0.38 % Refutation found
% 0.09/0.38 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.09/0.38 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.38 fof(f1,axiom,(
% 0.09/0.38 (![A,B,C]: (ifeq2(A,A,B,C) = B ))),
% 0.09/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.38 fof(f2,axiom,(
% 0.09/0.38 (![A,B,C]: (ifeq(A,A,B,C) = B ))),
% 0.09/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.38 fof(f3,axiom,(
% 0.09/0.38 (![V,U]: (ifeq(sorti1(V),true,ifeq(sorti1(U),true,sorti1(op1(U,V)),true),true) = true ))),
% 0.09/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.38 fof(f5,axiom,(
% 0.09/0.38 op1(sK2_ax3_U,sK1_ax3_V) != op1(sK1_ax3_V,sK2_ax3_U) ),
% 0.09/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.38 fof(f6,axiom,(
% 0.09/0.38 sorti1(sK1_ax3_V) = true ),
% 0.09/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.38 fof(f7,axiom,(
% 0.09/0.38 sorti1(sK2_ax3_U) = true ),
% 0.09/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.38 fof(f8,axiom,(
% 0.09/0.38 (![V,U]: (ifeq2(sorti2(V),true,ifeq2(sorti2(U),true,op2(U,V),op2(V,U)),op2(V,U)) = op2(V,U) ))),
% 0.09/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.38 fof(f9,negated_conjecture,(
% 0.09/0.38 (![U]: (ifeq(sorti1(U),true,sorti2(h(U)),true) = true ))),
% 0.09/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.38 fof(f10,negated_conjecture,(
% 0.09/0.38 (![X,W]: (ifeq2(sorti1(X),true,ifeq2(sorti1(W),true,op2(h(W),h(X)),h(op1(W,X))),h(op1(W,X))) = h(op1(W,X)) ))),
% 0.09/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.38 fof(f11,negated_conjecture,(
% 0.09/0.38 (![X2]: (ifeq2(sorti1(X2),true,j(h(X2)),X2) = X2 ))),
% 0.09/0.38 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.38 fof(f15,plain,(
% 0.09/0.38 ![X0,X1,X2]: (ifeq2(X0,X0,X1,X2)=X1)),
% 0.09/0.38 inference(cnf_transformation,[status(thm)],[f1])).
% 0.09/0.38 fof(f16,plain,(
% 0.09/0.38 ![X0,X1,X2]: (ifeq(X0,X0,X1,X2)=X1)),
% 0.09/0.38 inference(cnf_transformation,[status(thm)],[f2])).
% 0.09/0.38 fof(f17,plain,(
% 0.09/0.38 ![X0,X1]: (ifeq(sorti1(X0),true,ifeq(sorti1(X1),true,sorti1(op1(X1,X0)),true),true)=true)),
% 0.09/0.38 inference(cnf_transformation,[status(thm)],[f3])).
% 0.09/0.38 fof(f19,plain,(
% 0.09/0.38 ~op1(sK2_ax3_U,sK1_ax3_V)=op1(sK1_ax3_V,sK2_ax3_U)),
% 0.09/0.38 inference(cnf_transformation,[status(thm)],[f5])).
% 0.09/0.38 fof(f20,plain,(
% 0.09/0.38 sorti1(sK1_ax3_V)=true),
% 0.09/0.38 inference(cnf_transformation,[status(thm)],[f6])).
% 0.09/0.38 fof(f21,plain,(
% 0.09/0.38 sorti1(sK2_ax3_U)=true),
% 0.09/0.38 inference(cnf_transformation,[status(thm)],[f7])).
% 0.09/0.38 fof(f22,plain,(
% 0.09/0.38 ![X0,X1]: (ifeq2(sorti2(X0),true,ifeq2(sorti2(X1),true,op2(X1,X0),op2(X0,X1)),op2(X0,X1))=op2(X0,X1))),
% 0.09/0.38 inference(cnf_transformation,[status(thm)],[f8])).
% 0.09/0.38 fof(f23,plain,(
% 0.09/0.38 ![X0]: (ifeq(sorti1(X0),true,sorti2(h(X0)),true)=true)),
% 0.09/0.38 inference(cnf_transformation,[status(thm)],[f9])).
% 0.09/0.38 fof(f24,plain,(
% 0.09/0.38 ![X0,X1]: (ifeq2(sorti1(X0),true,ifeq2(sorti1(X1),true,op2(h(X1),h(X0)),h(op1(X1,X0))),h(op1(X1,X0)))=h(op1(X1,X0)))),
% 0.09/0.38 inference(cnf_transformation,[status(thm)],[f10])).
% 0.09/0.38 fof(f25,plain,(
% 0.09/0.38 ![X0]: (ifeq2(sorti1(X0),true,j(h(X0)),X0)=X0)),
% 0.09/0.38 inference(cnf_transformation,[status(thm)],[f11])).
% 0.09/0.38 fof(f29,definition,(
% 0.09/0.38 sF0_fnc=op1(sK2_ax3_U,sK1_ax3_V)),
% 0.09/0.38 introduced(definition,[new_symbols(definition,[sF0_fnc])],[function_definition])).
% 0.09/0.38 fof(f30,definition,(
% 0.09/0.38 sF1_fnc=op1(sK1_ax3_V,sK2_ax3_U)),
% 0.09/0.38 introduced(definition,[new_symbols(definition,[sF1_fnc])],[function_definition])).
% 0.09/0.38 fof(f31,plain,(
% 0.09/0.38 ~sF0_fnc=sF1_fnc),
% 0.09/0.38 inference(definition_folding,[],[f19,f30,f29])).
% 0.09/0.38 fof(f32,plain,(
% 0.09/0.38 ifeq2(sorti1(sK2_ax3_U),true,ifeq2(sorti1(sK1_ax3_V),true,op2(h(sK1_ax3_V),h(sK2_ax3_U)),h(sF1_fnc)),h(op1(sK1_ax3_V,sK2_ax3_U)))=h(op1(sK1_ax3_V,sK2_ax3_U))),
% 0.09/0.38 inference(paramodulation,[status(thm)],[f30,f24])).
% 0.09/0.38 fof(f33,plain,(
% 0.09/0.38 ifeq2(sorti1(sK1_ax3_V),true,ifeq2(sorti1(sK2_ax3_U),true,op2(h(sK2_ax3_U),h(sK1_ax3_V)),h(sF0_fnc)),h(op1(sK2_ax3_U,sK1_ax3_V)))=h(op1(sK2_ax3_U,sK1_ax3_V))),
% 0.09/0.38 inference(paramodulation,[status(thm)],[f29,f24])).
% 0.09/0.38 fof(f36,plain,(
% 0.09/0.38 ifeq2(true,true,ifeq2(sorti1(sK1_ax3_V),true,op2(h(sK1_ax3_V),h(sK2_ax3_U)),h(sF1_fnc)),h(op1(sK1_ax3_V,sK2_ax3_U)))=h(op1(sK1_ax3_V,sK2_ax3_U))),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f21,f32])).
% 0.09/0.38 fof(f37,plain,(
% 0.09/0.38 ifeq2(sorti1(sK1_ax3_V),true,op2(h(sK1_ax3_V),h(sK2_ax3_U)),h(sF1_fnc))=h(op1(sK1_ax3_V,sK2_ax3_U))),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f15,f36])).
% 0.09/0.38 fof(f38,plain,(
% 0.09/0.38 ifeq2(true,true,op2(h(sK1_ax3_V),h(sK2_ax3_U)),h(sF1_fnc))=h(op1(sK1_ax3_V,sK2_ax3_U))),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f20,f37])).
% 0.09/0.38 fof(f39,plain,(
% 0.09/0.38 op2(h(sK1_ax3_V),h(sK2_ax3_U))=h(op1(sK1_ax3_V,sK2_ax3_U))),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f15,f38])).
% 0.09/0.38 fof(f40,plain,(
% 0.09/0.38 op2(h(sK1_ax3_V),h(sK2_ax3_U))=h(sF1_fnc)),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f30,f39])).
% 0.09/0.38 fof(f41,plain,(
% 0.09/0.38 ifeq2(true,true,ifeq2(sorti1(sK2_ax3_U),true,op2(h(sK2_ax3_U),h(sK1_ax3_V)),h(sF0_fnc)),h(op1(sK2_ax3_U,sK1_ax3_V)))=h(op1(sK2_ax3_U,sK1_ax3_V))),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f20,f33])).
% 0.09/0.38 fof(f42,plain,(
% 0.09/0.38 ifeq2(sorti1(sK2_ax3_U),true,op2(h(sK2_ax3_U),h(sK1_ax3_V)),h(sF0_fnc))=h(op1(sK2_ax3_U,sK1_ax3_V))),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f15,f41])).
% 0.09/0.38 fof(f43,plain,(
% 0.09/0.38 ifeq2(true,true,op2(h(sK2_ax3_U),h(sK1_ax3_V)),h(sF0_fnc))=h(op1(sK2_ax3_U,sK1_ax3_V))),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f21,f42])).
% 0.09/0.38 fof(f44,plain,(
% 0.09/0.38 op2(h(sK2_ax3_U),h(sK1_ax3_V))=h(op1(sK2_ax3_U,sK1_ax3_V))),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f15,f43])).
% 0.09/0.38 fof(f45,plain,(
% 0.09/0.38 op2(h(sK2_ax3_U),h(sK1_ax3_V))=h(sF0_fnc)),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f29,f44])).
% 0.09/0.38 fof(f66,plain,(
% 0.09/0.38 ifeq(sorti1(sK2_ax3_U),true,ifeq(sorti1(sK1_ax3_V),true,sorti1(sF1_fnc),true),true)=true),
% 0.09/0.38 inference(paramodulation,[status(thm)],[f30,f17])).
% 0.09/0.38 fof(f67,plain,(
% 0.09/0.38 ifeq(sorti1(sK1_ax3_V),true,ifeq(sorti1(sK2_ax3_U),true,sorti1(sF0_fnc),true),true)=true),
% 0.09/0.38 inference(paramodulation,[status(thm)],[f29,f17])).
% 0.09/0.38 fof(f68,plain,(
% 0.09/0.38 ifeq(true,true,ifeq(sorti1(sK1_ax3_V),true,sorti1(sF1_fnc),true),true)=true),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f21,f66])).
% 0.09/0.38 fof(f69,plain,(
% 0.09/0.38 ifeq(sorti1(sK1_ax3_V),true,sorti1(sF1_fnc),true)=true),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f16,f68])).
% 0.09/0.38 fof(f70,plain,(
% 0.09/0.38 ifeq(true,true,sorti1(sF1_fnc),true)=true),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f20,f69])).
% 0.09/0.38 fof(f71,plain,(
% 0.09/0.38 sorti1(sF1_fnc)=true),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f16,f70])).
% 0.09/0.38 fof(f72,plain,(
% 0.09/0.38 ifeq(true,true,ifeq(sorti1(sK2_ax3_U),true,sorti1(sF0_fnc),true),true)=true),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f20,f67])).
% 0.09/0.38 fof(f73,plain,(
% 0.09/0.38 ifeq(sorti1(sK2_ax3_U),true,sorti1(sF0_fnc),true)=true),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f16,f72])).
% 0.09/0.38 fof(f74,plain,(
% 0.09/0.38 ifeq(true,true,sorti1(sF0_fnc),true)=true),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f21,f73])).
% 0.09/0.38 fof(f75,plain,(
% 0.09/0.38 sorti1(sF0_fnc)=true),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f16,f74])).
% 0.09/0.38 fof(f81,plain,(
% 0.09/0.38 ifeq2(true,true,j(h(sF1_fnc)),sF1_fnc)=sF1_fnc),
% 0.09/0.38 inference(paramodulation,[status(thm)],[f71,f25])).
% 0.09/0.38 fof(f87,plain,(
% 0.09/0.38 j(h(sF1_fnc))=sF1_fnc),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f15,f81])).
% 0.09/0.38 fof(f93,plain,(
% 0.09/0.38 ifeq2(true,true,j(h(sF0_fnc)),sF0_fnc)=sF0_fnc),
% 0.09/0.38 inference(paramodulation,[status(thm)],[f75,f25])).
% 0.09/0.38 fof(f99,plain,(
% 0.09/0.38 j(h(sF0_fnc))=sF0_fnc),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f15,f93])).
% 0.09/0.38 fof(f144,plain,(
% 0.09/0.38 ifeq2(sorti2(h(sK1_ax3_V)),true,ifeq2(sorti2(h(sK2_ax3_U)),true,h(sF0_fnc),op2(h(sK1_ax3_V),h(sK2_ax3_U))),op2(h(sK1_ax3_V),h(sK2_ax3_U)))=op2(h(sK1_ax3_V),h(sK2_ax3_U))),
% 0.09/0.38 inference(paramodulation,[status(thm)],[f45,f22])).
% 0.09/0.38 fof(f154,plain,(
% 0.09/0.38 ifeq2(sorti2(h(sK1_ax3_V)),true,ifeq2(sorti2(h(sK2_ax3_U)),true,h(sF0_fnc),h(sF1_fnc)),op2(h(sK1_ax3_V),h(sK2_ax3_U)))=op2(h(sK1_ax3_V),h(sK2_ax3_U))),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f40,f144])).
% 0.09/0.38 fof(f155,plain,(
% 0.09/0.38 ifeq2(sorti2(h(sK1_ax3_V)),true,ifeq2(sorti2(h(sK2_ax3_U)),true,h(sF0_fnc),h(sF1_fnc)),h(sF1_fnc))=op2(h(sK1_ax3_V),h(sK2_ax3_U))),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f40,f154])).
% 0.09/0.38 fof(f156,plain,(
% 0.09/0.38 ifeq2(sorti2(h(sK1_ax3_V)),true,ifeq2(sorti2(h(sK2_ax3_U)),true,h(sF0_fnc),h(sF1_fnc)),h(sF1_fnc))=h(sF1_fnc)),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f40,f155])).
% 0.09/0.38 fof(f176,plain,(
% 0.09/0.38 ifeq(true,true,sorti2(h(sK1_ax3_V)),true)=true),
% 0.09/0.38 inference(paramodulation,[status(thm)],[f20,f23])).
% 0.09/0.38 fof(f183,plain,(
% 0.09/0.38 ifeq2(true,true,ifeq2(sorti2(h(sK2_ax3_U)),true,h(sF0_fnc),h(sF1_fnc)),h(sF1_fnc))=h(sF1_fnc)),
% 0.09/0.38 inference(backward_demodulation,[status(thm)],[f186,f156])).
% 0.09/0.38 fof(f186,plain,(
% 0.09/0.38 sorti2(h(sK1_ax3_V))=true),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f16,f176])).
% 0.09/0.38 fof(f189,plain,(
% 0.09/0.38 ifeq2(sorti2(h(sK2_ax3_U)),true,h(sF0_fnc),h(sF1_fnc))=h(sF1_fnc)),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f15,f183])).
% 0.09/0.38 fof(f196,plain,(
% 0.09/0.38 ifeq(true,true,sorti2(h(sK2_ax3_U)),true)=true),
% 0.09/0.38 inference(paramodulation,[status(thm)],[f21,f23])).
% 0.09/0.38 fof(f203,plain,(
% 0.09/0.38 ifeq2(true,true,h(sF0_fnc),h(sF1_fnc))=h(sF1_fnc)),
% 0.09/0.38 inference(backward_demodulation,[status(thm)],[f205,f189])).
% 0.09/0.38 fof(f205,plain,(
% 0.09/0.38 sorti2(h(sK2_ax3_U))=true),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f16,f196])).
% 0.09/0.38 fof(f207,plain,(
% 0.09/0.38 j(h(sF0_fnc))=sF1_fnc),
% 0.09/0.38 inference(backward_demodulation,[status(thm)],[f216,f87])).
% 0.09/0.38 fof(f216,plain,(
% 0.09/0.38 h(sF0_fnc)=h(sF1_fnc)),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f15,f203])).
% 0.09/0.38 fof(f218,plain,(
% 0.09/0.38 sF0_fnc=sF1_fnc),
% 0.09/0.38 inference(forward_demodulation,[status(thm)],[f99,f207])).
% 0.09/0.38 fof(f219,plain,(
% 0.09/0.38 $false),
% 0.09/0.38 inference(forward_subsumption_resolution,[status(thm)],[f218,f31])).
% 0.09/0.38 % SZS output end CNFRefutation for theBenchmark.p
% 0.09/0.40 % Elapsed time: 0.026165 seconds
% 0.09/0.40 % CPU time: 0.043035 seconds
% 0.09/0.40 % Total memory used: 1.814 MB
% 0.09/0.40 % Net memory used: 1.792 MB
%------------------------------------------------------------------------------