%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU406+3 : 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 : n026.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 02:22:32 PM UTC 2026
% Result : Theorem 34.43s 7.24s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU406+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.40 % Computer : n026.cluster.edu
% 0.14/0.40 % Model : x86_64 x86_64
% 0.14/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40 % Memory : 8046.5625MB
% 0.14/0.40 % OS : Linux 6.8.0-71-generic
% 0.14/0.40 % CPULimit : 300
% 0.14/0.40 % WCLimit : 300
% 0.14/0.40 % DateTime : Mon Sep 21 06:23:42 UTC 2026
% 0.14/0.40 % CPUTime :
% 2.77/3.08 % Drodi V4.1.1
% 34.43/7.24 % Refutation found
% 34.43/7.24 % SZS status Theorem for theBenchmark: Theorem is valid
% 34.43/7.24 % SZS output start CNFRefutation for theBenchmark
% 34.43/7.24 fof(f4,axiom,(
% 34.43/7.24 (! [A,B] :( B = k1_tarski(A)<=> (! [C] :( r2_hidden(C,B)<=> C = A ) )) )),
% 34.43/7.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 34.43/7.24 fof(f30,axiom,(
% 34.43/7.24 (! [A,B,C] :( C = k2_xboole_0(A,B)<=> (! [D] :( r2_hidden(D,C)<=> ( r2_hidden(D,A)| r2_hidden(D,B) ) ) )) )),
% 34.43/7.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 34.43/7.24 fof(f32,axiom,(
% 34.43/7.24 (! [A,B,C] :( C = k4_xboole_0(A,B)<=> (! [D] :( r2_hidden(D,C)<=> ( r2_hidden(D,A)& ~ r2_hidden(D,B) ) ) )) )),
% 34.43/7.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 34.43/7.24 fof(f62,axiom,(
% 34.43/7.24 (! [A] : k2_xboole_0(A,k1_xboole_0) = A )),
% 34.43/7.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 34.43/7.24 fof(f369,axiom,(
% 34.43/7.24 (! [A,B,C] :~ ( k1_tarski(A) = k2_xboole_0(B,C)& B != C& B != k1_xboole_0& C != k1_xboole_0 ) )),
% 34.43/7.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 34.43/7.24 fof(f390,axiom,(
% 34.43/7.24 (! [A,B] :( k4_xboole_0(A,k1_tarski(B)) = A<=> ~ r2_hidden(B,A) ) )),
% 34.43/7.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 34.43/7.24 fof(f391,axiom,(
% 34.43/7.24 (! [A,B] :~ ( k4_xboole_0(A,k1_tarski(B)) = k1_xboole_0& A != k1_xboole_0& A != k1_tarski(B) ) )),
% 34.43/7.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 34.43/7.24 fof(f2809,axiom,(
% 34.43/7.24 (! [A,B,C] :( r2_hidden(A,k2_xboole_0(B,k1_tarski(C)))<=> ( r2_hidden(A,B)| A = C ) ) )),
% 34.43/7.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 34.43/7.24 fof(f19023,conjecture,(
% 34.43/7.24 (! [A,B,C,D] :~ ( r2_hidden(A,k2_xboole_0(C,D))& r2_hidden(B,k2_xboole_0(C,D))& ~ ( r2_hidden(A,k4_xboole_0(C,D))& r2_hidden(B,k4_xboole_0(C,D)) )& ~ ( r2_hidden(A,D)& r2_hidden(B,D) )& ~ ( r2_hidden(A,k4_xboole_0(C,D))& r2_hidden(B,D) )& ~ ( r2_hidden(A,D)& r2_hidden(B,k4_xboole_0(C,D)) ) ) )),
% 34.43/7.24 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 34.43/7.24 fof(f19024,negated_conjecture,(
% 34.43/7.24 ~((! [A,B,C,D] :~ ( r2_hidden(A,k2_xboole_0(C,D))& r2_hidden(B,k2_xboole_0(C,D))& ~ ( r2_hidden(A,k4_xboole_0(C,D))& r2_hidden(B,k4_xboole_0(C,D)) )& ~ ( r2_hidden(A,D)& r2_hidden(B,D) )& ~ ( r2_hidden(A,k4_xboole_0(C,D))& r2_hidden(B,D) )& ~ ( r2_hidden(A,D)& r2_hidden(B,k4_xboole_0(C,D)) ) ) ))),
% 34.43/7.24 inference(negated_conjecture,[status(cth)],[f19023])).
% 34.43/7.24 fof(f19032,plain,(
% 34.43/7.24 ![A,B]: ((~B=k1_tarski(A)|(![C]: ((~r2_hidden(C,B)|C=A)&(r2_hidden(C,B)|~C=A))))&(B=k1_tarski(A)|(?[C]: ((~r2_hidden(C,B)|~C=A)&(r2_hidden(C,B)|C=A)))))),
% 34.43/7.24 inference(NNF_transformation,[status(thm)],[f4])).
% 34.43/7.24 fof(f19033,plain,(
% 34.43/7.24 (![A,B]: (~B=k1_tarski(A)|((![C]: (~r2_hidden(C,B)|C=A))&(![C]: (r2_hidden(C,B)|~C=A)))))&(![A,B]: (B=k1_tarski(A)|(?[C]: ((~r2_hidden(C,B)|~C=A)&(r2_hidden(C,B)|C=A)))))),
% 34.43/7.24 inference(miniscoping,[status(thm)],[f19032])).
% 34.43/7.24 fof(f19034,plain,(
% 34.43/7.24 (![A,B]: (~B=k1_tarski(A)|((![C]: (~r2_hidden(C,B)|C=A))&(![C]: (r2_hidden(C,B)|~C=A)))))&(![A,B]: (B=k1_tarski(A)|((~r2_hidden(sK1_skl(B,A),B)|~sK1_skl(B,A)=A)&(r2_hidden(sK1_skl(B,A),B)|sK1_skl(B,A)=A))))),
% 34.43/7.24 inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl]),skolemize(C,sK1_skl(B,A))],[f19033])).
% 34.43/7.24 fof(f19037,plain,(
% 34.43/7.24 ![X0,X1]: (X0=k1_tarski(X1)|~r2_hidden(sK1_skl(X0,X1),X0)|~sK1_skl(X0,X1)=X1)),
% 34.43/7.24 inference(cnf_transformation,[status(thm)],[f19034])).
% 34.43/7.24 fof(f19119,plain,(
% 34.43/7.24 ![A,B,C]: ((~C=k2_xboole_0(A,B)|(![D]: ((~r2_hidden(D,C)|(r2_hidden(D,A)|r2_hidden(D,B)))&(r2_hidden(D,C)|(~r2_hidden(D,A)&~r2_hidden(D,B))))))&(C=k2_xboole_0(A,B)|(?[D]: ((~r2_hidden(D,C)|(~r2_hidden(D,A)&~r2_hidden(D,B)))&(r2_hidden(D,C)|(r2_hidden(D,A)|r2_hidden(D,B)))))))),
% 34.43/7.24 inference(NNF_transformation,[status(thm)],[f30])).
% 34.43/7.24 fof(f19120,plain,(
% 34.43/7.24 (![A,B,C]: (~C=k2_xboole_0(A,B)|((![D]: (~r2_hidden(D,C)|(r2_hidden(D,A)|r2_hidden(D,B))))&(![D]: (r2_hidden(D,C)|(~r2_hidden(D,A)&~r2_hidden(D,B)))))))&(![A,B,C]: (C=k2_xboole_0(A,B)|(?[D]: ((~r2_hidden(D,C)|(~r2_hidden(D,A)&~r2_hidden(D,B)))&(r2_hidden(D,C)|(r2_hidden(D,A)|r2_hidden(D,B)))))))),
% 34.43/7.24 inference(miniscoping,[status(thm)],[f19119])).
% 34.43/7.24 fof(f19121,plain,(
% 34.43/7.24 (![A,B,C]: (~C=k2_xboole_0(A,B)|((![D]: (~r2_hidden(D,C)|(r2_hidden(D,A)|r2_hidden(D,B))))&(![D]: (r2_hidden(D,C)|(~r2_hidden(D,A)&~r2_hidden(D,B)))))))&(![A,B,C]: (C=k2_xboole_0(A,B)|((~r2_hidden(sK23_skl(C,B,A),C)|(~r2_hidden(sK23_skl(C,B,A),A)&~r2_hidden(sK23_skl(C,B,A),B)))&(r2_hidden(sK23_skl(C,B,A),C)|(r2_hidden(sK23_skl(C,B,A),A)|r2_hidden(sK23_skl(C,B,A),B))))))),
% 34.43/7.24 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(D,sK23_skl(C,B,A))],[f19120])).
% 34.43/7.24 fof(f19122,plain,(
% 34.43/7.24 ![X0,X1,X2,X3]: (~X0=k2_xboole_0(X1,X2)|~r2_hidden(X3,X0)|r2_hidden(X3,X1)|r2_hidden(X3,X2))),
% 34.43/7.24 inference(cnf_transformation,[status(thm)],[f19121])).
% 34.43/7.24 fof(f19123,plain,(
% 34.43/7.24 ![X0,X1,X2,X3]: (~X0=k2_xboole_0(X1,X2)|r2_hidden(X3,X0)|~r2_hidden(X3,X1))),
% 34.43/7.24 inference(cnf_transformation,[status(thm)],[f19121])).
% 34.43/7.24 fof(f19137,plain,(
% 34.43/7.24 ![A,B,C]: ((~C=k4_xboole_0(A,B)|(![D]: ((~r2_hidden(D,C)|(r2_hidden(D,A)&~r2_hidden(D,B)))&(r2_hidden(D,C)|(~r2_hidden(D,A)|r2_hidden(D,B))))))&(C=k4_xboole_0(A,B)|(?[D]: ((~r2_hidden(D,C)|(~r2_hidden(D,A)|r2_hidden(D,B)))&(r2_hidden(D,C)|(r2_hidden(D,A)&~r2_hidden(D,B)))))))),
% 34.43/7.24 inference(NNF_transformation,[status(thm)],[f32])).
% 34.43/7.24 fof(f19138,plain,(
% 34.43/7.24 (![A,B,C]: (~C=k4_xboole_0(A,B)|((![D]: (~r2_hidden(D,C)|(r2_hidden(D,A)&~r2_hidden(D,B))))&(![D]: (r2_hidden(D,C)|(~r2_hidden(D,A)|r2_hidden(D,B)))))))&(![A,B,C]: (C=k4_xboole_0(A,B)|(?[D]: ((~r2_hidden(D,C)|(~r2_hidden(D,A)|r2_hidden(D,B)))&(r2_hidden(D,C)|(r2_hidden(D,A)&~r2_hidden(D,B)))))))),
% 34.43/7.24 inference(miniscoping,[status(thm)],[f19137])).
% 34.43/7.24 fof(f19139,plain,(
% 34.43/7.24 (![A,B,C]: (~C=k4_xboole_0(A,B)|((![D]: (~r2_hidden(D,C)|(r2_hidden(D,A)&~r2_hidden(D,B))))&(![D]: (r2_hidden(D,C)|(~r2_hidden(D,A)|r2_hidden(D,B)))))))&(![A,B,C]: (C=k4_xboole_0(A,B)|((~r2_hidden(sK25_skl(C,B,A),C)|(~r2_hidden(sK25_skl(C,B,A),A)|r2_hidden(sK25_skl(C,B,A),B)))&(r2_hidden(sK25_skl(C,B,A),C)|(r2_hidden(sK25_skl(C,B,A),A)&~r2_hidden(sK25_skl(C,B,A),B))))))),
% 34.43/7.24 inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl]),skolemize(D,sK25_skl(C,B,A))],[f19138])).
% 34.43/7.24 fof(f19142,plain,(
% 34.43/7.24 ![X0,X1,X2,X3]: (~X0=k4_xboole_0(X1,X2)|r2_hidden(X3,X0)|~r2_hidden(X3,X1)|r2_hidden(X3,X2))),
% 34.43/7.24 inference(cnf_transformation,[status(thm)],[f19139])).
% 34.43/7.24 fof(f19237,plain,(
% 34.43/7.24 ![X0]: (k2_xboole_0(X0,k1_xboole_0)=X0)),
% 34.43/7.24 inference(cnf_transformation,[status(thm)],[f62])).
% 34.43/7.24 fof(f19735,plain,(
% 34.43/7.24 ![A,B,C]: (((~k1_tarski(A)=k2_xboole_0(B,C)|B=C)|B=k1_xboole_0)|C=k1_xboole_0)),
% 34.43/7.24 inference(pre_NNF_transformation,[status(thm)],[f369])).
% 34.43/7.24 fof(f19736,plain,(
% 34.43/7.24 ![C]: ((![B]: (((![A]: ~k1_tarski(A)=k2_xboole_0(B,C))|B=C)|B=k1_xboole_0))|C=k1_xboole_0)),
% 34.43/7.24 inference(miniscoping,[status(thm)],[f19735])).
% 34.43/7.24 fof(f19737,plain,(
% 34.43/7.24 ![X0,X1,X2]: (~k1_tarski(X0)=k2_xboole_0(X1,X2)|X1=X2|X1=k1_xboole_0|X2=k1_xboole_0)),
% 34.43/7.24 inference(cnf_transformation,[status(thm)],[f19736])).
% 34.43/7.24 fof(f19780,plain,(
% 34.43/7.24 ![A,B]: ((~k4_xboole_0(A,k1_tarski(B))=A|~r2_hidden(B,A))&(k4_xboole_0(A,k1_tarski(B))=A|r2_hidden(B,A)))),
% 34.43/7.24 inference(NNF_transformation,[status(thm)],[f390])).
% 34.43/7.24 fof(f19781,plain,(
% 34.43/7.24 (![A,B]: (~k4_xboole_0(A,k1_tarski(B))=A|~r2_hidden(B,A)))&(![A,B]: (k4_xboole_0(A,k1_tarski(B))=A|r2_hidden(B,A)))),
% 34.43/7.24 inference(miniscoping,[status(thm)],[f19780])).
% 34.43/7.24 fof(f19783,plain,(
% 34.43/7.24 ![X0,X1]: (k4_xboole_0(X0,k1_tarski(X1))=X0|r2_hidden(X1,X0))),
% 34.43/7.24 inference(cnf_transformation,[status(thm)],[f19781])).
% 34.43/7.24 fof(f19784,plain,(
% 34.43/7.24 ![A,B]: ((~k4_xboole_0(A,k1_tarski(B))=k1_xboole_0|A=k1_xboole_0)|A=k1_tarski(B))),
% 34.43/7.24 inference(pre_NNF_transformation,[status(thm)],[f391])).
% 34.43/7.24 fof(f19785,plain,(
% 34.43/7.24 ![X0,X1]: (~k4_xboole_0(X0,k1_tarski(X1))=k1_xboole_0|X0=k1_xboole_0|X0=k1_tarski(X1))),
% 34.43/7.24 inference(cnf_transformation,[status(thm)],[f19784])).
% 34.43/7.24 fof(f27030,plain,(
% 34.43/7.24 ![A,B,C]: ((~r2_hidden(A,k2_xboole_0(B,k1_tarski(C)))|(r2_hidden(A,B)|A=C))&(r2_hidden(A,k2_xboole_0(B,k1_tarski(C)))|(~r2_hidden(A,B)&~A=C)))),
% 34.43/7.24 inference(NNF_transformation,[status(thm)],[f2809])).
% 34.43/7.24 fof(f27031,plain,(
% 34.43/7.24 (![A,B,C]: (~r2_hidden(A,k2_xboole_0(B,k1_tarski(C)))|(r2_hidden(A,B)|A=C)))&(![A,B,C]: (r2_hidden(A,k2_xboole_0(B,k1_tarski(C)))|(~r2_hidden(A,B)&~A=C)))),
% 34.43/7.24 inference(miniscoping,[status(thm)],[f27030])).
% 34.43/7.24 fof(f27032,plain,(
% 34.43/7.24 ![X0,X1,X2]: (~r2_hidden(X0,k2_xboole_0(X1,k1_tarski(X2)))|r2_hidden(X0,X1)|X0=X2)),
% 34.43/7.24 inference(cnf_transformation,[status(thm)],[f27031])).
% 34.43/7.24 fof(f89010,plain,(
% 34.43/7.24 (?[A,B,C,D]: (((((r2_hidden(A,k2_xboole_0(C,D))&r2_hidden(B,k2_xboole_0(C,D)))&(~r2_hidden(A,k4_xboole_0(C,D))|~r2_hidden(B,k4_xboole_0(C,D))))&(~r2_hidden(A,D)|~r2_hidden(B,D)))&(~r2_hidden(A,k4_xboole_0(C,D))|~r2_hidden(B,D)))&(~r2_hidden(A,D)|~r2_hidden(B,k4_xboole_0(C,D)))))),
% 34.43/7.24 inference(pre_NNF_transformation,[status(thm)],[f19024])).
% 34.43/7.24 fof(f89011,plain,(
% 34.43/7.24 (((((r2_hidden(sK6517_skl,k2_xboole_0(sK6519_skl,sK6520_skl))&r2_hidden(sK6518_skl,k2_xboole_0(sK6519_skl,sK6520_skl)))&(~r2_hidden(sK6517_skl,k4_xboole_0(sK6519_skl,sK6520_skl))|~r2_hidden(sK6518_skl,k4_xboole_0(sK6519_skl,sK6520_skl))))&(~r2_hidden(sK6517_skl,sK6520_skl)|~r2_hidden(sK6518_skl,sK6520_skl)))&(~r2_hidden(sK6517_skl,k4_xboole_0(sK6519_skl,sK6520_skl))|~r2_hidden(sK6518_skl,sK6520_skl)))&(~r2_hidden(sK6517_skl,sK6520_skl)|~r2_hidden(sK6518_skl,k4_xboole_0(sK6519_skl,sK6520_skl))))),
% 34.43/7.24 inference(skolemize,[status(esa),new_symbols(skolem,[sK6517_skl,sK6518_skl,sK6519_skl,sK6520_skl]),skolemize(A,sK6517_skl),skolemize(B,sK6518_skl),skolemize(C,sK6519_skl),skolemize(D,sK6520_skl)],[f89010])).
% 34.43/7.24 fof(f89012,plain,(
% 34.43/7.24 r2_hidden(sK6517_skl,k2_xboole_0(sK6519_skl,sK6520_skl))),
% 34.43/7.24 inference(cnf_transformation,[status(thm)],[f89011])).
% 34.43/7.24 fof(f89013,plain,(
% 34.43/7.24 r2_hidden(sK6518_skl,k2_xboole_0(sK6519_skl,sK6520_skl))),
% 34.43/7.24 inference(cnf_transformation,[status(thm)],[f89011])).
% 34.43/7.24 fof(f89014,plain,(
% 34.43/7.24 ~r2_hidden(sK6517_skl,k4_xboole_0(sK6519_skl,sK6520_skl))|~r2_hidden(sK6518_skl,k4_xboole_0(sK6519_skl,sK6520_skl))),
% 34.43/7.24 inference(cnf_transformation,[status(thm)],[f89011])).
% 34.43/7.24 fof(f89015,plain,(
% 34.43/7.24 ~r2_hidden(sK6517_skl,sK6520_skl)|~r2_hidden(sK6518_skl,sK6520_skl)),
% 34.43/7.24 inference(cnf_transformation,[status(thm)],[f89011])).
% 34.43/7.24 fof(f89016,plain,(
% 34.43/7.24 ~r2_hidden(sK6517_skl,k4_xboole_0(sK6519_skl,sK6520_skl))|~r2_hidden(sK6518_skl,sK6520_skl)),
% 34.43/7.24 inference(cnf_transformation,[status(thm)],[f89011])).
% 34.43/7.24 fof(f89017,plain,(
% 34.43/7.24 ~r2_hidden(sK6517_skl,sK6520_skl)|~r2_hidden(sK6518_skl,k4_xboole_0(sK6519_skl,sK6520_skl))),
% 34.43/7.24 inference(cnf_transformation,[status(thm)],[f89011])).
% 34.43/7.25 fof(f101019,definition,(
% 34.43/7.25 sQ1443_spl <=> (r2_hidden(sK6517_skl,k4_xboole_0(sK6519_skl,sK6520_skl)))),
% 34.43/7.25 introduced(definition,[new_symbols(definition,[sQ1443_spl])],[split_symbol_definition])).
% 34.43/7.25 fof(f101021,plain,(
% 34.43/7.25 ~r2_hidden(sK6517_skl,k4_xboole_0(sK6519_skl,sK6520_skl))|sQ1443_spl),
% 34.43/7.25 inference(component_clause,[status(thm)],[f101019])).
% 34.43/7.25 fof(f101022,definition,(
% 34.43/7.25 sQ1444_spl <=> (r2_hidden(sK6518_skl,k4_xboole_0(sK6519_skl,sK6520_skl)))),
% 34.43/7.25 introduced(definition,[new_symbols(definition,[sQ1444_spl])],[split_symbol_definition])).
% 34.43/7.25 fof(f101024,plain,(
% 34.43/7.25 ~r2_hidden(sK6518_skl,k4_xboole_0(sK6519_skl,sK6520_skl))|sQ1444_spl),
% 34.43/7.25 inference(component_clause,[status(thm)],[f101022])).
% 34.43/7.25 fof(f101025,plain,(
% 34.43/7.25 ~sQ1443_spl|~sQ1444_spl),
% 34.43/7.25 inference(split_clause,[status(thm)],[f89014,f101019,f101022])).
% 34.43/7.25 fof(f101026,definition,(
% 34.43/7.25 sQ1445_spl <=> (r2_hidden(sK6517_skl,sK6520_skl))),
% 34.43/7.25 introduced(definition,[new_symbols(definition,[sQ1445_spl])],[split_symbol_definition])).
% 34.43/7.25 fof(f101029,definition,(
% 34.43/7.25 sQ1446_spl <=> (r2_hidden(sK6518_skl,sK6520_skl))),
% 34.43/7.25 introduced(definition,[new_symbols(definition,[sQ1446_spl])],[split_symbol_definition])).
% 34.43/7.25 fof(f101032,plain,(
% 34.43/7.25 ~sQ1445_spl|~sQ1446_spl),
% 34.43/7.25 inference(split_clause,[status(thm)],[f89015,f101026,f101029])).
% 34.43/7.25 fof(f101033,plain,(
% 34.43/7.25 ~sQ1443_spl|~sQ1446_spl),
% 34.43/7.25 inference(split_clause,[status(thm)],[f89016,f101019,f101029])).
% 34.43/7.25 fof(f101034,plain,(
% 34.43/7.25 ~sQ1445_spl|~sQ1444_spl),
% 34.43/7.25 inference(split_clause,[status(thm)],[f89017,f101026,f101022])).
% 34.43/7.25 fof(f105550,plain,(
% 34.43/7.25 ![X0,X1,X2]: (~r2_hidden(X0,k2_xboole_0(X1,X2))|r2_hidden(X0,X1)|r2_hidden(X0,X2))),
% 34.43/7.25 inference(destructive_equality_resolution,[status(thm)],[f19122])).
% 34.43/7.25 fof(f105551,plain,(
% 34.43/7.25 ![X0,X1,X2]: (r2_hidden(X0,k2_xboole_0(X1,X2))|~r2_hidden(X0,X1))),
% 34.43/7.25 inference(destructive_equality_resolution,[status(thm)],[f19123])).
% 34.43/7.25 fof(f105558,plain,(
% 34.43/7.25 ![X0,X1,X2]: (r2_hidden(X0,k4_xboole_0(X1,X2))|~r2_hidden(X0,X1)|r2_hidden(X0,X2))),
% 34.43/7.25 inference(destructive_equality_resolution,[status(thm)],[f19142])).
% 34.43/7.25 fof(f110433,plain,(
% 34.43/7.25 ![X0,X1]: (k4_xboole_0(X0,k1_tarski(sK1_skl(X0,X1)))=X0|X0=k1_tarski(X1)|~sK1_skl(X0,X1)=X1)),
% 34.43/7.25 inference(resolution,[status(thm)],[f19783,f19037])).
% 34.43/7.25 fof(f110457,plain,(
% 34.43/7.25 r2_hidden(sK6518_skl,sK6519_skl)|r2_hidden(sK6518_skl,sK6520_skl)),
% 34.43/7.25 inference(resolution,[status(thm)],[f105550,f89013])).
% 34.43/7.25 fof(f110458,plain,(
% 34.43/7.25 r2_hidden(sK6517_skl,sK6519_skl)|r2_hidden(sK6517_skl,sK6520_skl)),
% 34.43/7.25 inference(resolution,[status(thm)],[f105550,f89012])).
% 34.43/7.25 fof(f110464,definition,(
% 34.43/7.25 sQ2483_spl <=> (r2_hidden(sK6518_skl,sK6519_skl))),
% 34.43/7.25 introduced(definition,[new_symbols(definition,[sQ2483_spl])],[split_symbol_definition])).
% 34.43/7.25 fof(f110467,plain,(
% 34.43/7.25 sQ2483_spl|sQ1446_spl),
% 34.43/7.25 inference(split_clause,[status(thm)],[f110457,f110464,f101029])).
% 34.43/7.25 fof(f110468,definition,(
% 34.43/7.25 sQ2484_spl <=> (r2_hidden(sK6517_skl,sK6519_skl))),
% 34.43/7.25 introduced(definition,[new_symbols(definition,[sQ2484_spl])],[split_symbol_definition])).
% 34.43/7.25 fof(f110471,plain,(
% 34.43/7.25 sQ2484_spl|sQ1445_spl),
% 34.43/7.25 inference(split_clause,[status(thm)],[f110458,f110468,f101026])).
% 34.43/7.25 fof(f110483,plain,(
% 34.43/7.25 ![X0]: (r2_hidden(sK6518_skl,k4_xboole_0(k2_xboole_0(sK6519_skl,sK6520_skl),X0))|r2_hidden(sK6518_skl,X0))),
% 34.43/7.25 inference(resolution,[status(thm)],[f105558,f89013])).
% 34.43/7.25 fof(f110484,plain,(
% 34.43/7.25 ![X0]: (r2_hidden(sK6517_skl,k4_xboole_0(k2_xboole_0(sK6519_skl,sK6520_skl),X0))|r2_hidden(sK6517_skl,X0))),
% 34.43/7.25 inference(resolution,[status(thm)],[f105558,f89012])).
% 34.43/7.25 fof(f110494,plain,(
% 34.43/7.25 ![X0,X1]: (r2_hidden(sK6518_skl,X0)|r2_hidden(sK6518_skl,k2_xboole_0(k4_xboole_0(k2_xboole_0(sK6519_skl,sK6520_skl),X0),X1)))),
% 34.43/7.25 inference(resolution,[status(thm)],[f110483,f105551])).
% 34.43/7.25 fof(f110498,plain,(
% 34.43/7.25 ![X0,X1]: (r2_hidden(sK6517_skl,X0)|r2_hidden(sK6517_skl,k2_xboole_0(k4_xboole_0(k2_xboole_0(sK6519_skl,sK6520_skl),X0),X1)))),
% 34.43/7.25 inference(resolution,[status(thm)],[f110484,f105551])).
% 34.43/7.25 fof(f110505,plain,(
% 34.43/7.25 ![X0,X1]: (r2_hidden(sK6518_skl,X0)|r2_hidden(sK6518_skl,k4_xboole_0(k2_xboole_0(sK6519_skl,sK6520_skl),X0))|r2_hidden(sK6518_skl,X1))),
% 34.43/7.25 inference(resolution,[status(thm)],[f110494,f105550])).
% 34.43/7.25 fof(f110512,definition,(
% 34.43/7.25 ![X0]: (sQ2485_spl <=> (r2_hidden(sK6518_skl,X0)|r2_hidden(sK6518_skl,k4_xboole_0(k2_xboole_0(sK6519_skl,sK6520_skl),X0))))),
% 34.43/7.25 introduced(definition,[new_symbols(definition,[sQ2485_spl])],[split_symbol_definition])).
% 34.43/7.25 fof(f110515,definition,(
% 34.43/7.25 ![X1]: (sQ2486_spl <=> (r2_hidden(sK6518_skl,X1)))),
% 34.43/7.25 introduced(definition,[new_symbols(definition,[sQ2486_spl])],[split_symbol_definition])).
% 34.43/7.25 fof(f110518,plain,(
% 34.43/7.25 sQ2485_spl|sQ2486_spl),
% 34.43/7.25 inference(split_clause,[status(thm)],[f110505,f110512,f110515])).
% 34.43/7.25 fof(f110523,plain,(
% 34.43/7.25 ![X0,X1]: (r2_hidden(sK6517_skl,X0)|r2_hidden(sK6517_skl,k4_xboole_0(k2_xboole_0(sK6519_skl,sK6520_skl),X0))|r2_hidden(sK6517_skl,X1))),
% 34.43/7.25 inference(resolution,[status(thm)],[f110498,f105550])).
% 34.43/7.25 fof(f110530,definition,(
% 34.43/7.25 ![X0]: (sQ2487_spl <=> (r2_hidden(sK6517_skl,X0)|r2_hidden(sK6517_skl,k4_xboole_0(k2_xboole_0(sK6519_skl,sK6520_skl),X0))))),
% 34.43/7.25 introduced(definition,[new_symbols(definition,[sQ2487_spl])],[split_symbol_definition])).
% 34.43/7.25 fof(f110533,definition,(
% 34.43/7.25 ![X1]: (sQ2488_spl <=> (r2_hidden(sK6517_skl,X1)))),
% 34.43/7.25 introduced(definition,[new_symbols(definition,[sQ2488_spl])],[split_symbol_definition])).
% 34.43/7.25 fof(f110536,plain,(
% 34.43/7.25 sQ2487_spl|sQ2488_spl),
% 34.43/7.25 inference(split_clause,[status(thm)],[f110523,f110530,f110533])).
% 34.43/7.25 fof(f110564,plain,(
% 34.43/7.25 ![X0]: (k1_tarski(X0)=k1_xboole_0|k1_tarski(X0)=k1_xboole_0|k1_xboole_0=k1_xboole_0)),
% 34.43/7.25 inference(resolution,[status(thm)],[f19737,f19237])).
% 34.43/7.25 fof(f110566,plain,(
% 34.43/7.25 ![X0,X1]: (~k1_tarski(X0)=X1|X1=k1_xboole_0|X1=k1_xboole_0|k1_xboole_0=k1_xboole_0)),
% 34.43/7.25 inference(paramodulation,[status(thm)],[f19237,f19737])).
% 34.43/7.25 fof(f110568,definition,(
% 34.43/7.25 ![X0]: (sQ2489_spl <=> (k1_tarski(X0)=k1_xboole_0|k1_tarski(X0)=k1_xboole_0))),
% 34.43/7.25 introduced(definition,[new_symbols(definition,[sQ2489_spl])],[split_symbol_definition])).
% 34.43/7.25 fof(f110571,definition,(
% 34.43/7.25 sQ2490_spl <=> (k1_xboole_0=k1_xboole_0)),
% 34.43/7.25 introduced(definition,[new_symbols(definition,[sQ2490_spl])],[split_symbol_definition])).
% 34.43/7.25 fof(f110574,plain,(
% 34.43/7.25 sQ2489_spl|sQ2490_spl),
% 34.43/7.25 inference(split_clause,[status(thm)],[f110564,f110568,f110571])).
% 18.24/7.76 fof(f110575,definition,(
% 18.24/7.76 ![X0,X1]: (sQ2491_spl <=> (~k1_tarski(X0)=X1|X1=k1_xboole_0|X1=k1_xboole_0))),
% 18.24/7.76 introduced(definition,[new_symbols(definition,[sQ2491_spl])],[split_symbol_definition])).
% 18.24/7.76 fof(f110578,plain,(
% 18.24/7.76 sQ2491_spl|sQ2490_spl),
% 18.24/7.76 inference(split_clause,[status(thm)],[f110566,f110575,f110571])).
% 18.24/7.76 fof(f110656,plain,(
% 18.24/7.76 ![X0,X1]: (r2_hidden(sK6518_skl,k4_xboole_0(k2_xboole_0(sK6519_skl,sK6520_skl),X0))|sK6518_skl=X1|r2_hidden(sK6518_skl,X0))),
% 18.24/7.76 inference(resolution,[status(thm)],[f27032,f110494])).
% 18.24/7.76 fof(f110657,plain,(
% 18.24/7.76 ![X0,X1]: (r2_hidden(sK6517_skl,k4_xboole_0(k2_xboole_0(sK6519_skl,sK6520_skl),X0))|sK6517_skl=X1|r2_hidden(sK6517_skl,X0))),
% 18.24/7.76 inference(resolution,[status(thm)],[f27032,f110498])).
% 18.24/7.76 fof(f110664,definition,(
% 18.24/7.76 ![X1]: (sQ2492_spl <=> (sK6518_skl=X1))),
% 18.24/7.76 introduced(definition,[new_symbols(definition,[sQ2492_spl])],[split_symbol_definition])).
% 18.24/7.76 fof(f110667,plain,(
% 18.24/7.76 sQ2485_spl|sQ2492_spl),
% 18.24/7.76 inference(split_clause,[status(thm)],[f110656,f110512,f110664])).
% 18.24/7.76 fof(f110668,definition,(
% 18.24/7.76 ![X1]: (sQ2493_spl <=> (sK6517_skl=X1))),
% 18.24/7.76 introduced(definition,[new_symbols(definition,[sQ2493_spl])],[split_symbol_definition])).
% 18.24/7.76 fof(f110669,plain,(
% 18.24/7.76 ![X0]: (sK6517_skl=X0|~sQ2493_spl)),
% 18.24/7.76 inference(component_clause,[status(thm)],[f110668])).
% 18.24/7.76 fof(f110671,plain,(
% 18.24/7.76 sQ2487_spl|sQ2493_spl),
% 18.24/7.76 inference(split_clause,[status(thm)],[f110657,f110530,f110668])).
% 18.24/7.76 fof(f110672,plain,(
% 18.24/7.76 ![X0]: (k1_xboole_0=k1_tarski(X0)|~sK1_skl(k1_xboole_0,X0)=X0|k1_xboole_0=k1_xboole_0|k1_xboole_0=k1_tarski(sK1_skl(k1_xboole_0,X0)))),
% 18.24/7.76 inference(resolution,[status(thm)],[f110433,f19785])).
% 18.24/7.76 fof(f110675,definition,(
% 18.24/7.76 ![X0]: (sQ2494_spl <=> (k1_xboole_0=k1_tarski(X0)|~sK1_skl(k1_xboole_0,X0)=X0|k1_xboole_0=k1_tarski(sK1_skl(k1_xboole_0,X0))))),
% 18.24/7.76 introduced(definition,[new_symbols(definition,[sQ2494_spl])],[split_symbol_definition])).
% 18.24/7.76 fof(f110678,plain,(
% 18.24/7.76 sQ2494_spl|sQ2490_spl),
% 18.24/7.76 inference(split_clause,[status(thm)],[f110672,f110675,f110571])).
% 18.24/7.76 fof(f111668,plain,(
% 18.24/7.76 ~r2_hidden(sK6517_skl,sK6519_skl)|r2_hidden(sK6517_skl,sK6520_skl)|sQ1443_spl),
% 18.24/7.76 inference(resolution,[status(thm)],[f101021,f105558])).
% 18.24/7.76 fof(f111684,plain,(
% 18.24/7.76 ~sQ2484_spl|sQ1445_spl|sQ1443_spl),
% 18.24/7.76 inference(split_clause,[status(thm)],[f111668,f110468,f101026,f101019])).
% 18.24/7.76 fof(f111691,plain,(
% 18.24/7.76 ~r2_hidden(sK6518_skl,sK6519_skl)|r2_hidden(sK6518_skl,sK6520_skl)|sQ1444_spl),
% 18.24/7.76 inference(resolution,[status(thm)],[f101024,f105558])).
% 18.24/7.76 fof(f111703,plain,(
% 18.24/7.76 ~r2_hidden(sK6517_skl,k4_xboole_0(sK6519_skl,sK6520_skl))|sQ1444_spl|~sQ2493_spl),
% 18.24/7.76 inference(paramodulation,[status(thm)],[f110669,f101024])).
% 18.24/7.76 fof(f111707,plain,(
% 18.24/7.76 ~sQ2483_spl|sQ1446_spl|sQ1444_spl),
% 18.24/7.76 inference(split_clause,[status(thm)],[f111691,f110464,f101029,f101022])).
% 18.24/7.76 fof(f111714,plain,(
% 18.24/7.76 ~sQ1443_spl|sQ1444_spl|~sQ2493_spl),
% 18.24/7.76 inference(split_clause,[status(thm)],[f111703,f101019,f101022,f110668])).
% 18.24/7.76 fof(f111715,plain,(
% 18.24/7.76 $false),
% 18.24/7.76 inference(sat_refutation,[status(thm)],[f101025,f101032,f101033,f101034,f110467,f110471,f110518,f110536,f110574,f110578,f110667,f110671,f110678,f111684,f111707,f111714])).
% 18.24/7.76 % SZS output end CNFRefutation for theBenchmark.p
% 4.02/7.88 % Elapsed time: 7.398878 seconds
% 4.02/7.88 % CPU time: 36.126119 seconds
% 4.02/7.88 % Total memory used: 5.341 GB
% 4.02/7.88 % Net memory used: 5.296 GB
%------------------------------------------------------------------------------