%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC271-1 : TPTP v9.3.1. Released v2.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 02:42:01 PM UTC 2026
% Result : Unsatisfiable 16.60s 2.75s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWC271-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.47 % Computer : n009.cluster.edu
% 0.18/0.47 % Model : x86_64 x86_64
% 0.18/0.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.47 % Memory : 8046.5625MB
% 0.18/0.47 % OS : Linux 6.8.0-71-generic
% 0.18/0.47 % CPULimit : 300
% 0.18/0.47 % WCLimit : 300
% 0.18/0.47 % DateTime : Mon Sep 21 08:10:42 UTC 2026
% 0.18/0.48 % CPUTime :
% 0.18/0.49 % Drodi V4.1.1
% 16.60/2.75 % Refutation found
% 16.60/2.75 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 16.60/2.75 % SZS output start CNFRefutation for theBenchmark
% 16.60/2.75 fof(f27,axiom,(
% 16.60/2.75 (![U]: (ssList(skaf68(U)) ))),
% 16.60/2.75 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 16.60/2.75 fof(f28,axiom,(
% 16.60/2.75 (![U]: (ssList(skaf67(U)) ))),
% 16.60/2.75 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 16.60/2.75 fof(f29,axiom,(
% 16.60/2.75 (![U]: (ssList(skaf66(U)) ))),
% 16.60/2.75 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 16.60/2.75 fof(f30,axiom,(
% 16.60/2.75 (![U]: (ssItem(skaf65(U)) ))),
% 16.60/2.75 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 16.60/2.75 fof(f31,axiom,(
% 16.60/2.75 (![U]: (ssItem(skaf64(U)) ))),
% 16.60/2.75 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 16.60/2.75 fof(f91,axiom,(
% 16.60/2.75 (![U]: (( ~ leq(skaf64(U),skaf65(U))| ~ ssList(U)| totalorderedP(U) ) ))),
% 16.60/2.75 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 16.60/2.75 fof(f103,axiom,(
% 16.60/2.75 (![U,V]: (( ~ lt(U,V)| ~ ssItem(V)| ~ ssItem(U)| leq(U,V) ) ))),
% 16.60/2.75 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 16.60/2.75 fof(f164,axiom,(
% 16.60/2.75 (![U]: (( ~ ssList(U)| totalorderedP(U)| app(app(skaf66(U),cons(skaf64(U),skaf67(U))),cons(skaf65(U),skaf68(U))) = U ) ))),
% 16.60/2.75 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 16.60/2.75 fof(f181,axiom,(
% 16.60/2.75 (![U,V,W,X,Y,Z]: (( app(app(U,cons(V,W)),cons(X,Y)) != Z| ~ ssList(Y)| ~ ssList(W)| ~ ssList(U)| ~ ssItem(X)| ~ ssItem(V)| ~ strictorderedP(Z)| ~ ssList(Z)| lt(V,X) ) ))),
% 16.60/2.75 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 16.60/2.75 fof(f186,negated_conjecture,(
% 16.60/2.75 ssList(sk1) ),
% 16.60/2.75 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 16.60/2.75 fof(f191,negated_conjecture,(
% 16.60/2.75 sk1 = sk3 ),
% 16.60/2.75 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 16.60/2.75 fof(f193,negated_conjecture,(
% 16.60/2.75 strictorderedP(sk3) ),
% 16.60/2.75 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 16.60/2.75 fof(f195,negated_conjecture,(
% 16.60/2.75 ~ totalorderedP(sk1) ),
% 16.60/2.75 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 16.60/2.75 fof(f222,plain,(
% 16.60/2.75 ![X0]: (ssList(skaf68(X0)))),
% 16.60/2.75 inference(cnf_transformation,[status(thm)],[f27])).
% 16.60/2.75 fof(f223,plain,(
% 16.60/2.75 ![X0]: (ssList(skaf67(X0)))),
% 16.60/2.75 inference(cnf_transformation,[status(thm)],[f28])).
% 16.60/2.75 fof(f224,plain,(
% 16.60/2.75 ![X0]: (ssList(skaf66(X0)))),
% 16.60/2.75 inference(cnf_transformation,[status(thm)],[f29])).
% 16.60/2.75 fof(f225,plain,(
% 16.60/2.75 ![X0]: (ssItem(skaf65(X0)))),
% 16.60/2.75 inference(cnf_transformation,[status(thm)],[f30])).
% 16.60/2.75 fof(f226,plain,(
% 16.60/2.75 ![X0]: (ssItem(skaf64(X0)))),
% 16.60/2.75 inference(cnf_transformation,[status(thm)],[f31])).
% 16.60/2.75 fof(f287,plain,(
% 16.60/2.75 ![X0]: (~leq(skaf64(X0),skaf65(X0))|~ssList(X0)|totalorderedP(X0))),
% 16.60/2.75 inference(cnf_transformation,[status(thm)],[f91])).
% 16.60/2.75 fof(f301,plain,(
% 16.60/2.75 ![X0,X1]: (~lt(X0,X1)|~ssItem(X1)|~ssItem(X0)|leq(X0,X1))),
% 16.60/2.75 inference(cnf_transformation,[status(thm)],[f103])).
% 16.60/2.75 fof(f390,plain,(
% 16.60/2.75 ![X0]: (~ssList(X0)|totalorderedP(X0)|app(app(skaf66(X0),cons(skaf64(X0),skaf67(X0))),cons(skaf65(X0),skaf68(X0)))=X0)),
% 16.60/2.75 inference(cnf_transformation,[status(thm)],[f164])).
% 16.60/2.75 fof(f416,plain,(
% 16.60/2.75 ![V,X]: ((![Z]: (((((![U]: ((![W]: ((![Y]: (~app(app(U,cons(V,W)),cons(X,Y))=Z|~ssList(Y)))|~ssList(W)))|~ssList(U)))|~ssItem(X))|~ssItem(V))|~strictorderedP(Z))|~ssList(Z)))|lt(V,X))),
% 16.60/2.75 inference(miniscoping,[status(thm)],[f181])).
% 16.60/2.75 fof(f417,plain,(
% 16.60/2.75 ![X0,X1,X2,X3,X4,X5]: (~app(app(X0,cons(X1,X2)),cons(X3,X4))=X5|~ssList(X4)|~ssList(X2)|~ssList(X0)|~ssItem(X3)|~ssItem(X1)|~strictorderedP(X5)|~ssList(X5)|lt(X1,X3))),
% 16.60/2.75 inference(cnf_transformation,[status(thm)],[f416])).
% 16.60/2.75 fof(f426,plain,(
% 16.60/2.75 ssList(sk1)),
% 16.60/2.75 inference(cnf_transformation,[status(thm)],[f186])).
% 16.60/2.75 fof(f431,plain,(
% 16.60/2.75 sk1=sk3),
% 16.60/2.75 inference(cnf_transformation,[status(thm)],[f191])).
% 16.60/2.75 fof(f433,plain,(
% 16.60/2.75 strictorderedP(sk3)),
% 16.60/2.75 inference(cnf_transformation,[status(thm)],[f193])).
% 16.60/2.75 fof(f435,plain,(
% 16.60/2.75 ~totalorderedP(sk1)),
% 16.60/2.75 inference(cnf_transformation,[status(thm)],[f195])).
% 16.60/2.75 fof(f467,plain,(
% 16.60/2.75 ![X0,X1,X2,X3,X4]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssItem(X3)|~ssItem(X4)|~strictorderedP(app(app(X2,cons(X4,X1)),cons(X3,X0)))|~ssList(app(app(X2,cons(X4,X1)),cons(X3,X0)))|lt(X4,X3))),
% 16.60/2.75 inference(destructive_equality_resolution,[status(thm)],[f417])).
% 16.60/2.75 fof(f474,plain,(
% 16.60/2.75 strictorderedP(sk1)),
% 16.60/2.75 inference(forward_demodulation,[status(thm)],[f431,f433])).
% 16.60/2.75 fof(f502,definition,(
% 16.60/2.75 sQ5_spl <=> (ssList(sk1))),
% 16.60/2.75 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 16.60/2.75 fof(f504,plain,(
% 16.60/2.75 ~ssList(sk1)|sQ5_spl),
% 16.60/2.75 inference(component_clause,[status(thm)],[f502])).
% 16.60/2.75 fof(f518,plain,(
% 16.60/2.75 $false|sQ5_spl),
% 16.60/2.75 inference(forward_subsumption_resolution,[status(thm)],[f504,f426])).
% 16.60/2.75 fof(f519,plain,(
% 16.60/2.75 sQ5_spl),
% 16.60/2.75 inference(contradiction_clause,[status(thm)],[f518])).
% 16.60/2.75 fof(f3215,definition,(
% 16.60/2.75 sQ314_spl <=> (totalorderedP(sk1))),
% 16.60/2.75 introduced(definition,[new_symbols(definition,[sQ314_spl])],[split_symbol_definition])).
% 16.60/2.75 fof(f3216,plain,(
% 16.60/2.75 totalorderedP(sk1)|~sQ314_spl),
% 16.60/2.75 inference(component_clause,[status(thm)],[f3215])).
% 16.60/2.75 fof(f4312,plain,(
% 16.60/2.75 $false|~sQ314_spl),
% 16.60/2.75 inference(forward_subsumption_resolution,[status(thm)],[f3216,f435])).
% 16.60/2.75 fof(f4313,plain,(
% 16.60/2.75 ~sQ314_spl),
% 16.60/2.75 inference(contradiction_clause,[status(thm)],[f4312])).
% 16.60/2.75 fof(f7745,plain,(
% 16.60/2.75 totalorderedP(sk1)|app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1)))=sk1),
% 16.60/2.75 inference(resolution,[status(thm)],[f390,f426])).
% 16.60/2.75 fof(f7778,definition,(
% 16.60/2.75 sQ768_spl <=> (app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1)))=sk1)),
% 16.60/2.75 introduced(definition,[new_symbols(definition,[sQ768_spl])],[split_symbol_definition])).
% 16.60/2.75 fof(f7779,plain,(
% 16.60/2.75 app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1)))=sk1|~sQ768_spl),
% 16.60/2.75 inference(component_clause,[status(thm)],[f7778])).
% 16.60/2.75 fof(f7781,plain,(
% 16.60/2.75 sQ314_spl|sQ768_spl),
% 16.60/2.75 inference(split_clause,[status(thm)],[f7745,f3215,f7778])).
% 16.60/2.75 fof(f10899,plain,(
% 16.60/2.75 ~ssList(skaf68(sk1))|~ssList(skaf67(sk1))|~ssList(skaf66(sk1))|~ssItem(skaf65(sk1))|~ssItem(skaf64(sk1))|~strictorderedP(app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1))))|~ssList(sk1)|lt(skaf64(sk1),skaf65(sk1))|~sQ768_spl),
% 16.60/2.75 inference(paramodulation,[status(thm)],[f7779,f467])).
% 16.60/2.75 fof(f10902,definition,(
% 16.60/2.75 sQ938_spl <=> (ssList(skaf68(sk1)))),
% 16.60/2.75 introduced(definition,[new_symbols(definition,[sQ938_spl])],[split_symbol_definition])).
% 16.60/2.75 fof(f10904,plain,(
% 16.60/2.75 ~ssList(skaf68(sk1))|sQ938_spl),
% 16.60/2.75 inference(component_clause,[status(thm)],[f10902])).
% 16.60/2.75 fof(f10905,definition,(
% 16.60/2.75 sQ939_spl <=> (ssList(skaf67(sk1)))),
% 16.60/2.75 introduced(definition,[new_symbols(definition,[sQ939_spl])],[split_symbol_definition])).
% 16.60/2.75 fof(f10907,plain,(
% 16.60/2.75 ~ssList(skaf67(sk1))|sQ939_spl),
% 16.60/2.75 inference(component_clause,[status(thm)],[f10905])).
% 16.60/2.75 fof(f10908,definition,(
% 16.60/2.75 sQ940_spl <=> (ssList(skaf66(sk1)))),
% 16.60/2.75 introduced(definition,[new_symbols(definition,[sQ940_spl])],[split_symbol_definition])).
% 16.60/2.75 fof(f10910,plain,(
% 16.60/2.75 ~ssList(skaf66(sk1))|sQ940_spl),
% 16.60/2.75 inference(component_clause,[status(thm)],[f10908])).
% 16.60/2.75 fof(f10911,definition,(
% 16.60/2.75 sQ941_spl <=> (ssItem(skaf65(sk1)))),
% 16.60/2.75 introduced(definition,[new_symbols(definition,[sQ941_spl])],[split_symbol_definition])).
% 16.60/2.75 fof(f10913,plain,(
% 16.60/2.75 ~ssItem(skaf65(sk1))|sQ941_spl),
% 16.60/2.75 inference(component_clause,[status(thm)],[f10911])).
% 16.60/2.75 fof(f10914,definition,(
% 16.60/2.75 sQ942_spl <=> (ssItem(skaf64(sk1)))),
% 16.60/2.75 introduced(definition,[new_symbols(definition,[sQ942_spl])],[split_symbol_definition])).
% 16.60/2.75 fof(f10916,plain,(
% 16.60/2.75 ~ssItem(skaf64(sk1))|sQ942_spl),
% 16.60/2.75 inference(component_clause,[status(thm)],[f10914])).
% 16.60/2.75 fof(f10920,definition,(
% 16.60/2.75 sQ944_spl <=> (leq(skaf64(sk1),skaf65(sk1)))),
% 16.60/2.75 introduced(definition,[new_symbols(definition,[sQ944_spl])],[split_symbol_definition])).
% 16.60/2.75 fof(f10921,plain,(
% 16.60/2.75 leq(skaf64(sk1),skaf65(sk1))|~sQ944_spl),
% 16.60/2.75 inference(component_clause,[status(thm)],[f10920])).
% 16.60/2.75 fof(f10924,definition,(
% 16.60/2.75 sQ945_spl <=> (strictorderedP(app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1)))))),
% 16.60/2.75 introduced(definition,[new_symbols(definition,[sQ945_spl])],[split_symbol_definition])).
% 16.60/2.75 fof(f10926,plain,(
% 16.60/2.75 ~strictorderedP(app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1))))|sQ945_spl),
% 16.60/2.75 inference(component_clause,[status(thm)],[f10924])).
% 16.60/2.75 fof(f10927,definition,(
% 16.60/2.75 sQ946_spl <=> (lt(skaf64(sk1),skaf65(sk1)))),
% 16.60/2.75 introduced(definition,[new_symbols(definition,[sQ946_spl])],[split_symbol_definition])).
% 16.60/2.75 fof(f10928,plain,(
% 16.60/2.75 lt(skaf64(sk1),skaf65(sk1))|~sQ946_spl),
% 16.60/2.75 inference(component_clause,[status(thm)],[f10927])).
% 16.60/2.75 fof(f10930,plain,(
% 16.60/2.75 ~sQ938_spl|~sQ939_spl|~sQ940_spl|~sQ941_spl|~sQ942_spl|~sQ945_spl|~sQ5_spl|sQ946_spl|~sQ768_spl),
% 16.60/2.75 inference(split_clause,[status(thm)],[f10899,f10902,f10905,f10908,f10911,f10914,f10924,f502,f10927,f7778])).
% 16.60/2.75 fof(f10942,plain,(
% 16.60/2.75 $false|sQ941_spl),
% 16.60/2.75 inference(forward_subsumption_resolution,[status(thm)],[f10913,f225])).
% 16.60/2.75 fof(f10943,plain,(
% 16.60/2.75 sQ941_spl),
% 16.60/2.75 inference(contradiction_clause,[status(thm)],[f10942])).
% 16.60/2.75 fof(f10944,plain,(
% 16.60/2.75 $false|sQ938_spl),
% 16.60/2.75 inference(forward_subsumption_resolution,[status(thm)],[f10904,f222])).
% 16.60/2.75 fof(f10945,plain,(
% 16.60/2.75 sQ938_spl),
% 16.60/2.75 inference(contradiction_clause,[status(thm)],[f10944])).
% 16.60/2.75 fof(f10946,plain,(
% 16.60/2.75 $false|sQ942_spl),
% 16.60/2.75 inference(forward_subsumption_resolution,[status(thm)],[f10916,f226])).
% 16.60/2.75 fof(f10947,plain,(
% 16.60/2.75 sQ942_spl),
% 16.60/2.75 inference(contradiction_clause,[status(thm)],[f10946])).
% 16.60/2.75 fof(f10948,plain,(
% 16.60/2.75 $false|sQ940_spl),
% 16.60/2.75 inference(forward_subsumption_resolution,[status(thm)],[f10910,f224])).
% 16.60/2.75 fof(f10949,plain,(
% 16.60/2.75 sQ940_spl),
% 16.60/2.75 inference(contradiction_clause,[status(thm)],[f10948])).
% 16.60/2.75 fof(f10950,plain,(
% 16.60/2.75 $false|sQ939_spl),
% 16.60/2.75 inference(forward_subsumption_resolution,[status(thm)],[f10907,f223])).
% 16.60/2.75 fof(f10951,plain,(
% 16.60/2.75 sQ939_spl),
% 16.60/2.75 inference(contradiction_clause,[status(thm)],[f10950])).
% 16.60/2.75 fof(f10954,plain,(
% 16.60/2.75 ~strictorderedP(sk1)|~sQ768_spl|sQ945_spl),
% 16.60/2.75 inference(forward_demodulation,[status(thm)],[f7779,f10926])).
% 16.60/2.75 fof(f10955,plain,(
% 16.60/2.75 $false|~sQ768_spl|sQ945_spl),
% 16.60/2.75 inference(forward_subsumption_resolution,[status(thm)],[f10954,f474])).
% 16.60/2.75 fof(f10956,plain,(
% 16.60/2.75 ~sQ768_spl|sQ945_spl),
% 16.60/2.75 inference(contradiction_clause,[status(thm)],[f10955])).
% 16.60/2.75 fof(f11087,definition,(
% 16.60/2.75 sQ957_spl <=> (ssList(skaf68(sk2)))),
% 16.60/2.75 introduced(definition,[new_symbols(definition,[sQ957_spl])],[split_symbol_definition])).
% 16.60/2.75 fof(f11089,plain,(
% 16.60/2.75 ~ssList(skaf68(sk2))|sQ957_spl),
% 16.60/2.75 inference(component_clause,[status(thm)],[f11087])).
% 16.60/2.75 fof(f11090,definition,(
% 16.60/2.75 sQ958_spl <=> (ssList(skaf67(sk2)))),
% 16.60/2.75 introduced(definition,[new_symbols(definition,[sQ958_spl])],[split_symbol_definition])).
% 16.60/2.75 fof(f11092,plain,(
% 16.60/2.75 ~ssList(skaf67(sk2))|sQ958_spl),
% 16.60/2.75 inference(component_clause,[status(thm)],[f11090])).
% 16.60/2.75 fof(f11093,definition,(
% 16.60/2.75 sQ959_spl <=> (ssList(skaf66(sk2)))),
% 16.60/2.75 introduced(definition,[new_symbols(definition,[sQ959_spl])],[split_symbol_definition])).
% 16.60/2.75 fof(f11095,plain,(
% 16.60/2.75 ~ssList(skaf66(sk2))|sQ959_spl),
% 16.60/2.75 inference(component_clause,[status(thm)],[f11093])).
% 16.60/2.75 fof(f11096,definition,(
% 16.60/2.75 sQ960_spl <=> (ssItem(skaf65(sk2)))),
% 16.60/2.75 introduced(definition,[new_symbols(definition,[sQ960_spl])],[split_symbol_definition])).
% 16.60/2.75 fof(f11098,plain,(
% 16.60/2.75 ~ssItem(skaf65(sk2))|sQ960_spl),
% 16.60/2.75 inference(component_clause,[status(thm)],[f11096])).
% 16.60/2.75 fof(f11099,definition,(
% 16.60/2.75 sQ961_spl <=> (ssItem(skaf64(sk2)))),
% 16.60/2.75 introduced(definition,[new_symbols(definition,[sQ961_spl])],[split_symbol_definition])).
% 16.60/2.75 fof(f11101,plain,(
% 16.60/2.75 ~ssItem(skaf64(sk2))|sQ961_spl),
% 16.60/2.75 inference(component_clause,[status(thm)],[f11099])).
% 16.60/2.75 fof(f11127,plain,(
% 16.60/2.75 $false|sQ960_spl),
% 16.60/2.75 inference(forward_subsumption_resolution,[status(thm)],[f11098,f225])).
% 16.60/2.75 fof(f11128,plain,(
% 16.60/2.75 sQ960_spl),
% 16.60/2.75 inference(contradiction_clause,[status(thm)],[f11127])).
% 16.60/2.75 fof(f11129,plain,(
% 16.60/2.75 $false|sQ957_spl),
% 16.60/2.75 inference(forward_subsumption_resolution,[status(thm)],[f11089,f222])).
% 16.60/2.75 fof(f11130,plain,(
% 16.60/2.75 sQ957_spl),
% 16.60/2.75 inference(contradiction_clause,[status(thm)],[f11129])).
% 16.60/2.75 fof(f11131,plain,(
% 16.60/2.75 $false|sQ961_spl),
% 16.60/2.75 inference(forward_subsumption_resolution,[status(thm)],[f11101,f226])).
% 16.60/2.75 fof(f11132,plain,(
% 16.60/2.75 sQ961_spl),
% 16.60/2.75 inference(contradiction_clause,[status(thm)],[f11131])).
% 16.60/2.75 fof(f11133,plain,(
% 16.60/2.75 $false|sQ959_spl),
% 16.60/2.75 inference(forward_subsumption_resolution,[status(thm)],[f11095,f224])).
% 16.60/2.75 fof(f11134,plain,(
% 16.60/2.75 sQ959_spl),
% 16.60/2.75 inference(contradiction_clause,[status(thm)],[f11133])).
% 16.60/2.75 fof(f11135,plain,(
% 16.60/2.75 $false|sQ958_spl),
% 16.60/2.75 inference(forward_subsumption_resolution,[status(thm)],[f11092,f223])).
% 16.60/2.75 fof(f11136,plain,(
% 16.60/2.75 sQ958_spl),
% 16.60/2.75 inference(contradiction_clause,[status(thm)],[f11135])).
% 16.60/2.78 fof(f11658,plain,(
% 16.60/2.78 ~ssItem(skaf65(sk1))|~ssItem(skaf64(sk1))|leq(skaf64(sk1),skaf65(sk1))|~sQ946_spl),
% 16.60/2.78 inference(resolution,[status(thm)],[f10928,f301])).
% 16.60/2.78 fof(f11663,plain,(
% 16.60/2.78 ~sQ941_spl|~sQ942_spl|sQ944_spl|~sQ946_spl),
% 16.60/2.78 inference(split_clause,[status(thm)],[f11658,f10911,f10914,f10920,f10927])).
% 16.60/2.78 fof(f11688,plain,(
% 16.60/2.78 ~ssList(sk1)|totalorderedP(sk1)|~sQ944_spl),
% 16.60/2.78 inference(resolution,[status(thm)],[f10921,f287])).
% 16.60/2.78 fof(f11693,plain,(
% 16.60/2.78 ~sQ5_spl|sQ314_spl|~sQ944_spl),
% 16.60/2.78 inference(split_clause,[status(thm)],[f11688,f502,f3215,f10920])).
% 16.60/2.78 fof(f11710,plain,(
% 16.60/2.78 $false),
% 16.60/2.78 inference(sat_refutation,[status(thm)],[f519,f4313,f7781,f10930,f10943,f10945,f10947,f10949,f10951,f10956,f11128,f11130,f11132,f11134,f11136,f11663,f11693])).
% 16.60/2.78 % SZS output end CNFRefutation for theBenchmark.p
% 16.60/2.81 % Elapsed time: 2.311259 seconds
% 16.60/2.81 % CPU time: 17.795376 seconds
% 16.60/2.81 % Total memory used: 274.616 MB
% 16.60/2.81 % Net memory used: 265.178 MB
%------------------------------------------------------------------------------