%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG226+4 : TPTP v9.3.1. Released v3.4.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 11:49:52 AM UTC 2026
% Result : Theorem 48.77s 13.79s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG226+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n004.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 13:06:27 UTC 2026
% 0.12/0.35 % CPUTime :
% 8.25/8.54 % Drodi V4.1.1
% 48.77/13.79 % Refutation found
% 48.77/13.79 % SZS status Theorem for theBenchmark: Theorem is valid
% 48.77/13.79 % SZS output start CNFRefutation for theBenchmark
% 48.77/13.79 fof(f8280,axiom,(
% 48.77/13.79 (! [A,B,C] :( ( m1_pboole(B,A)& m1_pboole(C,A) )=> ( r6_pboole(A,B,C)<=> B = C ) ) )),
% 48.77/13.79 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 48.77/13.79 fof(f42810,axiom,(
% 48.77/13.79 (! [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))) ) )) )),
% 48.77/13.79 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 48.77/13.79 fof(f42811,conjecture,(
% 48.77/13.79 (! [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) ) ) )) )) )),
% 48.77/13.79 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 48.77/13.79 fof(f42812,negated_conjecture,(
% 48.77/13.79 ~((! [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) ) ) )) )) ))),
% 48.77/13.79 inference(negated_conjecture,[status(cth)],[f42811])).
% 48.77/13.79 fof(f66597,plain,(
% 48.77/13.79 ![A,B,C]: ((~m1_pboole(B,A)|~m1_pboole(C,A))|(r6_pboole(A,B,C)<=>B=C))),
% 48.77/13.79 inference(pre_NNF_transformation,[status(thm)],[f8280])).
% 48.77/13.79 fof(f66598,plain,(
% 48.77/13.79 ![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)))),
% 48.77/13.79 inference(NNF_transformation,[status(thm)],[f66597])).
% 48.77/13.79 fof(f66600,plain,(
% 48.77/13.79 ![X0,X1,X2]: (~m1_pboole(X0,X1)|~m1_pboole(X2,X1)|r6_pboole(X1,X0,X2)|~X0=X2)),
% 48.77/13.79 inference(cnf_transformation,[status(thm)],[f66598])).
% 48.77/13.79 fof(f195240,plain,(
% 48.77/13.79 ![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))))))),
% 48.77/13.79 inference(pre_NNF_transformation,[status(thm)],[f42810])).
% 48.77/13.79 fof(f195241,plain,(
% 48.77/13.79 ![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))))),
% 48.77/13.79 inference(cnf_transformation,[status(thm)],[f195240])).
% 48.77/13.79 fof(f195242,plain,(
% 48.77/13.79 (?[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))))))))),
% 48.77/13.79 inference(pre_NNF_transformation,[status(thm)],[f42812])).
% 48.77/13.79 fof(f195243,plain,(
% 48.77/13.79 (~v1_xboole_0(sK15195_skl)&((v2_relat_1(sK15196_skl)&m1_pboole(sK15196_skl,sK15195_skl))&((v2_relat_1(sK15197_skl)&m1_pboole(sK15197_skl,sK15195_skl))&((k1_closure3(sK15195_skl,sK15196_skl)=k1_closure3(sK15195_skl,sK15197_skl)&k7_relat_1(sK15196_skl,k1_closure3(sK15195_skl,sK15196_skl))=k7_relat_1(sK15197_skl,k1_closure3(sK15195_skl,sK15197_skl)))&~r6_pboole(sK15195_skl,sK15196_skl,sK15197_skl)))))),
% 48.77/13.79 inference(skolemize,[status(esa),new_symbols(skolem,[sK15195_skl,sK15196_skl,sK15197_skl]),skolemize(A,sK15195_skl),skolemize(B,sK15196_skl),skolemize(C,sK15197_skl)],[f195242])).
% 48.77/13.79 fof(f195244,plain,(
% 48.77/13.79 ~v1_xboole_0(sK15195_skl)),
% 48.77/13.79 inference(cnf_transformation,[status(thm)],[f195243])).
% 48.77/13.79 fof(f195245,plain,(
% 48.77/13.79 v2_relat_1(sK15196_skl)),
% 48.77/13.79 inference(cnf_transformation,[status(thm)],[f195243])).
% 48.77/13.79 fof(f195246,plain,(
% 48.77/13.79 m1_pboole(sK15196_skl,sK15195_skl)),
% 48.77/13.79 inference(cnf_transformation,[status(thm)],[f195243])).
% 48.77/13.79 fof(f195247,plain,(
% 48.77/13.79 v2_relat_1(sK15197_skl)),
% 48.77/13.79 inference(cnf_transformation,[status(thm)],[f195243])).
% 48.77/13.79 fof(f195248,plain,(
% 48.77/13.79 m1_pboole(sK15197_skl,sK15195_skl)),
% 48.77/13.79 inference(cnf_transformation,[status(thm)],[f195243])).
% 48.77/13.79 fof(f195249,plain,(
% 48.77/13.79 k1_closure3(sK15195_skl,sK15196_skl)=k1_closure3(sK15195_skl,sK15197_skl)),
% 48.77/13.79 inference(cnf_transformation,[status(thm)],[f195243])).
% 48.77/13.79 fof(f195250,plain,(
% 48.77/13.79 k7_relat_1(sK15196_skl,k1_closure3(sK15195_skl,sK15196_skl))=k7_relat_1(sK15197_skl,k1_closure3(sK15195_skl,sK15197_skl))),
% 48.77/13.79 inference(cnf_transformation,[status(thm)],[f195243])).
% 48.77/13.79 fof(f195251,plain,(
% 48.77/13.79 ~r6_pboole(sK15195_skl,sK15196_skl,sK15197_skl)),
% 48.77/13.79 inference(cnf_transformation,[status(thm)],[f195243])).
% 48.77/13.79 fof(f217807,plain,(
% 17.37/14.72 ![X2,X1]: (~m1_pboole(X2,X1)|~m1_pboole(X2,X1)|r6_pboole(X1,X2,X2))),
% 17.37/14.72 inference(destructive_equality_resolution,[status(thm)],[f66600])).
% 17.37/14.72 fof(f217808,plain,(
% 17.37/14.72 ![X0,X1]: (~m1_pboole(X0,X1)|r6_pboole(X1,X0,X0))),
% 17.37/14.72 inference(duplicate_literals_removal,[status(thm)],[f217807])).
% 17.37/14.72 fof(f227277,plain,(
% 17.37/14.72 k7_relat_1(sK15196_skl,k1_closure3(sK15195_skl,sK15196_skl))=k7_relat_1(sK15197_skl,k1_closure3(sK15195_skl,sK15196_skl))),
% 17.37/14.72 inference(forward_demodulation,[status(thm)],[f195249,f195250])).
% 17.37/14.72 fof(f232477,plain,(
% 17.37/14.72 v1_xboole_0(sK15195_skl)|~v2_relat_1(sK15197_skl)|sK15197_skl=k1_funct_4(k1_pboole(sK15195_skl),k7_relat_1(sK15197_skl,k1_closure3(sK15195_skl,sK15197_skl)))),
% 17.37/14.72 inference(resolution,[status(thm)],[f195241,f195248])).
% 17.37/14.72 fof(f232478,plain,(
% 17.37/14.72 v1_xboole_0(sK15195_skl)|~v2_relat_1(sK15196_skl)|sK15196_skl=k1_funct_4(k1_pboole(sK15195_skl),k7_relat_1(sK15196_skl,k1_closure3(sK15195_skl,sK15196_skl)))),
% 17.37/14.72 inference(resolution,[status(thm)],[f195241,f195246])).
% 17.37/14.72 fof(f232481,plain,(
% 17.37/14.72 v1_xboole_0(sK15195_skl)|~v2_relat_1(sK15197_skl)|sK15197_skl=k1_funct_4(k1_pboole(sK15195_skl),k7_relat_1(sK15197_skl,k1_closure3(sK15195_skl,sK15196_skl)))),
% 17.37/14.72 inference(forward_demodulation,[status(thm)],[f195249,f232477])).
% 17.37/14.72 fof(f232482,plain,(
% 17.37/14.72 v1_xboole_0(sK15195_skl)|~v2_relat_1(sK15197_skl)|sK15197_skl=k1_funct_4(k1_pboole(sK15195_skl),k7_relat_1(sK15196_skl,k1_closure3(sK15195_skl,sK15196_skl)))),
% 17.37/14.72 inference(forward_demodulation,[status(thm)],[f227277,f232481])).
% 17.37/14.72 fof(f232483,plain,(
% 17.37/14.72 ~v2_relat_1(sK15197_skl)|sK15197_skl=k1_funct_4(k1_pboole(sK15195_skl),k7_relat_1(sK15196_skl,k1_closure3(sK15195_skl,sK15196_skl)))),
% 17.37/14.72 inference(forward_subsumption_resolution,[status(thm)],[f232482,f195244])).
% 17.37/14.72 fof(f232484,plain,(
% 17.37/14.72 ~v2_relat_1(sK15196_skl)|sK15196_skl=k1_funct_4(k1_pboole(sK15195_skl),k7_relat_1(sK15196_skl,k1_closure3(sK15195_skl,sK15196_skl)))),
% 17.37/14.72 inference(forward_subsumption_resolution,[status(thm)],[f232478,f195244])).
% 17.37/14.72 fof(f232549,plain,(
% 17.37/14.72 sK15197_skl=k1_funct_4(k1_pboole(sK15195_skl),k7_relat_1(sK15196_skl,k1_closure3(sK15195_skl,sK15196_skl)))),
% 17.37/14.72 inference(forward_subsumption_resolution,[status(thm)],[f232483,f195247])).
% 17.37/14.72 fof(f232550,plain,(
% 17.37/14.72 ~v2_relat_1(sK15196_skl)|sK15196_skl=sK15197_skl),
% 17.37/14.72 inference(forward_demodulation,[status(thm)],[f232549,f232484])).
% 17.37/14.72 fof(f232575,plain,(
% 17.37/14.72 ~r6_pboole(sK15195_skl,sK15196_skl,sK15196_skl)),
% 17.37/14.72 inference(backward_demodulation,[status(thm)],[f232579,f195251])).
% 17.37/14.72 fof(f232579,plain,(
% 17.37/14.72 sK15196_skl=sK15197_skl),
% 17.37/14.72 inference(forward_subsumption_resolution,[status(thm)],[f232550,f195245])).
% 17.37/14.72 fof(f232762,plain,(
% 17.37/14.72 ~m1_pboole(sK15196_skl,sK15195_skl)),
% 17.37/14.72 inference(resolution,[status(thm)],[f232575,f217808])).
% 17.37/14.72 fof(f232763,plain,(
% 17.37/14.72 $false),
% 17.37/14.72 inference(forward_subsumption_resolution,[status(thm)],[f232762,f195246])).
% 17.37/14.72 % SZS output end CNFRefutation for theBenchmark.p
% 9.71/14.89 % Elapsed time: 14.374024 seconds
% 9.71/14.89 % CPU time: 50.448994 seconds
% 9.71/14.89 % Total memory used: 12.905 GB
% 9.71/14.89 % Net memory used: 12.811 GB
%------------------------------------------------------------------------------