%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG226+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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:52 AM UTC 2026
% Result : Theorem 15.79s 5.99s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : ALG226+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.45 % Computer : n001.cluster.edu
% 0.17/0.45 % Model : x86_64 x86_64
% 0.17/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.45 % Memory : 8046.5625MB
% 0.17/0.45 % OS : Linux 6.8.0-71-generic
% 0.17/0.45 % CPULimit : 300
% 0.17/0.45 % WCLimit : 300
% 0.17/0.45 % DateTime : Mon Sep 21 13:12:01 UTC 2026
% 0.17/0.45 % CPUTime :
% 4.02/4.38 % Drodi V4.1.1
% 15.79/5.99 % Refutation found
% 15.79/5.99 % SZS status Theorem for theBenchmark: Theorem is valid
% 15.79/5.99 % SZS output start CNFRefutation for theBenchmark
% 15.79/5.99 fof(f5405,axiom,(
% 15.79/5.99 (! [A,B,C] :( ( m1_pboole(B,A)& m1_pboole(C,A) )=> ( r6_pboole(A,B,C)<=> B = C ) ) )),
% 15.79/5.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.79/5.99 fof(f16950,axiom,(
% 15.79/5.99 (! [A] :( ~ v1_xboole_0(A)=> (! [B] :( ( v2_relat_1(B)& m1_pboole(B,A) )=> B = k1_funct_4(k1_pboole(A),k7_relat_1(B,k1_closure3(A,B))) ) )) )),
% 15.79/5.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.79/5.99 fof(f16951,conjecture,(
% 15.79/5.99 (! [A] :( ~ v1_xboole_0(A)=> (! [B] :( ( v2_relat_1(B)& m1_pboole(B,A) )=> (! [C] :( ( v2_relat_1(C)& m1_pboole(C,A) )=> ( ( k1_closure3(A,B) = k1_closure3(A,C)& k7_relat_1(B,k1_closure3(A,B)) = k7_relat_1(C,k1_closure3(A,C)) )=> r6_pboole(A,B,C) ) ) )) )) )),
% 15.79/5.99 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 15.79/5.99 fof(f16952,negated_conjecture,(
% 15.79/5.99 ~((! [A] :( ~ v1_xboole_0(A)=> (! [B] :( ( v2_relat_1(B)& m1_pboole(B,A) )=> (! [C] :( ( v2_relat_1(C)& m1_pboole(C,A) )=> ( ( k1_closure3(A,B) = k1_closure3(A,C)& k7_relat_1(B,k1_closure3(A,B)) = k7_relat_1(C,k1_closure3(A,C)) )=> r6_pboole(A,B,C) ) ) )) )) ))),
% 15.79/5.99 inference(negated_conjecture,[status(cth)],[f16951])).
% 15.79/5.99 fof(f33054,plain,(
% 15.79/5.99 ![A,B,C]: ((~m1_pboole(B,A)|~m1_pboole(C,A))|(r6_pboole(A,B,C)<=>B=C))),
% 15.79/5.99 inference(pre_NNF_transformation,[status(thm)],[f5405])).
% 15.79/5.99 fof(f33055,plain,(
% 15.79/5.99 ![A,B,C]: ((~m1_pboole(B,A)|~m1_pboole(C,A))|((~r6_pboole(A,B,C)|B=C)&(r6_pboole(A,B,C)|~B=C)))),
% 15.79/5.99 inference(NNF_transformation,[status(thm)],[f33054])).
% 15.79/5.99 fof(f33057,plain,(
% 15.79/5.99 ![X0,X1,X2]: (~m1_pboole(X0,X1)|~m1_pboole(X2,X1)|r6_pboole(X1,X0,X2)|~X0=X2)),
% 15.79/5.99 inference(cnf_transformation,[status(thm)],[f33055])).
% 15.79/5.99 fof(f75975,plain,(
% 15.79/5.99 ![A]: (v1_xboole_0(A)|(![B]: ((~v2_relat_1(B)|~m1_pboole(B,A))|B=k1_funct_4(k1_pboole(A),k7_relat_1(B,k1_closure3(A,B))))))),
% 15.79/5.99 inference(pre_NNF_transformation,[status(thm)],[f16950])).
% 15.79/5.99 fof(f75976,plain,(
% 15.79/5.99 ![X0,X1]: (v1_xboole_0(X0)|~v2_relat_1(X1)|~m1_pboole(X1,X0)|X1=k1_funct_4(k1_pboole(X0),k7_relat_1(X1,k1_closure3(X0,X1))))),
% 15.79/5.99 inference(cnf_transformation,[status(thm)],[f75975])).
% 15.79/5.99 fof(f75977,plain,(
% 15.79/5.99 (?[A]: (~v1_xboole_0(A)&(?[B]: ((v2_relat_1(B)&m1_pboole(B,A))&(?[C]: ((v2_relat_1(C)&m1_pboole(C,A))&((k1_closure3(A,B)=k1_closure3(A,C)&k7_relat_1(B,k1_closure3(A,B))=k7_relat_1(C,k1_closure3(A,C)))&~r6_pboole(A,B,C))))))))),
% 15.79/5.99 inference(pre_NNF_transformation,[status(thm)],[f16952])).
% 15.79/5.99 fof(f75978,plain,(
% 15.79/5.99 (~v1_xboole_0(sK5437_skl)&((v2_relat_1(sK5438_skl)&m1_pboole(sK5438_skl,sK5437_skl))&((v2_relat_1(sK5439_skl)&m1_pboole(sK5439_skl,sK5437_skl))&((k1_closure3(sK5437_skl,sK5438_skl)=k1_closure3(sK5437_skl,sK5439_skl)&k7_relat_1(sK5438_skl,k1_closure3(sK5437_skl,sK5438_skl))=k7_relat_1(sK5439_skl,k1_closure3(sK5437_skl,sK5439_skl)))&~r6_pboole(sK5437_skl,sK5438_skl,sK5439_skl)))))),
% 15.79/5.99 inference(skolemize,[status(esa),new_symbols(skolem,[sK5437_skl,sK5438_skl,sK5439_skl]),skolemize(A,sK5437_skl),skolemize(B,sK5438_skl),skolemize(C,sK5439_skl)],[f75977])).
% 15.79/5.99 fof(f75979,plain,(
% 15.79/5.99 ~v1_xboole_0(sK5437_skl)),
% 15.79/5.99 inference(cnf_transformation,[status(thm)],[f75978])).
% 15.79/5.99 fof(f75980,plain,(
% 15.79/5.99 v2_relat_1(sK5438_skl)),
% 15.79/5.99 inference(cnf_transformation,[status(thm)],[f75978])).
% 15.79/5.99 fof(f75981,plain,(
% 15.79/5.99 m1_pboole(sK5438_skl,sK5437_skl)),
% 15.79/5.99 inference(cnf_transformation,[status(thm)],[f75978])).
% 15.79/5.99 fof(f75982,plain,(
% 15.79/5.99 v2_relat_1(sK5439_skl)),
% 15.79/5.99 inference(cnf_transformation,[status(thm)],[f75978])).
% 15.79/5.99 fof(f75983,plain,(
% 15.79/5.99 m1_pboole(sK5439_skl,sK5437_skl)),
% 15.79/5.99 inference(cnf_transformation,[status(thm)],[f75978])).
% 15.79/5.99 fof(f75984,plain,(
% 15.79/5.99 k1_closure3(sK5437_skl,sK5438_skl)=k1_closure3(sK5437_skl,sK5439_skl)),
% 15.79/5.99 inference(cnf_transformation,[status(thm)],[f75978])).
% 15.79/5.99 fof(f75985,plain,(
% 15.79/5.99 k7_relat_1(sK5438_skl,k1_closure3(sK5437_skl,sK5438_skl))=k7_relat_1(sK5439_skl,k1_closure3(sK5437_skl,sK5439_skl))),
% 15.79/5.99 inference(cnf_transformation,[status(thm)],[f75978])).
% 15.79/5.99 fof(f75986,plain,(
% 15.79/5.99 ~r6_pboole(sK5437_skl,sK5438_skl,sK5439_skl)),
% 15.79/5.99 inference(cnf_transformation,[status(thm)],[f75978])).
% 15.79/5.99 fof(f81197,plain,(
% 15.79/5.99 ![X2,X1]: (~m1_pboole(X2,X1)|~m1_pboole(X2,X1)|r6_pboole(X1,X2,X2))),
% 15.70/6.30 inference(destructive_equality_resolution,[status(thm)],[f33057])).
% 15.70/6.30 fof(f81198,plain,(
% 15.70/6.30 ![X0,X1]: (~m1_pboole(X0,X1)|r6_pboole(X1,X0,X0))),
% 15.70/6.30 inference(duplicate_literals_removal,[status(thm)],[f81197])).
% 15.70/6.30 fof(f83951,plain,(
% 15.70/6.30 k7_relat_1(sK5438_skl,k1_closure3(sK5437_skl,sK5438_skl))=k7_relat_1(sK5439_skl,k1_closure3(sK5437_skl,sK5438_skl))),
% 15.70/6.30 inference(forward_demodulation,[status(thm)],[f75984,f75985])).
% 15.70/6.30 fof(f86201,plain,(
% 15.70/6.30 r6_pboole(sK5437_skl,sK5438_skl,sK5438_skl)),
% 15.70/6.30 inference(resolution,[status(thm)],[f81198,f75981])).
% 15.70/6.30 fof(f87014,plain,(
% 15.70/6.30 v1_xboole_0(sK5437_skl)|~v2_relat_1(sK5439_skl)|sK5439_skl=k1_funct_4(k1_pboole(sK5437_skl),k7_relat_1(sK5439_skl,k1_closure3(sK5437_skl,sK5439_skl)))),
% 15.70/6.30 inference(resolution,[status(thm)],[f75976,f75983])).
% 15.70/6.30 fof(f87015,plain,(
% 15.70/6.30 v1_xboole_0(sK5437_skl)|~v2_relat_1(sK5438_skl)|sK5438_skl=k1_funct_4(k1_pboole(sK5437_skl),k7_relat_1(sK5438_skl,k1_closure3(sK5437_skl,sK5438_skl)))),
% 15.70/6.30 inference(resolution,[status(thm)],[f75976,f75981])).
% 15.70/6.30 fof(f87016,plain,(
% 15.70/6.30 v1_xboole_0(sK5437_skl)|~v2_relat_1(sK5439_skl)|sK5439_skl=k1_funct_4(k1_pboole(sK5437_skl),k7_relat_1(sK5439_skl,k1_closure3(sK5437_skl,sK5438_skl)))),
% 15.70/6.30 inference(forward_demodulation,[status(thm)],[f75984,f87014])).
% 15.70/6.30 fof(f87017,plain,(
% 15.70/6.30 v1_xboole_0(sK5437_skl)|~v2_relat_1(sK5439_skl)|sK5439_skl=k1_funct_4(k1_pboole(sK5437_skl),k7_relat_1(sK5438_skl,k1_closure3(sK5437_skl,sK5438_skl)))),
% 15.70/6.30 inference(forward_demodulation,[status(thm)],[f83951,f87016])).
% 15.70/6.30 fof(f87018,plain,(
% 15.70/6.30 ~v2_relat_1(sK5439_skl)|sK5439_skl=k1_funct_4(k1_pboole(sK5437_skl),k7_relat_1(sK5438_skl,k1_closure3(sK5437_skl,sK5438_skl)))),
% 15.70/6.30 inference(forward_subsumption_resolution,[status(thm)],[f87017,f75979])).
% 15.70/6.30 fof(f87019,plain,(
% 15.70/6.30 ~v2_relat_1(sK5438_skl)|sK5438_skl=k1_funct_4(k1_pboole(sK5437_skl),k7_relat_1(sK5438_skl,k1_closure3(sK5437_skl,sK5438_skl)))),
% 15.70/6.30 inference(forward_subsumption_resolution,[status(thm)],[f87015,f75979])).
% 15.70/6.30 fof(f87255,plain,(
% 15.70/6.30 sK5439_skl=k1_funct_4(k1_pboole(sK5437_skl),k7_relat_1(sK5438_skl,k1_closure3(sK5437_skl,sK5438_skl)))),
% 15.70/6.30 inference(forward_subsumption_resolution,[status(thm)],[f87018,f75982])).
% 15.70/6.30 fof(f87256,plain,(
% 15.70/6.30 ~v2_relat_1(sK5438_skl)|sK5438_skl=sK5439_skl),
% 15.70/6.30 inference(forward_demodulation,[status(thm)],[f87255,f87019])).
% 15.70/6.30 fof(f87282,plain,(
% 15.70/6.30 ~r6_pboole(sK5437_skl,sK5438_skl,sK5438_skl)),
% 15.70/6.30 inference(backward_demodulation,[status(thm)],[f87287,f75986])).
% 15.70/6.30 fof(f87287,plain,(
% 15.70/6.30 sK5438_skl=sK5439_skl),
% 15.70/6.30 inference(forward_subsumption_resolution,[status(thm)],[f87256,f75980])).
% 15.70/6.30 fof(f87306,plain,(
% 15.70/6.30 $false),
% 15.70/6.30 inference(forward_subsumption_resolution,[status(thm)],[f87282,f86201])).
% 15.70/6.30 % SZS output end CNFRefutation for theBenchmark.p
% 4.73/6.60 % Elapsed time: 6.094139 seconds
% 4.73/6.60 % CPU time: 16.908185 seconds
% 4.73/6.60 % Total memory used: 4.514 GB
% 4.73/6.60 % Net memory used: 4.485 GB
%------------------------------------------------------------------------------