%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC270-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 : n017.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 29.55s 9.25s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWC270-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/5.44 % Computer : n017.cluster.edu
% 0.18/5.44 % Model : x86_64 x86_64
% 0.18/5.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/5.44 % Memory : 8046.5625MB
% 0.18/5.44 % OS : Linux 6.8.0-71-generic
% 0.18/5.44 % CPULimit : 300
% 0.18/5.44 % WCLimit : 300
% 0.18/5.44 % DateTime : Mon Sep 21 08:06:18 UTC 2026
% 0.18/5.44 % CPUTime :
% 0.18/5.46 % Drodi V4.1.1
% 29.55/9.25 % Refutation found
% 29.55/9.25 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 29.55/9.25 % SZS output start CNFRefutation for theBenchmark
% 29.55/9.25 fof(f27,axiom,(
% 29.55/9.25 (![U]: (ssList(skaf68(U)) ))),
% 29.55/9.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.55/9.25 fof(f28,axiom,(
% 29.55/9.25 (![U]: (ssList(skaf67(U)) ))),
% 29.55/9.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.55/9.25 fof(f29,axiom,(
% 29.55/9.25 (![U]: (ssList(skaf66(U)) ))),
% 29.55/9.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.55/9.25 fof(f30,axiom,(
% 29.55/9.25 (![U]: (ssItem(skaf65(U)) ))),
% 29.55/9.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.55/9.25 fof(f31,axiom,(
% 29.55/9.25 (![U]: (ssItem(skaf64(U)) ))),
% 29.55/9.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.55/9.25 fof(f47,axiom,(
% 29.55/9.25 (![U]: (ssItem(skaf44(U)) ))),
% 29.55/9.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.55/9.25 fof(f74,axiom,(
% 29.55/9.25 (![U]: (( ~ ssList(U)| app(nil,U) = U ) ))),
% 29.55/9.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.55/9.25 fof(f91,axiom,(
% 29.55/9.25 (![U]: (( ~ leq(skaf64(U),skaf65(U))| ~ ssList(U)| totalorderedP(U) ) ))),
% 29.55/9.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.55/9.25 fof(f103,axiom,(
% 29.55/9.25 (![U,V]: (( ~ lt(U,V)| ~ ssItem(V)| ~ ssItem(U)| leq(U,V) ) ))),
% 29.55/9.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.55/9.25 fof(f164,axiom,(
% 29.55/9.25 (![U]: (( ~ ssList(U)| totalorderedP(U)| app(app(skaf66(U),cons(skaf64(U),skaf67(U))),cons(skaf65(U),skaf68(U))) = U ) ))),
% 29.55/9.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.55/9.25 fof(f181,axiom,(
% 29.55/9.25 (![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) ) ))),
% 29.55/9.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.55/9.25 fof(f186,negated_conjecture,(
% 29.55/9.25 ssList(sk1) ),
% 29.55/9.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.55/9.25 fof(f187,negated_conjecture,(
% 29.55/9.25 ssList(sk2) ),
% 29.55/9.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.55/9.25 fof(f191,negated_conjecture,(
% 29.55/9.25 sk1 = sk3 ),
% 29.55/9.25 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.55/9.25 fof(f193,negated_conjecture,(
% 29.55/9.26 strictorderedP(sk3) ),
% 29.55/9.26 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.55/9.26 fof(f194,negated_conjecture,(
% 29.55/9.26 ~ totalorderedP(sk1) ),
% 29.55/9.26 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 29.55/9.26 fof(f221,plain,(
% 29.55/9.26 ![X0]: (ssList(skaf68(X0)))),
% 29.55/9.26 inference(cnf_transformation,[status(thm)],[f27])).
% 29.55/9.26 fof(f222,plain,(
% 29.55/9.26 ![X0]: (ssList(skaf67(X0)))),
% 29.55/9.26 inference(cnf_transformation,[status(thm)],[f28])).
% 29.55/9.26 fof(f223,plain,(
% 29.55/9.26 ![X0]: (ssList(skaf66(X0)))),
% 29.55/9.26 inference(cnf_transformation,[status(thm)],[f29])).
% 29.55/9.26 fof(f224,plain,(
% 29.55/9.26 ![X0]: (ssItem(skaf65(X0)))),
% 29.55/9.26 inference(cnf_transformation,[status(thm)],[f30])).
% 29.55/9.26 fof(f225,plain,(
% 29.55/9.26 ![X0]: (ssItem(skaf64(X0)))),
% 29.55/9.26 inference(cnf_transformation,[status(thm)],[f31])).
% 29.55/9.26 fof(f241,plain,(
% 29.55/9.26 ![X0]: (ssItem(skaf44(X0)))),
% 29.55/9.26 inference(cnf_transformation,[status(thm)],[f47])).
% 29.55/9.26 fof(f269,plain,(
% 29.55/9.26 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 29.55/9.26 inference(cnf_transformation,[status(thm)],[f74])).
% 29.55/9.26 fof(f286,plain,(
% 29.55/9.26 ![X0]: (~leq(skaf64(X0),skaf65(X0))|~ssList(X0)|totalorderedP(X0))),
% 29.55/9.26 inference(cnf_transformation,[status(thm)],[f91])).
% 29.55/9.26 fof(f300,plain,(
% 29.55/9.26 ![X0,X1]: (~lt(X0,X1)|~ssItem(X1)|~ssItem(X0)|leq(X0,X1))),
% 29.55/9.26 inference(cnf_transformation,[status(thm)],[f103])).
% 29.55/9.26 fof(f389,plain,(
% 29.55/9.26 ![X0]: (~ssList(X0)|totalorderedP(X0)|app(app(skaf66(X0),cons(skaf64(X0),skaf67(X0))),cons(skaf65(X0),skaf68(X0)))=X0)),
% 29.55/9.26 inference(cnf_transformation,[status(thm)],[f164])).
% 29.55/9.26 fof(f415,plain,(
% 29.55/9.26 ![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))),
% 29.55/9.26 inference(miniscoping,[status(thm)],[f181])).
% 29.55/9.26 fof(f416,plain,(
% 29.55/9.26 ![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))),
% 29.55/9.26 inference(cnf_transformation,[status(thm)],[f415])).
% 29.55/9.26 fof(f425,plain,(
% 29.55/9.26 ssList(sk1)),
% 29.55/9.26 inference(cnf_transformation,[status(thm)],[f186])).
% 29.55/9.26 fof(f426,plain,(
% 29.55/9.26 ssList(sk2)),
% 29.55/9.26 inference(cnf_transformation,[status(thm)],[f187])).
% 29.55/9.26 fof(f430,plain,(
% 29.55/9.26 sk1=sk3),
% 29.55/9.26 inference(cnf_transformation,[status(thm)],[f191])).
% 29.55/9.26 fof(f432,plain,(
% 29.55/9.26 strictorderedP(sk3)),
% 29.55/9.26 inference(cnf_transformation,[status(thm)],[f193])).
% 29.55/9.26 fof(f433,plain,(
% 29.55/9.26 ~totalorderedP(sk1)),
% 29.55/9.26 inference(cnf_transformation,[status(thm)],[f194])).
% 29.55/9.26 fof(f465,plain,(
% 29.55/9.26 ![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))),
% 29.55/9.26 inference(destructive_equality_resolution,[status(thm)],[f416])).
% 29.55/9.26 fof(f472,plain,(
% 29.55/9.26 strictorderedP(sk1)),
% 29.55/9.26 inference(forward_demodulation,[status(thm)],[f430,f432])).
% 29.55/9.26 fof(f493,definition,(
% 29.55/9.26 sQ5_spl <=> (ssList(sk1))),
% 29.55/9.26 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 29.55/9.26 fof(f495,plain,(
% 29.55/9.26 ~ssList(sk1)|sQ5_spl),
% 29.55/9.26 inference(component_clause,[status(thm)],[f493])).
% 29.55/9.26 fof(f538,plain,(
% 29.55/9.26 $false|sQ5_spl),
% 29.55/9.26 inference(forward_subsumption_resolution,[status(thm)],[f495,f425])).
% 29.55/9.26 fof(f539,plain,(
% 29.55/9.26 sQ5_spl),
% 29.55/9.26 inference(contradiction_clause,[status(thm)],[f538])).
% 29.55/9.26 fof(f1376,plain,(
% 29.55/9.26 app(nil,sk2)=sk2),
% 29.55/9.26 inference(resolution,[status(thm)],[f269,f426])).
% 29.55/9.26 fof(f1678,plain,(
% 29.55/9.26 app(nil,sk1)=sk1),
% 29.55/9.26 inference(resolution,[status(thm)],[f425,f269])).
% 29.55/9.26 fof(f4667,definition,(
% 29.55/9.26 sQ524_spl <=> (totalorderedP(sk1))),
% 29.55/9.26 introduced(definition,[new_symbols(definition,[sQ524_spl])],[split_symbol_definition])).
% 29.55/9.26 fof(f4668,plain,(
% 29.55/9.26 totalorderedP(sk1)|~sQ524_spl),
% 29.55/9.26 inference(component_clause,[status(thm)],[f4667])).
% 29.55/9.26 fof(f5844,plain,(
% 29.55/9.26 $false|~sQ524_spl),
% 29.55/9.26 inference(forward_subsumption_resolution,[status(thm)],[f4668,f433])).
% 29.55/9.26 fof(f5845,plain,(
% 29.55/9.26 ~sQ524_spl),
% 29.55/9.26 inference(contradiction_clause,[status(thm)],[f5844])).
% 29.55/9.26 fof(f10178,definition,(
% 29.55/9.26 sQ1084_spl <=> (app(sk1,sk1)=app(sk1,sk1))),
% 29.55/9.26 introduced(definition,[new_symbols(definition,[sQ1084_spl])],[split_symbol_definition])).
% 29.55/9.26 fof(f10180,plain,(
% 29.55/9.26 ~app(sk1,sk1)=app(sk1,sk1)|sQ1084_spl),
% 29.55/9.26 inference(component_clause,[status(thm)],[f10178])).
% 29.55/9.26 fof(f10592,definition,(
% 29.55/9.26 sQ1102_spl <=> (app(nil,sk2)=sk2)),
% 29.55/9.26 introduced(definition,[new_symbols(definition,[sQ1102_spl])],[split_symbol_definition])).
% 29.55/9.26 fof(f10594,plain,(
% 29.55/9.26 ~app(nil,sk2)=sk2|sQ1102_spl),
% 29.55/9.26 inference(component_clause,[status(thm)],[f10592])).
% 29.55/9.26 fof(f10664,plain,(
% 29.55/9.26 totalorderedP(sk1)|app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1)))=sk1),
% 29.55/9.26 inference(resolution,[status(thm)],[f389,f425])).
% 29.55/9.26 fof(f10696,definition,(
% 29.55/9.26 sQ1104_spl <=> (app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1)))=sk1)),
% 29.55/9.26 introduced(definition,[new_symbols(definition,[sQ1104_spl])],[split_symbol_definition])).
% 29.55/9.26 fof(f10697,plain,(
% 29.55/9.26 app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1)))=sk1|~sQ1104_spl),
% 29.55/9.26 inference(component_clause,[status(thm)],[f10696])).
% 29.55/9.26 fof(f10699,plain,(
% 29.55/9.26 sQ524_spl|sQ1104_spl),
% 29.55/9.26 inference(split_clause,[status(thm)],[f10664,f4667,f10696])).
% 29.55/9.26 fof(f11145,definition,(
% 29.55/9.26 sQ1125_spl <=> (app(nil,sk1)=sk1)),
% 29.55/9.26 introduced(definition,[new_symbols(definition,[sQ1125_spl])],[split_symbol_definition])).
% 29.55/9.26 fof(f11147,plain,(
% 29.55/9.26 ~app(nil,sk1)=sk1|sQ1125_spl),
% 29.55/9.26 inference(component_clause,[status(thm)],[f11145])).
% 29.55/9.26 fof(f11279,definition,(
% 29.55/9.26 sQ1137_spl <=> (app(sk2,sk2)=app(sk2,sk2))),
% 29.55/9.26 introduced(definition,[new_symbols(definition,[sQ1137_spl])],[split_symbol_definition])).
% 29.55/9.26 fof(f11281,plain,(
% 29.55/9.26 ~app(sk2,sk2)=app(sk2,sk2)|sQ1137_spl),
% 29.55/9.26 inference(component_clause,[status(thm)],[f11279])).
% 29.55/9.26 fof(f13898,plain,(
% 29.55/9.26 ~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))|~sQ1104_spl),
% 29.55/9.26 inference(paramodulation,[status(thm)],[f10697,f465])).
% 29.55/9.26 fof(f13901,definition,(
% 29.55/9.26 sQ1279_spl <=> (ssList(skaf68(sk1)))),
% 29.55/9.26 introduced(definition,[new_symbols(definition,[sQ1279_spl])],[split_symbol_definition])).
% 29.55/9.26 fof(f13903,plain,(
% 29.55/9.26 ~ssList(skaf68(sk1))|sQ1279_spl),
% 29.55/9.26 inference(component_clause,[status(thm)],[f13901])).
% 29.55/9.26 fof(f13904,definition,(
% 29.55/9.26 sQ1280_spl <=> (ssList(skaf67(sk1)))),
% 29.55/9.26 introduced(definition,[new_symbols(definition,[sQ1280_spl])],[split_symbol_definition])).
% 29.55/9.26 fof(f13906,plain,(
% 29.55/9.26 ~ssList(skaf67(sk1))|sQ1280_spl),
% 29.55/9.26 inference(component_clause,[status(thm)],[f13904])).
% 29.55/9.26 fof(f13907,definition,(
% 29.55/9.26 sQ1281_spl <=> (ssList(skaf66(sk1)))),
% 29.55/9.26 introduced(definition,[new_symbols(definition,[sQ1281_spl])],[split_symbol_definition])).
% 29.55/9.26 fof(f13909,plain,(
% 29.55/9.26 ~ssList(skaf66(sk1))|sQ1281_spl),
% 29.55/9.26 inference(component_clause,[status(thm)],[f13907])).
% 29.55/9.26 fof(f13910,definition,(
% 29.55/9.26 sQ1282_spl <=> (ssItem(skaf65(sk1)))),
% 29.55/9.26 introduced(definition,[new_symbols(definition,[sQ1282_spl])],[split_symbol_definition])).
% 29.55/9.26 fof(f13912,plain,(
% 29.55/9.26 ~ssItem(skaf65(sk1))|sQ1282_spl),
% 29.55/9.26 inference(component_clause,[status(thm)],[f13910])).
% 29.55/9.26 fof(f13913,definition,(
% 29.55/9.26 sQ1283_spl <=> (ssItem(skaf64(sk1)))),
% 29.55/9.26 introduced(definition,[new_symbols(definition,[sQ1283_spl])],[split_symbol_definition])).
% 29.55/9.26 fof(f13915,plain,(
% 29.55/9.26 ~ssItem(skaf64(sk1))|sQ1283_spl),
% 29.55/9.26 inference(component_clause,[status(thm)],[f13913])).
% 29.55/9.26 fof(f13919,definition,(
% 29.55/9.26 sQ1285_spl <=> (leq(skaf64(sk1),skaf65(sk1)))),
% 29.55/9.26 introduced(definition,[new_symbols(definition,[sQ1285_spl])],[split_symbol_definition])).
% 29.55/9.26 fof(f13920,plain,(
% 29.55/9.26 leq(skaf64(sk1),skaf65(sk1))|~sQ1285_spl),
% 29.55/9.26 inference(component_clause,[status(thm)],[f13919])).
% 29.55/9.26 fof(f13921,plain,(
% 29.55/9.26 ~leq(skaf64(sk1),skaf65(sk1))|sQ1285_spl),
% 29.55/9.26 inference(component_clause,[status(thm)],[f13919])).
% 29.55/9.26 fof(f13923,definition,(
% 29.55/9.26 sQ1286_spl <=> (strictorderedP(app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1)))))),
% 29.55/9.26 introduced(definition,[new_symbols(definition,[sQ1286_spl])],[split_symbol_definition])).
% 29.55/9.26 fof(f13925,plain,(
% 29.55/9.26 ~strictorderedP(app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1))))|sQ1286_spl),
% 29.55/9.26 inference(component_clause,[status(thm)],[f13923])).
% 29.55/9.26 fof(f13926,definition,(
% 29.55/9.26 sQ1287_spl <=> (lt(skaf64(sk1),skaf65(sk1)))),
% 29.55/9.26 introduced(definition,[new_symbols(definition,[sQ1287_spl])],[split_symbol_definition])).
% 29.55/9.26 fof(f13929,plain,(
% 29.55/9.26 ~sQ1279_spl|~sQ1280_spl|~sQ1281_spl|~sQ1282_spl|~sQ1283_spl|~sQ1286_spl|~sQ5_spl|sQ1287_spl|~sQ1104_spl),
% 29.55/9.26 inference(split_clause,[status(thm)],[f13898,f13901,f13904,f13907,f13910,f13913,f13923,f493,f13926,f10696])).
% 29.55/9.26 fof(f13941,plain,(
% 29.55/9.26 $false|sQ1282_spl),
% 29.55/9.26 inference(forward_subsumption_resolution,[status(thm)],[f13912,f224])).
% 29.55/9.26 fof(f13942,plain,(
% 29.55/9.26 sQ1282_spl),
% 29.55/9.26 inference(contradiction_clause,[status(thm)],[f13941])).
% 29.55/9.26 fof(f13943,plain,(
% 29.55/9.26 $false|sQ1279_spl),
% 29.55/9.26 inference(forward_subsumption_resolution,[status(thm)],[f13903,f221])).
% 29.55/9.26 fof(f13944,plain,(
% 29.55/9.26 sQ1279_spl),
% 29.55/9.26 inference(contradiction_clause,[status(thm)],[f13943])).
% 29.55/9.26 fof(f13945,plain,(
% 29.55/9.26 $false|sQ1283_spl),
% 29.55/9.26 inference(forward_subsumption_resolution,[status(thm)],[f13915,f225])).
% 29.55/9.26 fof(f13946,plain,(
% 29.55/9.26 sQ1283_spl),
% 29.55/9.26 inference(contradiction_clause,[status(thm)],[f13945])).
% 29.55/9.26 fof(f13947,plain,(
% 29.55/9.26 $false|sQ1281_spl),
% 29.55/9.26 inference(forward_subsumption_resolution,[status(thm)],[f13909,f223])).
% 29.55/9.26 fof(f13948,plain,(
% 29.55/9.26 sQ1281_spl),
% 29.55/9.26 inference(contradiction_clause,[status(thm)],[f13947])).
% 29.55/9.26 fof(f13949,plain,(
% 29.55/9.26 $false|sQ1280_spl),
% 29.55/9.26 inference(forward_subsumption_resolution,[status(thm)],[f13906,f222])).
% 29.55/9.26 fof(f13950,plain,(
% 29.55/9.26 sQ1280_spl),
% 29.55/9.26 inference(contradiction_clause,[status(thm)],[f13949])).
% 29.55/9.26 fof(f13953,plain,(
% 29.55/9.26 ~strictorderedP(sk1)|~sQ1104_spl|sQ1286_spl),
% 29.55/9.26 inference(forward_demodulation,[status(thm)],[f10697,f13925])).
% 29.55/9.26 fof(f13954,plain,(
% 29.55/9.26 $false|~sQ1104_spl|sQ1286_spl),
% 29.55/9.26 inference(forward_subsumption_resolution,[status(thm)],[f13953,f472])).
% 29.55/9.26 fof(f13955,plain,(
% 29.55/9.26 ~sQ1104_spl|sQ1286_spl),
% 29.55/9.26 inference(contradiction_clause,[status(thm)],[f13954])).
% 29.55/9.26 fof(f13962,definition,(
% 29.55/9.26 sQ1291_spl <=> (ssList(skaf68(sk2)))),
% 29.55/9.26 introduced(definition,[new_symbols(definition,[sQ1291_spl])],[split_symbol_definition])).
% 29.55/9.26 fof(f13964,plain,(
% 29.55/9.26 ~ssList(skaf68(sk2))|sQ1291_spl),
% 29.55/9.26 inference(component_clause,[status(thm)],[f13962])).
% 29.55/9.26 fof(f13965,definition,(
% 29.55/9.26 sQ1292_spl <=> (ssList(skaf67(sk2)))),
% 29.55/9.26 introduced(definition,[new_symbols(definition,[sQ1292_spl])],[split_symbol_definition])).
% 29.55/9.26 fof(f13967,plain,(
% 29.55/9.26 ~ssList(skaf67(sk2))|sQ1292_spl),
% 29.55/9.26 inference(component_clause,[status(thm)],[f13965])).
% 29.55/9.26 fof(f13968,definition,(
% 29.55/9.26 sQ1293_spl <=> (ssList(skaf66(sk2)))),
% 29.55/9.26 introduced(definition,[new_symbols(definition,[sQ1293_spl])],[split_symbol_definition])).
% 29.55/9.26 fof(f13970,plain,(
% 29.55/9.26 ~ssList(skaf66(sk2))|sQ1293_spl),
% 29.55/9.26 inference(component_clause,[status(thm)],[f13968])).
% 29.55/9.26 fof(f13971,definition,(
% 29.55/9.26 sQ1294_spl <=> (ssItem(skaf65(sk2)))),
% 29.55/9.26 introduced(definition,[new_symbols(definition,[sQ1294_spl])],[split_symbol_definition])).
% 29.55/9.26 fof(f13973,plain,(
% 29.55/9.26 ~ssItem(skaf65(sk2))|sQ1294_spl),
% 29.55/9.26 inference(component_clause,[status(thm)],[f13971])).
% 29.55/9.26 fof(f13974,definition,(
% 29.55/9.26 sQ1295_spl <=> (ssItem(skaf64(sk2)))),
% 29.55/9.26 introduced(definition,[new_symbols(definition,[sQ1295_spl])],[split_symbol_definition])).
% 29.55/9.26 fof(f13976,plain,(
% 29.55/9.26 ~ssItem(skaf64(sk2))|sQ1295_spl),
% 29.55/9.26 inference(component_clause,[status(thm)],[f13974])).
% 29.55/9.26 fof(f14002,plain,(
% 29.55/9.26 $false|sQ1294_spl),
% 29.55/9.26 inference(forward_subsumption_resolution,[status(thm)],[f13973,f224])).
% 29.55/9.26 fof(f14003,plain,(
% 29.55/9.26 sQ1294_spl),
% 29.55/9.26 inference(contradiction_clause,[status(thm)],[f14002])).
% 29.55/9.26 fof(f14004,plain,(
% 29.55/9.26 $false|sQ1291_spl),
% 29.55/9.26 inference(forward_subsumption_resolution,[status(thm)],[f13964,f221])).
% 29.55/9.26 fof(f14005,plain,(
% 29.55/9.26 sQ1291_spl),
% 29.55/9.26 inference(contradiction_clause,[status(thm)],[f14004])).
% 29.55/9.26 fof(f14006,plain,(
% 29.55/9.26 $false|sQ1295_spl),
% 29.55/9.26 inference(forward_subsumption_resolution,[status(thm)],[f13976,f225])).
% 29.55/9.26 fof(f14007,plain,(
% 29.55/9.26 sQ1295_spl),
% 29.55/9.26 inference(contradiction_clause,[status(thm)],[f14006])).
% 29.55/9.26 fof(f14008,plain,(
% 29.55/9.26 $false|sQ1293_spl),
% 29.55/9.26 inference(forward_subsumption_resolution,[status(thm)],[f13970,f223])).
% 29.55/9.26 fof(f14009,plain,(
% 29.55/9.26 sQ1293_spl),
% 29.55/9.26 inference(contradiction_clause,[status(thm)],[f14008])).
% 29.55/9.26 fof(f14010,plain,(
% 29.55/9.26 $false|sQ1292_spl),
% 29.55/9.26 inference(forward_subsumption_resolution,[status(thm)],[f13967,f222])).
% 29.55/9.26 fof(f14011,plain,(
% 29.55/9.26 sQ1292_spl),
% 29.55/9.26 inference(contradiction_clause,[status(thm)],[f14010])).
% 29.55/9.26 fof(f15521,plain,(
% 29.55/9.26 ~lt(skaf64(sk1),skaf65(sk1))|~ssItem(skaf65(sk1))|~ssItem(skaf64(sk1))|sQ1285_spl),
% 29.55/9.26 inference(resolution,[status(thm)],[f13921,f300])).
% 29.55/9.26 fof(f15523,plain,(
% 29.55/9.26 ~sQ1287_spl|~sQ1282_spl|~sQ1283_spl|sQ1285_spl),
% 29.55/9.26 inference(split_clause,[status(thm)],[f15521,f13926,f13910,f13913,f13919])).
% 29.55/9.26 fof(f16734,plain,(
% 29.55/9.26 $false|sQ1137_spl),
% 29.55/9.26 inference(trivial_equality_resolution,[status(thm)],[f11281])).
% 29.55/9.26 fof(f16735,plain,(
% 29.55/9.26 sQ1137_spl),
% 29.55/9.26 inference(contradiction_clause,[status(thm)],[f16734])).
% 29.55/9.26 fof(f16736,plain,(
% 29.55/9.26 ~sk1=sk1|sQ1125_spl),
% 29.55/9.26 inference(forward_demodulation,[status(thm)],[f1678,f11147])).
% 29.55/9.26 fof(f16737,plain,(
% 29.55/9.26 $false|sQ1125_spl),
% 29.55/9.26 inference(trivial_equality_resolution,[status(thm)],[f16736])).
% 29.55/9.26 fof(f16738,plain,(
% 29.55/9.26 sQ1125_spl),
% 29.55/9.26 inference(contradiction_clause,[status(thm)],[f16737])).
% 29.55/9.26 fof(f16740,plain,(
% 29.55/9.26 ~sk2=sk2|sQ1102_spl),
% 29.55/9.26 inference(forward_demodulation,[status(thm)],[f1376,f10594])).
% 29.55/9.26 fof(f16741,plain,(
% 29.55/9.26 $false|sQ1102_spl),
% 29.55/9.26 inference(trivial_equality_resolution,[status(thm)],[f16740])).
% 29.55/9.26 fof(f16742,plain,(
% 29.55/9.26 sQ1102_spl),
% 29.55/9.26 inference(contradiction_clause,[status(thm)],[f16741])).
% 29.55/9.26 fof(f16743,plain,(
% 29.55/9.26 $false|sQ1084_spl),
% 29.55/9.26 inference(trivial_equality_resolution,[status(thm)],[f10180])).
% 29.55/9.26 fof(f16744,plain,(
% 29.55/9.26 sQ1084_spl),
% 29.55/9.26 inference(contradiction_clause,[status(thm)],[f16743])).
% 29.55/9.26 fof(f16887,definition,(
% 29.55/9.26 sQ1451_spl <=> (ssItem(skaf44(sk2)))),
% 29.55/9.26 introduced(definition,[new_symbols(definition,[sQ1451_spl])],[split_symbol_definition])).
% 29.55/9.26 fof(f16889,plain,(
% 29.55/9.26 ~ssItem(skaf44(sk2))|sQ1451_spl),
% 29.55/9.26 inference(component_clause,[status(thm)],[f16887])).
% 29.55/9.26 fof(f16961,plain,(
% 29.55/9.26 $false|sQ1451_spl),
% 29.55/9.26 inference(forward_subsumption_resolution,[status(thm)],[f16889,f241])).
% 29.55/9.26 fof(f16962,plain,(
% 29.55/9.26 sQ1451_spl),
% 29.55/9.26 inference(contradiction_clause,[status(thm)],[f16961])).
% 29.55/9.26 fof(f17152,plain,(
% 29.55/9.26 ~ssList(sk1)|totalorderedP(sk1)|~sQ1285_spl),
% 29.55/9.26 inference(resolution,[status(thm)],[f286,f13920])).
% 29.55/9.26 fof(f17155,plain,(
% 29.55/9.26 ~sQ5_spl|sQ524_spl|~sQ1285_spl),
% 29.55/9.26 inference(split_clause,[status(thm)],[f17152,f493,f4667,f13919])).
% 29.55/9.26 fof(f17158,plain,(
% 29.55/9.26 $false),
% 29.55/9.27 inference(sat_refutation,[status(thm)],[f539,f5845,f10699,f13929,f13942,f13944,f13946,f13948,f13950,f13955,f14003,f14005,f14007,f14009,f14011,f15523,f16735,f16738,f16742,f16744,f16962,f17155])).
% 29.55/9.27 % SZS output end CNFRefutation for theBenchmark.p
% 29.55/9.29 % Elapsed time: 3.831628 seconds
% 29.55/9.29 % CPU time: 30.054698 seconds
% 29.55/9.29 % Total memory used: 338.770 MB
% 29.55/9.29 % Net memory used: 325.110 MB
%------------------------------------------------------------------------------