%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NUM390+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.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 01:42:49 PM UTC 2026
% Result : Theorem 0.13s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM390+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n005.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 02:26:33 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 0.13/0.40 % Refutation found
% 0.13/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.40 fof(f1,axiom,(
% 0.13/0.40 (! [A,B] :( in(A,B)=> ~ in(B,A) ) )),
% 0.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f2,axiom,(
% 0.13/0.40 (! [A,B] :( proper_subset(A,B)=> ~ proper_subset(B,A) ) )),
% 0.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f4,axiom,(
% 0.13/0.40 (! [A] :( ordinal(A)=> ( epsilon_transitive(A)& epsilon_connected(A) ) ) )),
% 0.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f7,axiom,(
% 0.13/0.40 (! [A] :( ( epsilon_transitive(A)& epsilon_connected(A) )=> ordinal(A) ) )),
% 0.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f8,axiom,(
% 0.13/0.40 (! [A] :( epsilon_transitive(A)<=> (! [B] :( in(B,A)=> subset(B,A) ) )) )),
% 0.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f9,axiom,(
% 0.13/0.40 (! [A,B] :( proper_subset(A,B)<=> ( subset(A,B)& A != B ) ) )),
% 0.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f28,axiom,(
% 0.13/0.40 (! [A,B,C] :( ( subset(A,B)& subset(B,C) )=> subset(A,C) ) )),
% 0.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f29,axiom,(
% 0.13/0.40 (! [A] :( epsilon_transitive(A)=> (! [B] :( ordinal(B)=> ( proper_subset(A,B)=> in(A,B) ) ) )) )),
% 0.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f30,conjecture,(
% 0.13/0.40 (! [A] :( epsilon_transitive(A)=> (! [B] :( ordinal(B)=> (! [C] :( ordinal(C)=> ( ( subset(A,B)& in(B,C) )=> in(A,C) ) ) )) )) )),
% 0.13/0.40 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f31,negated_conjecture,(
% 0.13/0.40 ~((! [A] :( epsilon_transitive(A)=> (! [B] :( ordinal(B)=> (! [C] :( ordinal(C)=> ( ( subset(A,B)& in(B,C) )=> in(A,C) ) ) )) )) ))),
% 0.13/0.40 inference(negated_conjecture,[status(cth)],[f30])).
% 0.13/0.40 fof(f40,plain,(
% 0.13/0.40 ![A,B]: (~in(A,B)|~in(B,A))),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f1])).
% 0.13/0.40 fof(f41,plain,(
% 0.13/0.40 ![X0,X1]: (~in(X0,X1)|~in(X1,X0))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f40])).
% 0.13/0.40 fof(f42,plain,(
% 0.13/0.40 ![A,B]: (~proper_subset(A,B)|~proper_subset(B,A))),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.13/0.40 fof(f43,plain,(
% 0.13/0.40 ![X0,X1]: (~proper_subset(X0,X1)|~proper_subset(X1,X0))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.13/0.40 fof(f46,plain,(
% 0.13/0.40 ![A]: (~ordinal(A)|(epsilon_transitive(A)&epsilon_connected(A)))),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 0.13/0.40 fof(f47,plain,(
% 0.13/0.40 ![X0]: (~ordinal(X0)|epsilon_transitive(X0))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f46])).
% 0.13/0.40 fof(f48,plain,(
% 0.13/0.40 ![X0]: (~ordinal(X0)|epsilon_connected(X0))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f46])).
% 0.13/0.40 fof(f55,plain,(
% 0.13/0.40 ![A]: ((~epsilon_transitive(A)|~epsilon_connected(A))|ordinal(A))),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f7])).
% 0.13/0.40 fof(f56,plain,(
% 0.13/0.40 ![X0]: (~epsilon_transitive(X0)|~epsilon_connected(X0)|ordinal(X0))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f55])).
% 0.13/0.40 fof(f57,plain,(
% 0.13/0.40 ![A]: (epsilon_transitive(A)<=>(![B]: (~in(B,A)|subset(B,A))))),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.13/0.40 fof(f58,plain,(
% 0.13/0.40 ![A]: ((~epsilon_transitive(A)|(![B]: (~in(B,A)|subset(B,A))))&(epsilon_transitive(A)|(?[B]: (in(B,A)&~subset(B,A)))))),
% 0.13/0.40 inference(NNF_transformation,[status(thm)],[f57])).
% 0.13/0.40 fof(f59,plain,(
% 0.13/0.40 (![A]: (~epsilon_transitive(A)|(![B]: (~in(B,A)|subset(B,A)))))&(![A]: (epsilon_transitive(A)|(?[B]: (in(B,A)&~subset(B,A)))))),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f58])).
% 0.13/0.40 fof(f60,plain,(
% 0.13/0.40 (![A]: (~epsilon_transitive(A)|(![B]: (~in(B,A)|subset(B,A)))))&(![A]: (epsilon_transitive(A)|(in(sK0_skl(A),A)&~subset(sK0_skl(A),A))))),
% 0.13/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(B,sK0_skl(A))],[f59])).
% 0.13/0.40 fof(f61,plain,(
% 0.13/0.40 ![X0,X1]: (~epsilon_transitive(X0)|~in(X1,X0)|subset(X1,X0))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f60])).
% 0.13/0.40 fof(f64,plain,(
% 0.13/0.40 ![A,B]: ((~proper_subset(A,B)|(subset(A,B)&~A=B))&(proper_subset(A,B)|(~subset(A,B)|A=B)))),
% 0.13/0.40 inference(NNF_transformation,[status(thm)],[f9])).
% 0.13/0.40 fof(f65,plain,(
% 0.13/0.40 (![A,B]: (~proper_subset(A,B)|(subset(A,B)&~A=B)))&(![A,B]: (proper_subset(A,B)|(~subset(A,B)|A=B)))),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f64])).
% 0.13/0.40 fof(f68,plain,(
% 0.13/0.40 ![X0,X1]: (proper_subset(X0,X1)|~subset(X0,X1)|X0=X1)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f65])).
% 0.13/0.40 fof(f119,plain,(
% 0.13/0.40 ![A,B,C]: ((~subset(A,B)|~subset(B,C))|subset(A,C))),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 0.13/0.40 fof(f120,plain,(
% 0.13/0.40 ![A,C]: ((![B]: (~subset(A,B)|~subset(B,C)))|subset(A,C))),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f119])).
% 0.13/0.40 fof(f121,plain,(
% 0.13/0.40 ![X0,X1,X2]: (~subset(X0,X1)|~subset(X1,X2)|subset(X0,X2))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f120])).
% 0.13/0.40 fof(f122,plain,(
% 0.13/0.40 ![A]: (~epsilon_transitive(A)|(![B]: (~ordinal(B)|(~proper_subset(A,B)|in(A,B)))))),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 0.13/0.40 fof(f123,plain,(
% 0.13/0.40 ![X0,X1]: (~epsilon_transitive(X0)|~ordinal(X1)|~proper_subset(X0,X1)|in(X0,X1))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f122])).
% 0.13/0.40 fof(f124,plain,(
% 0.13/0.40 (?[A]: (epsilon_transitive(A)&(?[B]: (ordinal(B)&(?[C]: (ordinal(C)&((subset(A,B)&in(B,C))&~in(A,C))))))))),
% 0.13/0.40 inference(pre_NNF_transformation,[status(thm)],[f31])).
% 0.13/0.40 fof(f125,plain,(
% 0.13/0.40 (epsilon_transitive(sK13_skl)&(ordinal(sK14_skl)&(ordinal(sK15_skl)&((subset(sK13_skl,sK14_skl)&in(sK14_skl,sK15_skl))&~in(sK13_skl,sK15_skl)))))),
% 0.13/0.40 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl,sK15_skl]),skolemize(A,sK13_skl),skolemize(B,sK14_skl),skolemize(C,sK15_skl)],[f124])).
% 0.13/0.40 fof(f126,plain,(
% 0.13/0.40 epsilon_transitive(sK13_skl)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f125])).
% 0.13/0.40 fof(f128,plain,(
% 0.13/0.40 ordinal(sK15_skl)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f125])).
% 0.13/0.40 fof(f129,plain,(
% 0.13/0.40 subset(sK13_skl,sK14_skl)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f125])).
% 0.13/0.40 fof(f130,plain,(
% 0.13/0.40 in(sK14_skl,sK15_skl)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f125])).
% 0.13/0.40 fof(f131,plain,(
% 0.13/0.40 ~in(sK13_skl,sK15_skl)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f125])).
% 0.13/0.40 fof(f156,plain,(
% 0.13/0.40 epsilon_transitive(sK15_skl)),
% 0.13/0.40 inference(resolution,[status(thm)],[f47,f128])).
% 0.13/0.40 fof(f160,plain,(
% 0.13/0.40 epsilon_connected(sK15_skl)),
% 0.13/0.40 inference(resolution,[status(thm)],[f48,f128])).
% 0.13/0.40 fof(f166,plain,(
% 0.13/0.40 proper_subset(sK13_skl,sK14_skl)|sK13_skl=sK14_skl),
% 0.13/0.40 inference(resolution,[status(thm)],[f129,f68])).
% 0.13/0.40 fof(f167,plain,(
% 0.13/0.40 ![X0]: (~subset(sK14_skl,X0)|subset(sK13_skl,X0))),
% 0.13/0.40 inference(resolution,[status(thm)],[f129,f121])).
% 0.13/0.40 fof(f168,definition,(
% 0.13/0.40 sQ0_spl <=> (proper_subset(sK13_skl,sK14_skl))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f169,plain,(
% 0.13/0.40 proper_subset(sK13_skl,sK14_skl)|~sQ0_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f168])).
% 0.13/0.40 fof(f171,definition,(
% 0.13/0.40 sQ1_spl <=> (sK13_skl=sK14_skl)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f172,plain,(
% 0.13/0.40 sK13_skl=sK14_skl|~sQ1_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f171])).
% 0.13/0.40 fof(f174,plain,(
% 0.13/0.40 sQ0_spl|sQ1_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f166,f168,f171])).
% 0.13/0.40 fof(f175,plain,(
% 0.13/0.40 ~epsilon_transitive(sK15_skl)|subset(sK14_skl,sK15_skl)),
% 0.13/0.40 inference(resolution,[status(thm)],[f130,f61])).
% 0.13/0.40 fof(f176,plain,(
% 0.13/0.40 ~in(sK15_skl,sK14_skl)),
% 0.13/0.40 inference(resolution,[status(thm)],[f130,f41])).
% 0.13/0.40 fof(f177,definition,(
% 0.13/0.40 sQ2_spl <=> (epsilon_transitive(sK15_skl))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f179,plain,(
% 0.13/0.40 ~epsilon_transitive(sK15_skl)|sQ2_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f177])).
% 0.13/0.40 fof(f180,definition,(
% 0.13/0.40 sQ3_spl <=> (subset(sK14_skl,sK15_skl))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f181,plain,(
% 0.13/0.40 subset(sK14_skl,sK15_skl)|~sQ3_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f180])).
% 0.13/0.40 fof(f183,plain,(
% 0.13/0.40 ~sQ2_spl|sQ3_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f175,f177,f180])).
% 0.13/0.40 fof(f184,plain,(
% 0.13/0.40 $false|sQ2_spl),
% 0.13/0.40 inference(forward_subsumption_resolution,[status(thm)],[f179,f156])).
% 0.13/0.40 fof(f185,plain,(
% 0.13/0.40 sQ2_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f184])).
% 0.13/0.40 fof(f186,plain,(
% 0.13/0.40 ~epsilon_transitive(sK15_skl)|ordinal(sK15_skl)),
% 0.13/0.40 inference(resolution,[status(thm)],[f160,f56])).
% 0.13/0.40 fof(f187,definition,(
% 0.13/0.40 sQ4_spl <=> (ordinal(sK15_skl))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f190,plain,(
% 0.13/0.40 ~sQ2_spl|sQ4_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f186,f177,f187])).
% 0.13/0.40 fof(f204,definition,(
% 0.13/0.40 sQ7_spl <=> (epsilon_transitive(sK13_skl))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f206,plain,(
% 0.13/0.40 ~epsilon_transitive(sK13_skl)|sQ7_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f204])).
% 0.13/0.40 fof(f214,plain,(
% 0.13/0.40 in(sK13_skl,sK15_skl)|~sQ1_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f172,f130])).
% 0.13/0.40 fof(f220,plain,(
% 0.13/0.40 $false|~sQ1_spl),
% 0.13/0.40 inference(forward_subsumption_resolution,[status(thm)],[f214,f131])).
% 0.13/0.40 fof(f221,plain,(
% 0.13/0.40 ~sQ1_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f220])).
% 0.13/0.40 fof(f222,plain,(
% 0.13/0.40 $false|sQ7_spl),
% 0.13/0.40 inference(forward_subsumption_resolution,[status(thm)],[f206,f126])).
% 0.13/0.40 fof(f223,plain,(
% 0.13/0.40 sQ7_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f222])).
% 0.13/0.40 fof(f234,plain,(
% 0.13/0.40 proper_subset(sK14_skl,sK15_skl)|sK14_skl=sK15_skl|~sQ3_spl),
% 0.13/0.40 inference(resolution,[status(thm)],[f181,f68])).
% 0.13/0.40 fof(f236,definition,(
% 0.13/0.40 sQ9_spl <=> (proper_subset(sK14_skl,sK15_skl))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f237,plain,(
% 0.13/0.40 proper_subset(sK14_skl,sK15_skl)|~sQ9_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f236])).
% 0.13/0.40 fof(f239,definition,(
% 0.13/0.40 sQ10_spl <=> (sK14_skl=sK15_skl)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f240,plain,(
% 0.13/0.40 sK14_skl=sK15_skl|~sQ10_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f239])).
% 0.13/0.40 fof(f242,plain,(
% 0.13/0.40 sQ9_spl|sQ10_spl|~sQ3_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f234,f236,f239,f180])).
% 0.13/0.40 fof(f243,plain,(
% 0.13/0.40 subset(sK13_skl,sK15_skl)|~sQ3_spl),
% 0.13/0.40 inference(resolution,[status(thm)],[f167,f181])).
% 0.13/0.40 fof(f255,plain,(
% 0.13/0.40 ~proper_subset(sK15_skl,sK14_skl)|~sQ9_spl),
% 0.13/0.40 inference(resolution,[status(thm)],[f237,f43])).
% 0.13/0.40 fof(f262,plain,(
% 0.13/0.40 ~in(sK14_skl,sK14_skl)|~sQ10_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f240,f176])).
% 0.13/0.40 fof(f264,plain,(
% 0.13/0.40 in(sK14_skl,sK14_skl)|~sQ10_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f240,f130])).
% 0.13/0.40 fof(f270,plain,(
% 0.13/0.40 $false|~sQ10_spl),
% 0.13/0.40 inference(forward_subsumption_resolution,[status(thm)],[f264,f262])).
% 0.13/0.40 fof(f271,plain,(
% 0.13/0.40 ~sQ10_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f270])).
% 0.13/0.40 fof(f284,plain,(
% 0.13/0.40 proper_subset(sK13_skl,sK15_skl)|sK13_skl=sK15_skl|~sQ3_spl),
% 0.13/0.40 inference(resolution,[status(thm)],[f243,f68])).
% 0.13/0.40 fof(f286,definition,(
% 0.13/0.40 sQ13_spl <=> (proper_subset(sK13_skl,sK15_skl))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f287,plain,(
% 0.13/0.40 proper_subset(sK13_skl,sK15_skl)|~sQ13_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f286])).
% 0.13/0.40 fof(f289,definition,(
% 0.13/0.40 sQ14_spl <=> (sK13_skl=sK15_skl)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f290,plain,(
% 0.13/0.40 sK13_skl=sK15_skl|~sQ14_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f289])).
% 0.13/0.40 fof(f292,plain,(
% 0.13/0.40 sQ13_spl|sQ14_spl|~sQ3_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f284,f286,f289,f180])).
% 0.13/0.40 fof(f297,plain,(
% 0.13/0.40 ~epsilon_transitive(sK13_skl)|~ordinal(sK15_skl)|in(sK13_skl,sK15_skl)|~sQ13_spl),
% 0.13/0.40 inference(resolution,[status(thm)],[f287,f123])).
% 0.13/0.40 fof(f298,definition,(
% 0.13/0.40 sQ15_spl <=> (in(sK13_skl,sK15_skl))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f299,plain,(
% 0.13/0.40 in(sK13_skl,sK15_skl)|~sQ15_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f298])).
% 0.13/0.40 fof(f301,plain,(
% 0.13/0.40 ~sQ7_spl|~sQ4_spl|sQ15_spl|~sQ13_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f297,f204,f187,f298,f286])).
% 0.13/0.40 fof(f302,plain,(
% 0.13/0.40 $false|~sQ15_spl),
% 0.13/0.40 inference(forward_subsumption_resolution,[status(thm)],[f299,f131])).
% 0.13/0.40 fof(f303,plain,(
% 0.13/0.40 ~sQ15_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f302])).
% 0.13/0.40 fof(f304,plain,(
% 0.13/0.40 ~proper_subset(sK13_skl,sK14_skl)|~sQ14_spl|~sQ9_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f290,f255])).
% 0.13/0.40 fof(f319,plain,(
% 0.13/0.40 $false|~sQ0_spl|~sQ14_spl|~sQ9_spl),
% 0.13/0.40 inference(forward_subsumption_resolution,[status(thm)],[f304,f169])).
% 0.13/0.40 fof(f320,plain,(
% 0.13/0.40 ~sQ0_spl|~sQ14_spl|~sQ9_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f319])).
% 0.13/0.40 fof(f321,plain,(
% 0.13/0.40 $false),
% 0.13/0.40 inference(sat_refutation,[status(thm)],[f174,f183,f185,f190,f221,f223,f242,f271,f292,f301,f303,f320])).
% 0.13/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.42 % Elapsed time: 0.059366 seconds
% 0.13/0.42 % CPU time: 0.144840 seconds
% 0.13/0.42 % Total memory used: 21.508 MB
% 0.13/0.42 % Net memory used: 21.335 MB
%------------------------------------------------------------------------------