%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG226+2 : 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 : n007.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 9.22s 2.26s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ALG226+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n007.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Mon Sep 21 13:04:36 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.82/1.11 % Drodi V4.1.1
% 9.22/2.26 % Refutation found
% 9.22/2.26 % SZS status Theorem for theBenchmark: Theorem is valid
% 9.22/2.26 % SZS output start CNFRefutation for theBenchmark
% 9.22/2.26 fof(f3148,axiom,(
% 9.22/2.26 (! [A,B,C] :( ( m1_pboole(B,A)& m1_pboole(C,A) )=> ( r6_pboole(A,B,C)<=> B = C ) ) )),
% 9.22/2.26 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.22/2.26 fof(f4730,axiom,(
% 9.22/2.26 (! [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))) ) )) )),
% 9.22/2.26 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.22/2.26 fof(f4731,conjecture,(
% 9.22/2.26 (! [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) ) ) )) )) )),
% 9.22/2.26 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 9.22/2.26 fof(f4732,negated_conjecture,(
% 9.22/2.26 ~((! [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) ) ) )) )) ))),
% 9.22/2.26 inference(negated_conjecture,[status(cth)],[f4731])).
% 9.22/2.26 fof(f14066,plain,(
% 9.22/2.26 ![A,B,C]: ((~m1_pboole(B,A)|~m1_pboole(C,A))|(r6_pboole(A,B,C)<=>B=C))),
% 9.22/2.26 inference(pre_NNF_transformation,[status(thm)],[f3148])).
% 9.22/2.26 fof(f14067,plain,(
% 9.22/2.26 ![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)))),
% 9.22/2.26 inference(NNF_transformation,[status(thm)],[f14066])).
% 9.22/2.26 fof(f14069,plain,(
% 9.22/2.26 ![X0,X1,X2]: (~m1_pboole(X0,X1)|~m1_pboole(X2,X1)|r6_pboole(X1,X0,X2)|~X0=X2)),
% 9.22/2.26 inference(cnf_transformation,[status(thm)],[f14067])).
% 9.22/2.26 fof(f19243,plain,(
% 9.22/2.26 ![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))))))),
% 9.22/2.26 inference(pre_NNF_transformation,[status(thm)],[f4730])).
% 9.22/2.26 fof(f19244,plain,(
% 9.22/2.26 ![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))))),
% 9.22/2.26 inference(cnf_transformation,[status(thm)],[f19243])).
% 9.22/2.26 fof(f19245,plain,(
% 9.22/2.26 (?[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))))))))),
% 9.22/2.26 inference(pre_NNF_transformation,[status(thm)],[f4732])).
% 9.22/2.26 fof(f19246,plain,(
% 9.22/2.26 (~v1_xboole_0(sK1314_skl)&((v2_relat_1(sK1315_skl)&m1_pboole(sK1315_skl,sK1314_skl))&((v2_relat_1(sK1316_skl)&m1_pboole(sK1316_skl,sK1314_skl))&((k1_closure3(sK1314_skl,sK1315_skl)=k1_closure3(sK1314_skl,sK1316_skl)&k7_relat_1(sK1315_skl,k1_closure3(sK1314_skl,sK1315_skl))=k7_relat_1(sK1316_skl,k1_closure3(sK1314_skl,sK1316_skl)))&~r6_pboole(sK1314_skl,sK1315_skl,sK1316_skl)))))),
% 9.22/2.26 inference(skolemize,[status(esa),new_symbols(skolem,[sK1314_skl,sK1315_skl,sK1316_skl]),skolemize(A,sK1314_skl),skolemize(B,sK1315_skl),skolemize(C,sK1316_skl)],[f19245])).
% 9.22/2.26 fof(f19247,plain,(
% 9.22/2.26 ~v1_xboole_0(sK1314_skl)),
% 9.22/2.26 inference(cnf_transformation,[status(thm)],[f19246])).
% 9.22/2.26 fof(f19248,plain,(
% 9.22/2.26 v2_relat_1(sK1315_skl)),
% 9.22/2.26 inference(cnf_transformation,[status(thm)],[f19246])).
% 9.22/2.26 fof(f19249,plain,(
% 9.22/2.26 m1_pboole(sK1315_skl,sK1314_skl)),
% 9.22/2.26 inference(cnf_transformation,[status(thm)],[f19246])).
% 9.22/2.26 fof(f19250,plain,(
% 9.22/2.26 v2_relat_1(sK1316_skl)),
% 9.22/2.26 inference(cnf_transformation,[status(thm)],[f19246])).
% 9.22/2.26 fof(f19251,plain,(
% 9.22/2.26 m1_pboole(sK1316_skl,sK1314_skl)),
% 9.22/2.26 inference(cnf_transformation,[status(thm)],[f19246])).
% 9.22/2.26 fof(f19252,plain,(
% 9.22/2.26 k1_closure3(sK1314_skl,sK1315_skl)=k1_closure3(sK1314_skl,sK1316_skl)),
% 9.22/2.26 inference(cnf_transformation,[status(thm)],[f19246])).
% 9.22/2.26 fof(f19253,plain,(
% 9.22/2.26 k7_relat_1(sK1315_skl,k1_closure3(sK1314_skl,sK1315_skl))=k7_relat_1(sK1316_skl,k1_closure3(sK1314_skl,sK1316_skl))),
% 9.22/2.26 inference(cnf_transformation,[status(thm)],[f19246])).
% 9.22/2.26 fof(f19254,plain,(
% 9.22/2.26 ~r6_pboole(sK1314_skl,sK1315_skl,sK1316_skl)),
% 9.22/2.26 inference(cnf_transformation,[status(thm)],[f19246])).
% 9.22/2.26 fof(f21098,plain,(
% 9.22/2.26 ![X2,X1]: (~m1_pboole(X2,X1)|~m1_pboole(X2,X1)|r6_pboole(X1,X2,X2))),
% 6.46/2.37 inference(destructive_equality_resolution,[status(thm)],[f14069])).
% 6.46/2.37 fof(f21099,plain,(
% 6.46/2.37 ![X0,X1]: (~m1_pboole(X0,X1)|r6_pboole(X1,X0,X0))),
% 6.46/2.37 inference(duplicate_literals_removal,[status(thm)],[f21098])).
% 6.46/2.37 fof(f21584,plain,(
% 6.46/2.37 k7_relat_1(sK1315_skl,k1_closure3(sK1314_skl,sK1315_skl))=k7_relat_1(sK1316_skl,k1_closure3(sK1314_skl,sK1315_skl))),
% 6.46/2.37 inference(forward_demodulation,[status(thm)],[f19252,f19253])).
% 6.46/2.37 fof(f23455,plain,(
% 6.46/2.37 r6_pboole(sK1314_skl,sK1315_skl,sK1315_skl)),
% 6.46/2.37 inference(resolution,[status(thm)],[f21099,f19249])).
% 6.46/2.37 fof(f23703,plain,(
% 6.46/2.37 v1_xboole_0(sK1314_skl)|~v2_relat_1(sK1316_skl)|sK1316_skl=k1_funct_4(k1_pboole(sK1314_skl),k7_relat_1(sK1316_skl,k1_closure3(sK1314_skl,sK1316_skl)))),
% 6.46/2.37 inference(resolution,[status(thm)],[f19244,f19251])).
% 6.46/2.37 fof(f23704,plain,(
% 6.46/2.37 v1_xboole_0(sK1314_skl)|~v2_relat_1(sK1315_skl)|sK1315_skl=k1_funct_4(k1_pboole(sK1314_skl),k7_relat_1(sK1315_skl,k1_closure3(sK1314_skl,sK1315_skl)))),
% 6.46/2.37 inference(resolution,[status(thm)],[f19244,f19249])).
% 6.46/2.37 fof(f23705,plain,(
% 6.46/2.37 v1_xboole_0(sK1314_skl)|~v2_relat_1(sK1316_skl)|sK1316_skl=k1_funct_4(k1_pboole(sK1314_skl),k7_relat_1(sK1316_skl,k1_closure3(sK1314_skl,sK1315_skl)))),
% 6.46/2.37 inference(forward_demodulation,[status(thm)],[f19252,f23703])).
% 6.46/2.37 fof(f23706,plain,(
% 6.46/2.37 v1_xboole_0(sK1314_skl)|~v2_relat_1(sK1316_skl)|sK1316_skl=k1_funct_4(k1_pboole(sK1314_skl),k7_relat_1(sK1315_skl,k1_closure3(sK1314_skl,sK1315_skl)))),
% 6.46/2.37 inference(forward_demodulation,[status(thm)],[f21584,f23705])).
% 6.46/2.37 fof(f23707,plain,(
% 6.46/2.37 ~v2_relat_1(sK1316_skl)|sK1316_skl=k1_funct_4(k1_pboole(sK1314_skl),k7_relat_1(sK1315_skl,k1_closure3(sK1314_skl,sK1315_skl)))),
% 6.46/2.37 inference(forward_subsumption_resolution,[status(thm)],[f23706,f19247])).
% 6.46/2.37 fof(f23708,plain,(
% 6.46/2.37 ~v2_relat_1(sK1315_skl)|sK1315_skl=k1_funct_4(k1_pboole(sK1314_skl),k7_relat_1(sK1315_skl,k1_closure3(sK1314_skl,sK1315_skl)))),
% 6.46/2.37 inference(forward_subsumption_resolution,[status(thm)],[f23704,f19247])).
% 6.46/2.37 fof(f23947,plain,(
% 6.46/2.37 sK1316_skl=k1_funct_4(k1_pboole(sK1314_skl),k7_relat_1(sK1315_skl,k1_closure3(sK1314_skl,sK1315_skl)))),
% 6.46/2.37 inference(forward_subsumption_resolution,[status(thm)],[f23707,f19250])).
% 6.46/2.37 fof(f23948,plain,(
% 6.46/2.37 ~v2_relat_1(sK1315_skl)|sK1315_skl=sK1316_skl),
% 6.46/2.37 inference(forward_demodulation,[status(thm)],[f23947,f23708])).
% 6.46/2.37 fof(f23971,plain,(
% 6.46/2.37 ~r6_pboole(sK1314_skl,sK1315_skl,sK1315_skl)),
% 6.46/2.37 inference(backward_demodulation,[status(thm)],[f23975,f19254])).
% 6.46/2.37 fof(f23975,plain,(
% 6.46/2.37 sK1315_skl=sK1316_skl),
% 6.46/2.37 inference(forward_subsumption_resolution,[status(thm)],[f23948,f19248])).
% 6.46/2.37 fof(f23989,plain,(
% 6.46/2.37 $false),
% 6.46/2.37 inference(forward_subsumption_resolution,[status(thm)],[f23971,f23455])).
% 6.46/2.37 % SZS output end CNFRefutation for theBenchmark.p
% 6.46/2.39 % Elapsed time: 1.927061 seconds
% 6.46/2.39 % CPU time: 9.873199 seconds
% 6.46/2.39 % Total memory used: 789.119 MB
% 6.46/2.39 % Net memory used: 776.068 MB
%------------------------------------------------------------------------------