%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU406+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 : n002.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 0.59s 1.14s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU406+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.10/0.36 % Computer : n002.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 06:23:49 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.55/0.81 % Drodi V4.1.1
% 0.59/1.14 % Refutation found
% 0.59/1.14 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.59/1.14 % SZS output start CNFRefutation for theBenchmark
% 0.59/1.14 fof(f26,axiom,(
% 0.59/1.14 (? [A] : ~ v1_xboole_0(A) )),
% 0.59/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.59/1.14 fof(f29,axiom,(
% 0.59/1.14 (! [A] :( A = k1_xboole_0<=> (! [B] : ~ r2_hidden(B,A) )) )),
% 0.59/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.59/1.14 fof(f30,axiom,(
% 0.59/1.14 (! [A,B,C] :( C = k2_xboole_0(A,B)<=> (! [D] :( r2_hidden(D,C)<=> ( r2_hidden(D,A)| r2_hidden(D,B) ) ) )) )),
% 0.59/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.59/1.14 fof(f32,axiom,(
% 0.59/1.14 (! [A,B,C] :( C = k4_xboole_0(A,B)<=> (! [D] :( r2_hidden(D,C)<=> ( r2_hidden(D,A)& ~ r2_hidden(D,B) ) ) )) )),
% 0.59/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.59/1.14 fof(f54,axiom,(
% 0.59/1.14 (! [A,B] : k2_xboole_0(A,B) = k2_xboole_0(B,A) )),
% 0.59/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.59/1.14 fof(f62,axiom,(
% 0.59/1.14 (! [A] : k2_xboole_0(A,k1_xboole_0) = A )),
% 0.59/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.59/1.14 fof(f64,axiom,(
% 0.59/1.14 (! [A] : k4_xboole_0(A,k1_xboole_0) = A )),
% 0.59/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.59/1.14 fof(f65,axiom,(
% 0.59/1.14 (! [A] : k4_xboole_0(k1_xboole_0,A) = k1_xboole_0 )),
% 0.59/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.59/1.14 fof(f76,axiom,(
% 0.59/1.14 (! [A,B] : r1_tarski(A,k2_xboole_0(A,B)) )),
% 0.59/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.59/1.14 fof(f84,axiom,(
% 0.59/1.14 (! [A,B] :( k2_xboole_0(A,B) = k1_xboole_0=> A = k1_xboole_0 ) )),
% 0.59/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.59/1.14 fof(f106,axiom,(
% 0.59/1.14 (! [A,B] :( k4_xboole_0(A,B) = k1_xboole_0<=> r1_tarski(A,B) ) )),
% 0.59/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.59/1.14 fof(f109,axiom,(
% 0.59/1.14 (! [A,B] : k4_xboole_0(k2_xboole_0(A,B),B) = k4_xboole_0(A,B) )),
% 0.59/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.59/1.14 fof(f421,axiom,(
% 0.59/1.14 (! [A,B] :( ( ~ v1_xboole_0(A)& ~ v1_xboole_0(B) )=> ~ r1_subset_1(A,A) ) )),
% 0.59/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.59/1.14 fof(f424,axiom,(
% 0.59/1.14 (! [A,B] :( ( ~ v1_xboole_0(A)& ~ v1_xboole_0(B) )=> ~ r2_subset_1(A,A) ) )),
% 0.59/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.59/1.14 fof(f4434,conjecture,(
% 0.59/1.14 (! [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)) ) ) )),
% 0.59/1.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.59/1.14 fof(f4435,negated_conjecture,(
% 0.59/1.14 ~((! [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)) ) ) ))),
% 0.59/1.14 inference(negated_conjecture,[status(cth)],[f4434])).
% 0.59/1.14 fof(f4517,plain,(
% 0.59/1.14 ~v1_xboole_0(sK21_skl)),
% 0.59/1.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl]),skolemize(A,sK21_skl)],[f26])).
% 0.59/1.14 fof(f4518,plain,(
% 0.59/1.14 ~v1_xboole_0(sK21_skl)),
% 0.59/1.14 inference(cnf_transformation,[status(thm)],[f4517])).
% 0.59/1.14 fof(f4525,plain,(
% 0.59/1.14 ![A]: ((~A=k1_xboole_0|(![B]: ~r2_hidden(B,A)))&(A=k1_xboole_0|(?[B]: r2_hidden(B,A))))),
% 0.59/1.14 inference(NNF_transformation,[status(thm)],[f29])).
% 0.59/1.14 fof(f4526,plain,(
% 0.59/1.14 (![A]: (~A=k1_xboole_0|(![B]: ~r2_hidden(B,A))))&(![A]: (A=k1_xboole_0|(?[B]: r2_hidden(B,A))))),
% 0.59/1.14 inference(miniscoping,[status(thm)],[f4525])).
% 0.59/1.14 fof(f4527,plain,(
% 0.59/1.14 (![A]: (~A=k1_xboole_0|(![B]: ~r2_hidden(B,A))))&(![A]: (A=k1_xboole_0|r2_hidden(sK22_skl(A),A)))),
% 0.59/1.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK22_skl]),skolemize(B,sK22_skl(A))],[f4526])).
% 0.59/1.14 fof(f4528,plain,(
% 0.59/1.14 ![X0,X1]: (~X0=k1_xboole_0|~r2_hidden(X1,X0))),
% 0.59/1.14 inference(cnf_transformation,[status(thm)],[f4527])).
% 0.59/1.14 fof(f4530,plain,(
% 0.59/1.14 ![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)))))))),
% 0.59/1.14 inference(NNF_transformation,[status(thm)],[f30])).
% 0.59/1.14 fof(f4531,plain,(
% 0.59/1.14 (![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)))))))),
% 0.59/1.14 inference(miniscoping,[status(thm)],[f4530])).
% 0.59/1.14 fof(f4532,plain,(
% 0.59/1.14 (![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))))))),
% 0.59/1.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(D,sK23_skl(C,B,A))],[f4531])).
% 0.59/1.14 fof(f4533,plain,(
% 0.59/1.14 ![X0,X1,X2,X3]: (~X0=k2_xboole_0(X1,X2)|~r2_hidden(X3,X0)|r2_hidden(X3,X1)|r2_hidden(X3,X2))),
% 0.59/1.14 inference(cnf_transformation,[status(thm)],[f4532])).
% 0.59/1.14 fof(f4535,plain,(
% 0.59/1.14 ![X0,X1,X2,X3]: (~X0=k2_xboole_0(X1,X2)|r2_hidden(X3,X0)|~r2_hidden(X3,X2))),
% 0.59/1.14 inference(cnf_transformation,[status(thm)],[f4532])).
% 0.59/1.14 fof(f4548,plain,(
% 0.59/1.14 ![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)))))))),
% 0.59/1.14 inference(NNF_transformation,[status(thm)],[f32])).
% 0.59/1.14 fof(f4549,plain,(
% 0.59/1.14 (![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)))))))),
% 0.59/1.14 inference(miniscoping,[status(thm)],[f4548])).
% 0.59/1.14 fof(f4550,plain,(
% 0.59/1.14 (![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))))))),
% 0.59/1.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl]),skolemize(D,sK25_skl(C,B,A))],[f4549])).
% 0.59/1.14 fof(f4553,plain,(
% 0.59/1.14 ![X0,X1,X2,X3]: (~X0=k4_xboole_0(X1,X2)|r2_hidden(X3,X0)|~r2_hidden(X3,X1)|r2_hidden(X3,X2))),
% 0.59/1.14 inference(cnf_transformation,[status(thm)],[f4550])).
% 0.59/1.14 fof(f4641,plain,(
% 0.59/1.14 ![X0,X1]: (k2_xboole_0(X0,X1)=k2_xboole_0(X1,X0))),
% 0.59/1.14 inference(cnf_transformation,[status(thm)],[f54])).
% 0.59/1.14 fof(f4648,plain,(
% 0.59/1.14 ![X0]: (k2_xboole_0(X0,k1_xboole_0)=X0)),
% 0.59/1.14 inference(cnf_transformation,[status(thm)],[f62])).
% 0.59/1.14 fof(f4650,plain,(
% 0.59/1.14 ![X0]: (k4_xboole_0(X0,k1_xboole_0)=X0)),
% 0.59/1.14 inference(cnf_transformation,[status(thm)],[f64])).
% 0.59/1.14 fof(f4651,plain,(
% 0.59/1.14 ![X0]: (k4_xboole_0(k1_xboole_0,X0)=k1_xboole_0)),
% 0.59/1.14 inference(cnf_transformation,[status(thm)],[f65])).
% 0.59/1.14 fof(f4670,plain,(
% 0.59/1.14 ![X0,X1]: (r1_tarski(X0,k2_xboole_0(X0,X1)))),
% 0.59/1.14 inference(cnf_transformation,[status(thm)],[f76])).
% 0.59/1.14 fof(f4691,plain,(
% 0.59/1.14 ![A,B]: (~k2_xboole_0(A,B)=k1_xboole_0|A=k1_xboole_0)),
% 0.59/1.14 inference(pre_NNF_transformation,[status(thm)],[f84])).
% 0.59/1.14 fof(f4692,plain,(
% 0.59/1.14 ![A]: ((![B]: ~k2_xboole_0(A,B)=k1_xboole_0)|A=k1_xboole_0)),
% 0.59/1.14 inference(miniscoping,[status(thm)],[f4691])).
% 0.59/1.14 fof(f4693,plain,(
% 0.59/1.14 ![X0,X1]: (~k2_xboole_0(X0,X1)=k1_xboole_0|X0=k1_xboole_0)),
% 0.59/1.14 inference(cnf_transformation,[status(thm)],[f4692])).
% 0.59/1.14 fof(f4734,plain,(
% 0.59/1.14 ![A,B]: ((~k4_xboole_0(A,B)=k1_xboole_0|r1_tarski(A,B))&(k4_xboole_0(A,B)=k1_xboole_0|~r1_tarski(A,B)))),
% 0.59/1.14 inference(NNF_transformation,[status(thm)],[f106])).
% 0.59/1.14 fof(f4735,plain,(
% 0.59/1.14 (![A,B]: (~k4_xboole_0(A,B)=k1_xboole_0|r1_tarski(A,B)))&(![A,B]: (k4_xboole_0(A,B)=k1_xboole_0|~r1_tarski(A,B)))),
% 0.59/1.14 inference(miniscoping,[status(thm)],[f4734])).
% 0.59/1.14 fof(f4736,plain,(
% 0.59/1.14 ![X0,X1]: (~k4_xboole_0(X0,X1)=k1_xboole_0|r1_tarski(X0,X1))),
% 0.59/1.14 inference(cnf_transformation,[status(thm)],[f4735])).
% 0.59/1.14 fof(f4737,plain,(
% 0.59/1.14 ![X0,X1]: (k4_xboole_0(X0,X1)=k1_xboole_0|~r1_tarski(X0,X1))),
% 0.59/1.14 inference(cnf_transformation,[status(thm)],[f4735])).
% 0.59/1.14 fof(f4742,plain,(
% 0.59/1.14 ![X0,X1]: (k4_xboole_0(k2_xboole_0(X0,X1),X1)=k4_xboole_0(X0,X1))),
% 0.59/1.14 inference(cnf_transformation,[status(thm)],[f109])).
% 0.59/1.14 fof(f5487,plain,(
% 0.59/1.14 ![A,B]: ((v1_xboole_0(A)|v1_xboole_0(B))|~r1_subset_1(A,A))),
% 0.59/1.14 inference(pre_NNF_transformation,[status(thm)],[f421])).
% 0.59/1.14 fof(f5488,plain,(
% 0.59/1.14 ![A]: ((v1_xboole_0(A)|(![B]: v1_xboole_0(B)))|~r1_subset_1(A,A))),
% 0.59/1.14 inference(miniscoping,[status(thm)],[f5487])).
% 0.59/1.14 fof(f5489,plain,(
% 0.59/1.14 ![X0,X1]: (v1_xboole_0(X0)|v1_xboole_0(X1)|~r1_subset_1(X0,X0))),
% 0.59/1.14 inference(cnf_transformation,[status(thm)],[f5488])).
% 0.59/1.14 fof(f5496,plain,(
% 0.59/1.14 ![A,B]: ((v1_xboole_0(A)|v1_xboole_0(B))|~r2_subset_1(A,A))),
% 0.59/1.14 inference(pre_NNF_transformation,[status(thm)],[f424])).
% 0.59/1.14 fof(f5497,plain,(
% 0.59/1.14 ![A]: ((v1_xboole_0(A)|(![B]: v1_xboole_0(B)))|~r2_subset_1(A,A))),
% 0.59/1.14 inference(miniscoping,[status(thm)],[f5496])).
% 0.59/1.14 fof(f5498,plain,(
% 0.59/1.14 ![X0,X1]: (v1_xboole_0(X0)|v1_xboole_0(X1)|~r2_subset_1(X0,X0))),
% 0.59/1.14 inference(cnf_transformation,[status(thm)],[f5497])).
% 0.59/1.14 fof(f18494,plain,(
% 0.59/1.14 (?[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)))))),
% 0.59/1.14 inference(pre_NNF_transformation,[status(thm)],[f4435])).
% 0.59/1.14 fof(f18495,plain,(
% 0.59/1.14 (((((r2_hidden(sK1189_skl,k2_xboole_0(sK1191_skl,sK1192_skl))&r2_hidden(sK1190_skl,k2_xboole_0(sK1191_skl,sK1192_skl)))&(~r2_hidden(sK1189_skl,k4_xboole_0(sK1191_skl,sK1192_skl))|~r2_hidden(sK1190_skl,k4_xboole_0(sK1191_skl,sK1192_skl))))&(~r2_hidden(sK1189_skl,sK1192_skl)|~r2_hidden(sK1190_skl,sK1192_skl)))&(~r2_hidden(sK1189_skl,k4_xboole_0(sK1191_skl,sK1192_skl))|~r2_hidden(sK1190_skl,sK1192_skl)))&(~r2_hidden(sK1189_skl,sK1192_skl)|~r2_hidden(sK1190_skl,k4_xboole_0(sK1191_skl,sK1192_skl))))),
% 0.59/1.14 inference(skolemize,[status(esa),new_symbols(skolem,[sK1189_skl,sK1190_skl,sK1191_skl,sK1192_skl]),skolemize(A,sK1189_skl),skolemize(B,sK1190_skl),skolemize(C,sK1191_skl),skolemize(D,sK1192_skl)],[f18494])).
% 0.59/1.14 fof(f18496,plain,(
% 0.59/1.14 r2_hidden(sK1189_skl,k2_xboole_0(sK1191_skl,sK1192_skl))),
% 0.59/1.14 inference(cnf_transformation,[status(thm)],[f18495])).
% 0.59/1.14 fof(f18497,plain,(
% 0.59/1.14 r2_hidden(sK1190_skl,k2_xboole_0(sK1191_skl,sK1192_skl))),
% 0.59/1.14 inference(cnf_transformation,[status(thm)],[f18495])).
% 0.59/1.14 fof(f18498,plain,(
% 0.59/1.14 ~r2_hidden(sK1189_skl,k4_xboole_0(sK1191_skl,sK1192_skl))|~r2_hidden(sK1190_skl,k4_xboole_0(sK1191_skl,sK1192_skl))),
% 0.59/1.14 inference(cnf_transformation,[status(thm)],[f18495])).
% 0.59/1.14 fof(f18499,plain,(
% 0.59/1.14 ~r2_hidden(sK1189_skl,sK1192_skl)|~r2_hidden(sK1190_skl,sK1192_skl)),
% 0.59/1.14 inference(cnf_transformation,[status(thm)],[f18495])).
% 0.59/1.14 fof(f18500,plain,(
% 0.59/1.14 ~r2_hidden(sK1189_skl,k4_xboole_0(sK1191_skl,sK1192_skl))|~r2_hidden(sK1190_skl,sK1192_skl)),
% 0.59/1.14 inference(cnf_transformation,[status(thm)],[f18495])).
% 0.59/1.14 fof(f18501,plain,(
% 0.59/1.14 ~r2_hidden(sK1189_skl,sK1192_skl)|~r2_hidden(sK1190_skl,k4_xboole_0(sK1191_skl,sK1192_skl))),
% 0.59/1.14 inference(cnf_transformation,[status(thm)],[f18495])).
% 0.59/1.14 fof(f19902,definition,(
% 0.59/1.14 ![X0]: (sQ13_spl <=> (v1_xboole_0(X0)|~r1_subset_1(X0,X0)))),
% 0.59/1.14 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.59/1.14 fof(f19905,definition,(
% 0.59/1.14 ![X1]: (sQ14_spl <=> (v1_xboole_0(X1)))),
% 0.59/1.14 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.59/1.14 fof(f19906,plain,(
% 0.59/1.14 ![X0]: (v1_xboole_0(X0)|~sQ14_spl)),
% 0.59/1.14 inference(component_clause,[status(thm)],[f19905])).
% 0.59/1.14 fof(f19908,plain,(
% 0.59/1.14 sQ13_spl|sQ14_spl),
% 0.59/1.14 inference(split_clause,[status(thm)],[f5489,f19902,f19905])).
% 0.59/1.14 fof(f19909,definition,(
% 0.59/1.14 ![X0]: (sQ15_spl <=> (v1_xboole_0(X0)|~r2_subset_1(X0,X0)))),
% 0.59/1.14 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.59/1.14 fof(f19912,plain,(
% 0.59/1.14 sQ15_spl|sQ14_spl),
% 0.59/1.14 inference(split_clause,[status(thm)],[f5498,f19909,f19905])).
% 0.59/1.14 fof(f21482,definition,(
% 0.59/1.14 sQ431_spl <=> (r2_hidden(sK1189_skl,k4_xboole_0(sK1191_skl,sK1192_skl)))),
% 0.59/1.14 introduced(definition,[new_symbols(definition,[sQ431_spl])],[split_symbol_definition])).
% 0.59/1.14 fof(f21484,plain,(
% 0.59/1.14 ~r2_hidden(sK1189_skl,k4_xboole_0(sK1191_skl,sK1192_skl))|sQ431_spl),
% 0.59/1.14 inference(component_clause,[status(thm)],[f21482])).
% 0.59/1.14 fof(f21485,definition,(
% 0.59/1.14 sQ432_spl <=> (r2_hidden(sK1190_skl,k4_xboole_0(sK1191_skl,sK1192_skl)))),
% 0.59/1.14 introduced(definition,[new_symbols(definition,[sQ432_spl])],[split_symbol_definition])).
% 0.59/1.14 fof(f21488,plain,(
% 0.59/1.14 ~sQ431_spl|~sQ432_spl),
% 0.59/1.14 inference(split_clause,[status(thm)],[f18498,f21482,f21485])).
% 0.59/1.14 fof(f21489,definition,(
% 0.59/1.14 sQ433_spl <=> (r2_hidden(sK1189_skl,sK1192_skl))),
% 0.59/1.14 introduced(definition,[new_symbols(definition,[sQ433_spl])],[split_symbol_definition])).
% 0.59/1.14 fof(f21492,definition,(
% 0.59/1.14 sQ434_spl <=> (r2_hidden(sK1190_skl,sK1192_skl))),
% 0.59/1.14 introduced(definition,[new_symbols(definition,[sQ434_spl])],[split_symbol_definition])).
% 0.59/1.14 fof(f21495,plain,(
% 0.59/1.14 ~sQ433_spl|~sQ434_spl),
% 0.59/1.14 inference(split_clause,[status(thm)],[f18499,f21489,f21492])).
% 0.59/1.14 fof(f21496,plain,(
% 0.59/1.14 ~sQ431_spl|~sQ434_spl),
% 0.59/1.14 inference(split_clause,[status(thm)],[f18500,f21482,f21492])).
% 0.59/1.14 fof(f21497,plain,(
% 0.59/1.14 ~sQ433_spl|~sQ432_spl),
% 0.59/1.14 inference(split_clause,[status(thm)],[f18501,f21489,f21485])).
% 0.59/1.14 fof(f22089,plain,(
% 0.59/1.14 ![X0]: (~r2_hidden(X0,k1_xboole_0))),
% 0.59/1.14 inference(destructive_equality_resolution,[status(thm)],[f4528])).
% 0.59/1.14 fof(f22090,plain,(
% 0.59/1.14 ![X0,X1,X2]: (~r2_hidden(X0,k2_xboole_0(X1,X2))|r2_hidden(X0,X1)|r2_hidden(X0,X2))),
% 0.59/1.14 inference(destructive_equality_resolution,[status(thm)],[f4533])).
% 0.59/1.14 fof(f22092,plain,(
% 0.59/1.14 ![X0,X1,X2]: (r2_hidden(X0,k2_xboole_0(X1,X2))|~r2_hidden(X0,X2))),
% 0.59/1.14 inference(destructive_equality_resolution,[status(thm)],[f4535])).
% 0.59/1.14 fof(f22098,plain,(
% 0.59/1.14 ![X0,X1,X2]: (r2_hidden(X0,k4_xboole_0(X1,X2))|~r2_hidden(X0,X1)|r2_hidden(X0,X2))),
% 0.59/1.14 inference(destructive_equality_resolution,[status(thm)],[f4553])).
% 0.59/1.14 fof(f23165,plain,(
% 0.59/1.14 ![X0]: (r2_hidden(sK1189_skl,k2_xboole_0(X0,k2_xboole_0(sK1191_skl,sK1192_skl))))),
% 0.59/1.14 inference(resolution,[status(thm)],[f22092,f18496])).
% 0.59/1.14 fof(f23207,plain,(
% 0.59/1.14 ![X0]: (r1_tarski(X0,X0))),
% 0.59/1.14 inference(paramodulation,[status(thm)],[f4648,f4670])).
% 0.59/1.14 fof(f23212,plain,(
% 0.59/1.14 ![X0]: (r2_hidden(sK1190_skl,k4_xboole_0(k2_xboole_0(sK1191_skl,sK1192_skl),X0))|r2_hidden(sK1190_skl,X0))),
% 0.59/1.14 inference(resolution,[status(thm)],[f22098,f18497])).
% 0.59/1.14 fof(f23218,plain,(
% 0.59/1.14 ![X0]: (r2_hidden(sK1189_skl,k4_xboole_0(k2_xboole_0(sK1191_skl,sK1192_skl),X0))|r2_hidden(sK1189_skl,X0))),
% 0.59/1.14 inference(resolution,[status(thm)],[f22098,f18496])).
% 0.59/1.14 fof(f23222,plain,(
% 0.59/1.14 ![X0]: (X0=k2_xboole_0(k1_xboole_0,X0))),
% 0.59/1.14 inference(paramodulation,[status(thm)],[f4648,f4641])).
% 0.59/1.14 fof(f23255,definition,(
% 0.59/1.14 ![X0]: (sQ584_spl <=> (r2_hidden(sK1189_skl,X0)))),
% 0.59/1.14 introduced(definition,[new_symbols(definition,[sQ584_spl])],[split_symbol_definition])).
% 0.59/1.14 fof(f23256,plain,(
% 0.59/1.14 ![X0]: (r2_hidden(sK1189_skl,X0)|~sQ584_spl)),
% 0.59/1.14 inference(component_clause,[status(thm)],[f23255])).
% 0.59/1.14 fof(f23399,plain,(
% 0.59/1.14 ![X0]: (r1_tarski(k1_xboole_0,X0))),
% 0.59/1.14 inference(paramodulation,[status(thm)],[f23222,f4670])).
% 0.59/1.14 fof(f23499,plain,(
% 0.59/1.14 $false|~sQ14_spl),
% 0.59/1.14 inference(forward_subsumption_resolution,[status(thm)],[f4518,f19906])).
% 0.59/1.14 fof(f23500,plain,(
% 0.59/1.14 ~sQ14_spl),
% 0.59/1.14 inference(contradiction_clause,[status(thm)],[f23499])).
% 0.59/1.14 fof(f23566,definition,(
% 0.59/1.14 sQ587_spl <=> (r2_hidden(sK1190_skl,k2_xboole_0(sK1191_skl,sK1192_skl)))),
% 0.59/1.14 introduced(definition,[new_symbols(definition,[sQ587_spl])],[split_symbol_definition])).
% 0.59/1.14 fof(f23628,plain,(
% 0.59/1.14 ![X0]: (~X0=k1_xboole_0|k1_xboole_0=k1_xboole_0)),
% 0.59/1.14 inference(paramodulation,[status(thm)],[f23222,f4693])).
% 0.59/1.14 fof(f23636,definition,(
% 0.59/1.14 ![X0]: (sQ588_spl <=> (~X0=k1_xboole_0))),
% 0.59/1.14 introduced(definition,[new_symbols(definition,[sQ588_spl])],[split_symbol_definition])).
% 0.59/1.14 fof(f23637,plain,(
% 0.59/1.14 ![X0]: (~X0=k1_xboole_0|~sQ588_spl)),
% 0.59/1.14 inference(component_clause,[status(thm)],[f23636])).
% 0.59/1.14 fof(f23639,definition,(
% 0.59/1.14 sQ589_spl <=> (k1_xboole_0=k1_xboole_0)),
% 0.59/1.14 introduced(definition,[new_symbols(definition,[sQ589_spl])],[split_symbol_definition])).
% 0.59/1.16 fof(f23642,plain,(
% 0.59/1.16 sQ588_spl|sQ589_spl),
% 0.59/1.16 inference(split_clause,[status(thm)],[f23628,f23636,f23639])).
% 0.59/1.16 fof(f23643,plain,(
% 0.59/1.16 $false|~sQ588_spl),
% 0.59/1.16 inference(destructive_equality_resolution,[status(thm)],[f23637])).
% 0.59/1.16 fof(f23644,plain,(
% 0.59/1.16 ~sQ588_spl),
% 0.59/1.16 inference(contradiction_clause,[status(thm)],[f23643])).
% 0.59/1.16 fof(f23691,plain,(
% 0.59/1.16 ![X0]: (r2_hidden(sK1189_skl,X0)|r2_hidden(sK1189_skl,k2_xboole_0(sK1191_skl,sK1192_skl)))),
% 0.59/1.16 inference(resolution,[status(thm)],[f23165,f22090])).
% 0.59/1.16 fof(f23705,definition,(
% 0.59/1.16 sQ590_spl <=> (r2_hidden(sK1189_skl,k2_xboole_0(sK1191_skl,sK1192_skl)))),
% 0.59/1.16 introduced(definition,[new_symbols(definition,[sQ590_spl])],[split_symbol_definition])).
% 0.59/1.16 fof(f23708,plain,(
% 0.59/1.16 sQ584_spl|sQ590_spl),
% 0.59/1.16 inference(split_clause,[status(thm)],[f23691,f23255,f23705])).
% 0.59/1.16 fof(f23713,plain,(
% 0.59/1.16 $false|~sQ584_spl|sQ431_spl),
% 0.59/1.16 inference(backward_subsumption_resolution,[status(thm)],[f21484,f23256])).
% 0.59/1.16 fof(f23730,plain,(
% 0.59/1.16 ~sQ584_spl|sQ431_spl),
% 0.59/1.16 inference(contradiction_clause,[status(thm)],[f23713])).
% 0.59/1.16 fof(f23782,plain,(
% 0.59/1.16 ![X0]: (~k1_xboole_0=k1_xboole_0|r1_tarski(k1_xboole_0,X0))),
% 0.59/1.16 inference(paramodulation,[status(thm)],[f4651,f4736])).
% 0.59/1.16 fof(f23784,definition,(
% 0.59/1.16 ![X0]: (sQ591_spl <=> (r1_tarski(k1_xboole_0,X0)))),
% 0.59/1.16 introduced(definition,[new_symbols(definition,[sQ591_spl])],[split_symbol_definition])).
% 0.59/1.16 fof(f23787,plain,(
% 0.59/1.16 ~sQ589_spl|sQ591_spl),
% 0.59/1.16 inference(split_clause,[status(thm)],[f23782,f23639,f23784])).
% 0.59/1.16 fof(f23792,plain,(
% 0.59/1.16 ![X0]: (k4_xboole_0(X0,X0)=k1_xboole_0)),
% 0.59/1.16 inference(resolution,[status(thm)],[f4737,f23207])).
% 0.59/1.16 fof(f23843,plain,(
% 0.59/1.16 ![X0]: (~k1_xboole_0=k1_xboole_0|r1_tarski(X0,X0))),
% 0.59/1.16 inference(paramodulation,[status(thm)],[f23792,f4736])).
% 0.59/1.16 fof(f23847,definition,(
% 0.59/1.16 ![X0]: (sQ592_spl <=> (r1_tarski(X0,X0)))),
% 0.59/1.16 introduced(definition,[new_symbols(definition,[sQ592_spl])],[split_symbol_definition])).
% 0.59/1.16 fof(f23850,plain,(
% 0.59/1.16 ~sQ589_spl|sQ592_spl),
% 0.59/1.16 inference(split_clause,[status(thm)],[f23843,f23639,f23847])).
% 0.59/1.16 fof(f23855,definition,(
% 0.59/1.16 ![X0]: (sQ593_spl <=> (~r1_tarski(k1_xboole_0,X0)))),
% 0.59/1.16 introduced(definition,[new_symbols(definition,[sQ593_spl])],[split_symbol_definition])).
% 0.59/1.16 fof(f23856,plain,(
% 0.59/1.16 ![X0]: (~r1_tarski(k1_xboole_0,X0)|~sQ593_spl)),
% 0.59/1.16 inference(component_clause,[status(thm)],[f23855])).
% 0.59/1.16 fof(f23859,plain,(
% 0.59/1.16 $false|~sQ593_spl),
% 0.59/1.16 inference(forward_subsumption_resolution,[status(thm)],[f23856,f23399])).
% 0.59/1.16 fof(f23860,plain,(
% 0.59/1.16 ~sQ593_spl),
% 0.59/1.16 inference(contradiction_clause,[status(thm)],[f23859])).
% 0.59/1.16 fof(f24182,plain,(
% 0.59/1.16 r2_hidden(sK1190_skl,k4_xboole_0(sK1191_skl,sK1192_skl))|r2_hidden(sK1190_skl,sK1192_skl)),
% 0.59/1.16 inference(paramodulation,[status(thm)],[f4742,f23212])).
% 0.59/1.16 fof(f24183,plain,(
% 0.59/1.16 r2_hidden(sK1190_skl,k2_xboole_0(sK1191_skl,sK1192_skl))|r2_hidden(sK1190_skl,k1_xboole_0)),
% 0.59/1.16 inference(paramodulation,[status(thm)],[f4650,f23212])).
% 0.59/1.16 fof(f24187,plain,(
% 0.59/1.16 sQ432_spl|sQ434_spl),
% 0.59/1.16 inference(split_clause,[status(thm)],[f24182,f21485,f21492])).
% 0.59/1.16 fof(f24188,definition,(
% 0.59/1.16 sQ594_spl <=> (r2_hidden(sK1190_skl,k1_xboole_0))),
% 0.59/1.16 introduced(definition,[new_symbols(definition,[sQ594_spl])],[split_symbol_definition])).
% 0.59/1.16 fof(f24189,plain,(
% 0.59/1.16 r2_hidden(sK1190_skl,k1_xboole_0)|~sQ594_spl),
% 0.59/1.16 inference(component_clause,[status(thm)],[f24188])).
% 0.59/1.16 fof(f24191,plain,(
% 0.59/1.16 sQ587_spl|sQ594_spl),
% 0.59/1.16 inference(split_clause,[status(thm)],[f24183,f23566,f24188])).
% 0.59/1.16 fof(f24193,plain,(
% 0.59/1.16 $false|~sQ594_spl),
% 0.59/1.16 inference(forward_subsumption_resolution,[status(thm)],[f24189,f22089])).
% 0.59/1.16 fof(f24194,plain,(
% 0.59/1.16 ~sQ594_spl),
% 0.59/1.16 inference(contradiction_clause,[status(thm)],[f24193])).
% 0.59/1.16 fof(f24415,plain,(
% 0.59/1.16 r2_hidden(sK1189_skl,k4_xboole_0(sK1191_skl,sK1192_skl))|r2_hidden(sK1189_skl,sK1192_skl)),
% 0.59/1.16 inference(paramodulation,[status(thm)],[f4742,f23218])).
% 0.59/1.16 fof(f24420,plain,(
% 0.59/1.16 sQ431_spl|sQ433_spl),
% 0.59/1.16 inference(split_clause,[status(thm)],[f24415,f21482,f21489])).
% 0.59/1.16 fof(f24426,plain,(
% 0.59/1.16 $false),
% 0.59/1.16 inference(sat_refutation,[status(thm)],[f19908,f19912,f21488,f21495,f21496,f21497,f23500,f23642,f23644,f23708,f23730,f23787,f23850,f23860,f24187,f24191,f24194,f24420])).
% 0.59/1.16 % SZS output end CNFRefutation for theBenchmark.p
% 1.83/1.28 % Elapsed time: 0.896775 seconds
% 1.83/1.28 % CPU time: 3.199768 seconds
% 1.83/1.28 % Total memory used: 767.730 MB
% 1.83/1.28 % Net memory used: 761.607 MB
%------------------------------------------------------------------------------