%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : ALG227+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 : n009.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:53 AM UTC 2026
% Result : Theorem 105.71s 14.24s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG227+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n009.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 13:07:00 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.55/0.83 % Drodi V4.1.1
% 105.71/14.24 % Refutation found
% 105.71/14.24 % SZS status Theorem for theBenchmark: Theorem is valid
% 105.71/14.24 % SZS output start CNFRefutation for theBenchmark
% 105.71/14.24 fof(f4703,axiom,(
% 105.71/14.24 (! [A,B,C] :( ( ~ v1_xboole_0(B)& m1_pboole(C,B) )=> ( r2_hidden(A,a_2_0_closure3(B,C))<=> (? [D] :( m1_subset_1(D,B)& A = D& k1_funct_1(C,D) != k1_xboole_0 ) )) ) )),
% 105.71/14.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 105.71/14.24 fof(f4728,axiom,(
% 105.71/14.24 (! [A] :( ~ v1_xboole_0(A)=> (! [B] :( m1_pboole(B,A)=> (! [C] :( C = k1_closure3(A,B)<=> C = a_2_0_closure3(A,B) ) )) )) )),
% 105.71/14.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 105.71/14.24 fof(f4731,conjecture,(
% 105.71/14.24 (! [A] :( ~ v1_xboole_0(A)=> (! [B] :( m1_pboole(B,A)=> (! [C] :( m1_subset_1(C,A)=> ( ~ r2_hidden(C,k1_closure3(A,B))=> k1_funct_1(B,C) = k1_xboole_0 ) ) )) )) )),
% 105.71/14.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 105.71/14.24 fof(f4732,negated_conjecture,(
% 105.71/14.24 ~((! [A] :( ~ v1_xboole_0(A)=> (! [B] :( m1_pboole(B,A)=> (! [C] :( m1_subset_1(C,A)=> ( ~ r2_hidden(C,k1_closure3(A,B))=> k1_funct_1(B,C) = k1_xboole_0 ) ) )) )) ))),
% 105.71/14.24 inference(negated_conjecture,[status(cth)],[f4731])).
% 105.71/14.24 fof(f19156,plain,(
% 105.71/14.24 ![A,B,C]: ((v1_xboole_0(B)|~m1_pboole(C,B))|(r2_hidden(A,a_2_0_closure3(B,C))<=>(?[D]: ((m1_subset_1(D,B)&A=D)&~k1_funct_1(C,D)=k1_xboole_0))))),
% 105.71/14.24 inference(pre_NNF_transformation,[status(thm)],[f4703])).
% 105.71/14.24 fof(f19157,plain,(
% 105.71/14.24 ![A,B,C]: ((v1_xboole_0(B)|~m1_pboole(C,B))|((~r2_hidden(A,a_2_0_closure3(B,C))|(?[D]: ((m1_subset_1(D,B)&A=D)&~k1_funct_1(C,D)=k1_xboole_0)))&(r2_hidden(A,a_2_0_closure3(B,C))|(![D]: ((~m1_subset_1(D,B)|~A=D)|k1_funct_1(C,D)=k1_xboole_0)))))),
% 105.71/14.24 inference(NNF_transformation,[status(thm)],[f19156])).
% 105.71/14.24 fof(f19158,plain,(
% 105.71/14.24 ![B,C]: ((v1_xboole_0(B)|~m1_pboole(C,B))|((![A]: (~r2_hidden(A,a_2_0_closure3(B,C))|(?[D]: ((m1_subset_1(D,B)&A=D)&~k1_funct_1(C,D)=k1_xboole_0))))&(![A]: (r2_hidden(A,a_2_0_closure3(B,C))|(![D]: ((~m1_subset_1(D,B)|~A=D)|k1_funct_1(C,D)=k1_xboole_0))))))),
% 105.71/14.24 inference(miniscoping,[status(thm)],[f19157])).
% 105.71/14.24 fof(f19159,plain,(
% 105.71/14.24 ![B,C]: ((v1_xboole_0(B)|~m1_pboole(C,B))|((![A]: (~r2_hidden(A,a_2_0_closure3(B,C))|((m1_subset_1(sK1307_skl(A,C,B),B)&A=sK1307_skl(A,C,B))&~k1_funct_1(C,sK1307_skl(A,C,B))=k1_xboole_0)))&(![A]: (r2_hidden(A,a_2_0_closure3(B,C))|(![D]: ((~m1_subset_1(D,B)|~A=D)|k1_funct_1(C,D)=k1_xboole_0))))))),
% 105.71/14.24 inference(skolemize,[status(esa),new_symbols(skolem,[sK1307_skl]),skolemize(D,sK1307_skl(A,C,B))],[f19158])).
% 105.71/14.24 fof(f19163,plain,(
% 105.71/14.24 ![X0,X1,X2,X3]: (v1_xboole_0(X0)|~m1_pboole(X1,X0)|r2_hidden(X2,a_2_0_closure3(X0,X1))|~m1_subset_1(X3,X0)|~X2=X3|k1_funct_1(X1,X3)=k1_xboole_0)),
% 105.71/14.24 inference(cnf_transformation,[status(thm)],[f19159])).
% 105.71/14.24 fof(f19230,plain,(
% 105.71/14.24 ![A]: (v1_xboole_0(A)|(![B]: (~m1_pboole(B,A)|(![C]: (C=k1_closure3(A,B)<=>C=a_2_0_closure3(A,B))))))),
% 105.71/14.24 inference(pre_NNF_transformation,[status(thm)],[f4728])).
% 105.71/14.24 fof(f19231,plain,(
% 105.71/14.24 ![A]: (v1_xboole_0(A)|(![B]: (~m1_pboole(B,A)|(![C]: ((~C=k1_closure3(A,B)|C=a_2_0_closure3(A,B))&(C=k1_closure3(A,B)|~C=a_2_0_closure3(A,B)))))))),
% 105.71/14.24 inference(NNF_transformation,[status(thm)],[f19230])).
% 105.71/14.24 fof(f19232,plain,(
% 105.71/14.24 ![A]: (v1_xboole_0(A)|(![B]: (~m1_pboole(B,A)|((![C]: (~C=k1_closure3(A,B)|C=a_2_0_closure3(A,B)))&(![C]: (C=k1_closure3(A,B)|~C=a_2_0_closure3(A,B)))))))),
% 105.71/14.24 inference(miniscoping,[status(thm)],[f19231])).
% 105.71/14.24 fof(f19233,plain,(
% 105.71/14.24 ![X0,X1,X2]: (v1_xboole_0(X0)|~m1_pboole(X1,X0)|~X2=k1_closure3(X0,X1)|X2=a_2_0_closure3(X0,X1))),
% 105.71/14.24 inference(cnf_transformation,[status(thm)],[f19232])).
% 105.71/14.24 fof(f19239,plain,(
% 105.71/14.24 (?[A]: (~v1_xboole_0(A)&(?[B]: (m1_pboole(B,A)&(?[C]: (m1_subset_1(C,A)&(~r2_hidden(C,k1_closure3(A,B))&~k1_funct_1(B,C)=k1_xboole_0)))))))),
% 105.71/14.24 inference(pre_NNF_transformation,[status(thm)],[f4732])).
% 105.71/14.24 fof(f19240,plain,(
% 105.71/14.24 (~v1_xboole_0(sK1313_skl)&(m1_pboole(sK1314_skl,sK1313_skl)&(m1_subset_1(sK1315_skl,sK1313_skl)&(~r2_hidden(sK1315_skl,k1_closure3(sK1313_skl,sK1314_skl))&~k1_funct_1(sK1314_skl,sK1315_skl)=k1_xboole_0))))),
% 105.71/14.24 inference(skolemize,[status(esa),new_symbols(skolem,[sK1313_skl,sK1314_skl,sK1315_skl]),skolemize(A,sK1313_skl),skolemize(B,sK1314_skl),skolemize(C,sK1315_skl)],[f19239])).
% 105.71/14.24 fof(f19241,plain,(
% 105.71/14.24 ~v1_xboole_0(sK1313_skl)),
% 105.71/14.24 inference(cnf_transformation,[status(thm)],[f19240])).
% 105.71/14.24 fof(f19242,plain,(
% 105.71/14.24 m1_pboole(sK1314_skl,sK1313_skl)),
% 105.71/14.24 inference(cnf_transformation,[status(thm)],[f19240])).
% 105.71/14.24 fof(f19243,plain,(
% 105.71/14.24 m1_subset_1(sK1315_skl,sK1313_skl)),
% 105.71/14.24 inference(cnf_transformation,[status(thm)],[f19240])).
% 105.71/14.24 fof(f19244,plain,(
% 105.71/14.24 ~r2_hidden(sK1315_skl,k1_closure3(sK1313_skl,sK1314_skl))),
% 105.71/14.24 inference(cnf_transformation,[status(thm)],[f19240])).
% 105.71/14.24 fof(f19245,plain,(
% 105.71/14.24 ~k1_funct_1(sK1314_skl,sK1315_skl)=k1_xboole_0),
% 105.71/14.24 inference(cnf_transformation,[status(thm)],[f19240])).
% 105.71/14.24 fof(f23677,plain,(
% 105.71/14.24 ![X0,X1,X2]: (v1_xboole_0(X0)|~m1_pboole(X1,X0)|r2_hidden(X2,a_2_0_closure3(X0,X1))|~m1_subset_1(X2,X0)|k1_funct_1(X1,X2)=k1_xboole_0)),
% 105.71/14.24 inference(destructive_equality_resolution,[status(thm)],[f19163])).
% 105.71/14.24 fof(f23678,plain,(
% 105.71/14.24 ![X0,X1]: (v1_xboole_0(X0)|~m1_pboole(X1,X0)|k1_closure3(X0,X1)=a_2_0_closure3(X0,X1))),
% 105.71/14.24 inference(destructive_equality_resolution,[status(thm)],[f19233])).
% 105.71/14.24 fof(f23858,definition,(
% 105.71/14.24 sQ602_spl <=> (v1_xboole_0(sK1313_skl))),
% 105.71/14.24 introduced(definition,[new_symbols(definition,[sQ602_spl])],[split_symbol_definition])).
% 105.71/14.24 fof(f23859,plain,(
% 105.71/14.24 v1_xboole_0(sK1313_skl)|~sQ602_spl),
% 105.71/14.24 inference(component_clause,[status(thm)],[f23858])).
% 105.71/14.24 fof(f23865,plain,(
% 105.71/14.24 $false|~sQ602_spl),
% 105.71/14.24 inference(forward_subsumption_resolution,[status(thm)],[f23859,f19241])).
% 105.71/14.24 fof(f23866,plain,(
% 105.71/14.24 ~sQ602_spl),
% 105.71/14.24 inference(contradiction_clause,[status(thm)],[f23865])).
% 105.71/14.24 fof(f42842,plain,(
% 105.71/14.24 ![X0]: (v1_xboole_0(sK1313_skl)|r2_hidden(X0,a_2_0_closure3(sK1313_skl,sK1314_skl))|~m1_subset_1(X0,sK1313_skl)|k1_funct_1(sK1314_skl,X0)=k1_xboole_0)),
% 105.71/14.24 inference(resolution,[status(thm)],[f23677,f19242])).
% 105.71/14.24 fof(f42848,definition,(
% 105.71/14.24 ![X0]: (sQ1814_spl <=> (r2_hidden(X0,a_2_0_closure3(sK1313_skl,sK1314_skl))|~m1_subset_1(X0,sK1313_skl)|k1_funct_1(sK1314_skl,X0)=k1_xboole_0))),
% 105.71/14.24 introduced(definition,[new_symbols(definition,[sQ1814_spl])],[split_symbol_definition])).
% 105.71/14.24 fof(f42849,plain,(
% 105.71/14.24 ![X0]: (r2_hidden(X0,a_2_0_closure3(sK1313_skl,sK1314_skl))|~m1_subset_1(X0,sK1313_skl)|k1_funct_1(sK1314_skl,X0)=k1_xboole_0|~sQ1814_spl)),
% 105.71/14.24 inference(component_clause,[status(thm)],[f42848])).
% 105.71/14.24 fof(f42851,plain,(
% 105.71/14.24 sQ602_spl|sQ1814_spl),
% 105.71/14.24 inference(split_clause,[status(thm)],[f42842,f23858,f42848])).
% 105.71/14.24 fof(f42864,plain,(
% 105.71/14.24 v1_xboole_0(sK1313_skl)|k1_closure3(sK1313_skl,sK1314_skl)=a_2_0_closure3(sK1313_skl,sK1314_skl)),
% 105.71/14.24 inference(resolution,[status(thm)],[f23678,f19242])).
% 105.71/14.24 fof(f42870,definition,(
% 105.71/14.24 sQ1818_spl <=> (k1_closure3(sK1313_skl,sK1314_skl)=a_2_0_closure3(sK1313_skl,sK1314_skl))),
% 105.71/14.24 introduced(definition,[new_symbols(definition,[sQ1818_spl])],[split_symbol_definition])).
% 105.71/14.24 fof(f42871,plain,(
% 105.71/14.24 k1_closure3(sK1313_skl,sK1314_skl)=a_2_0_closure3(sK1313_skl,sK1314_skl)|~sQ1818_spl),
% 105.71/14.24 inference(component_clause,[status(thm)],[f42870])).
% 105.71/14.24 fof(f42873,plain,(
% 105.71/14.24 sQ602_spl|sQ1818_spl),
% 105.71/14.24 inference(split_clause,[status(thm)],[f42864,f23858,f42870])).
% 105.71/14.24 fof(f42927,definition,(
% 105.71/14.24 sQ1822_spl <=> (k1_funct_1(sK1314_skl,sK1315_skl)=k1_xboole_0)),
% 105.71/14.24 introduced(definition,[new_symbols(definition,[sQ1822_spl])],[split_symbol_definition])).
% 105.71/14.24 fof(f42928,plain,(
% 105.71/14.24 k1_funct_1(sK1314_skl,sK1315_skl)=k1_xboole_0|~sQ1822_spl),
% 105.71/14.24 inference(component_clause,[status(thm)],[f42927])).
% 105.71/14.24 fof(f42938,plain,(
% 105.71/14.24 $false|~sQ1822_spl),
% 105.71/14.24 inference(forward_subsumption_resolution,[status(thm)],[f42928,f19245])).
% 105.71/14.24 fof(f42939,plain,(
% 105.71/14.24 ~sQ1822_spl),
% 105.71/14.24 inference(contradiction_clause,[status(thm)],[f42938])).
% 105.71/14.24 fof(f43668,plain,(
% 105.71/14.24 ![X0]: (r2_hidden(X0,k1_closure3(sK1313_skl,sK1314_skl))|~m1_subset_1(X0,sK1313_skl)|k1_funct_1(sK1314_skl,X0)=k1_xboole_0|~sQ1818_spl|~sQ1814_spl)),
% 105.71/14.24 inference(backward_demodulation,[status(thm)],[f42871,f42849])).
% 105.71/14.24 fof(f43959,plain,(
% 105.71/14.24 r2_hidden(sK1315_skl,k1_closure3(sK1313_skl,sK1314_skl))|k1_funct_1(sK1314_skl,sK1315_skl)=k1_xboole_0|~sQ1818_spl|~sQ1814_spl),
% 105.71/14.24 inference(resolution,[status(thm)],[f43668,f19243])).
% 105.71/14.24 fof(f43974,definition,(
% 105.71/14.24 sQ1868_spl <=> (r2_hidden(sK1315_skl,k1_closure3(sK1313_skl,sK1314_skl)))),
% 105.71/14.24 introduced(definition,[new_symbols(definition,[sQ1868_spl])],[split_symbol_definition])).
% 105.71/14.32 fof(f43975,plain,(
% 105.71/14.32 r2_hidden(sK1315_skl,k1_closure3(sK1313_skl,sK1314_skl))|~sQ1868_spl),
% 105.71/14.32 inference(component_clause,[status(thm)],[f43974])).
% 105.71/14.32 fof(f43977,plain,(
% 105.71/14.32 sQ1868_spl|sQ1822_spl|~sQ1818_spl|~sQ1814_spl),
% 105.71/14.32 inference(split_clause,[status(thm)],[f43959,f43974,f42927,f42870,f42848])).
% 105.71/14.32 fof(f43982,plain,(
% 105.71/14.32 $false|~sQ1868_spl),
% 105.71/14.32 inference(forward_subsumption_resolution,[status(thm)],[f43975,f19244])).
% 105.71/14.32 fof(f43983,plain,(
% 105.71/14.32 ~sQ1868_spl),
% 105.71/14.32 inference(contradiction_clause,[status(thm)],[f43982])).
% 105.71/14.32 fof(f43984,plain,(
% 105.71/14.32 $false),
% 105.71/14.32 inference(sat_refutation,[status(thm)],[f23866,f42851,f42873,f42939,f43977,f43983])).
% 105.71/14.32 % SZS output end CNFRefutation for theBenchmark.p
% 29.64/14.43 % Elapsed time: 14.036331 seconds
% 29.64/14.43 % CPU time: 107.495778 seconds
% 29.64/14.43 % Total memory used: 1.139 GB
% 29.64/14.43 % Net memory used: 1.068 GB
%------------------------------------------------------------------------------