%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC340-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 : n011.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:12 PM UTC 2026
% Result : Unsatisfiable 36.75s 10.14s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWC340-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.16/5.42 % Computer : n011.cluster.edu
% 0.16/5.42 % Model : x86_64 x86_64
% 0.16/5.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/5.42 % Memory : 8046.5625MB
% 0.16/5.42 % OS : Linux 6.8.0-71-generic
% 0.16/5.42 % CPULimit : 300
% 0.16/5.42 % WCLimit : 300
% 0.16/5.42 % DateTime : Mon Sep 21 08:17:15 UTC 2026
% 0.16/5.42 % CPUTime :
% 0.16/5.45 % Drodi V4.1.1
% 36.75/10.14 % Refutation found
% 36.75/10.14 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 36.75/10.14 % SZS output start CNFRefutation for theBenchmark
% 36.75/10.14 fof(f9,axiom,(
% 36.75/10.14 ssItem(skac3) ),
% 36.75/10.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.14 fof(f10,axiom,(
% 36.75/10.14 ssItem(skac2) ),
% 36.75/10.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.14 fof(f27,axiom,(
% 36.75/10.14 (![U]: (ssList(skaf68(U)) ))),
% 36.75/10.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.14 fof(f28,axiom,(
% 36.75/10.14 (![U]: (ssList(skaf67(U)) ))),
% 36.75/10.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.14 fof(f29,axiom,(
% 36.75/10.14 (![U]: (ssList(skaf66(U)) ))),
% 36.75/10.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.14 fof(f30,axiom,(
% 36.75/10.14 (![U]: (ssItem(skaf65(U)) ))),
% 36.75/10.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.14 fof(f31,axiom,(
% 36.75/10.14 (![U]: (ssItem(skaf64(U)) ))),
% 36.75/10.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.14 fof(f32,axiom,(
% 36.75/10.14 (![U]: (ssList(skaf63(U)) ))),
% 36.75/10.14 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.14 fof(f35,axiom,(
% 36.75/10.14 (![U]: (ssItem(skaf60(U)) ))),
% 36.75/10.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.15 fof(f37,axiom,(
% 36.75/10.15 (![U]: (ssList(skaf58(U)) ))),
% 36.75/10.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.15 fof(f38,axiom,(
% 36.75/10.15 (![U]: (ssList(skaf57(U)) ))),
% 36.75/10.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.15 fof(f39,axiom,(
% 36.75/10.15 (![U]: (ssList(skaf56(U)) ))),
% 36.75/10.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.15 fof(f40,axiom,(
% 36.75/10.15 (![U]: (ssItem(skaf55(U)) ))),
% 36.75/10.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.15 fof(f41,axiom,(
% 36.75/10.15 (![U]: (ssItem(skaf54(U)) ))),
% 36.75/10.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.15 fof(f47,axiom,(
% 36.75/10.15 (![U]: (ssItem(skaf44(U)) ))),
% 36.75/10.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.15 fof(f50,axiom,(
% 36.75/10.15 (![U,V]: (ssList(skaf46(U,V)) ))),
% 36.75/10.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.15 fof(f51,axiom,(
% 36.75/10.15 (![U,V]: (ssList(skaf45(U,V)) ))),
% 36.75/10.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.15 fof(f85,axiom,(
% 36.75/10.15 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| ssList(app(V,U)) ) ))),
% 36.75/10.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.15 fof(f91,axiom,(
% 36.75/10.15 (![U]: (( ~ leq(skaf64(U),skaf65(U))| ~ ssList(U)| totalorderedP(U) ) ))),
% 36.75/10.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.15 fof(f103,axiom,(
% 36.75/10.15 (![U,V]: (( ~ lt(U,V)| ~ ssItem(V)| ~ ssItem(U)| leq(U,V) ) ))),
% 36.75/10.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.15 fof(f164,axiom,(
% 36.75/10.15 (![U]: (( ~ ssList(U)| totalorderedP(U)| app(app(skaf66(U),cons(skaf64(U),skaf67(U))),cons(skaf65(U),skaf68(U))) = U ) ))),
% 36.75/10.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.15 fof(f181,axiom,(
% 36.75/10.15 (![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) ) ))),
% 36.75/10.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.15 fof(f186,negated_conjecture,(
% 36.75/10.15 ssList(sk1) ),
% 36.75/10.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.15 fof(f187,negated_conjecture,(
% 36.75/10.15 ssList(sk2) ),
% 36.75/10.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.15 fof(f190,negated_conjecture,(
% 36.75/10.15 sk2 = sk4 ),
% 36.75/10.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.15 fof(f191,negated_conjecture,(
% 36.75/10.15 sk1 = sk3 ),
% 36.75/10.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.15 fof(f192,negated_conjecture,(
% 36.75/10.15 segmentP(sk4,sk3) ),
% 36.75/10.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.15 fof(f193,negated_conjecture,(
% 36.75/10.15 strictorderedP(sk3) ),
% 36.75/10.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.15 fof(f194,negated_conjecture,(
% 36.75/10.15 ( ~ segmentP(sk2,sk1)| ~ totalorderedP(sk1) ) ),
% 36.75/10.15 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 36.75/10.15 fof(f203,plain,(
% 36.75/10.15 ssItem(skac3)),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f9])).
% 36.75/10.15 fof(f204,plain,(
% 36.75/10.15 ssItem(skac2)),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f10])).
% 36.75/10.15 fof(f221,plain,(
% 36.75/10.15 ![X0]: (ssList(skaf68(X0)))),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f27])).
% 36.75/10.15 fof(f222,plain,(
% 36.75/10.15 ![X0]: (ssList(skaf67(X0)))),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f28])).
% 36.75/10.15 fof(f223,plain,(
% 36.75/10.15 ![X0]: (ssList(skaf66(X0)))),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f29])).
% 36.75/10.15 fof(f224,plain,(
% 36.75/10.15 ![X0]: (ssItem(skaf65(X0)))),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f30])).
% 36.75/10.15 fof(f225,plain,(
% 36.75/10.15 ![X0]: (ssItem(skaf64(X0)))),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f31])).
% 36.75/10.15 fof(f226,plain,(
% 36.75/10.15 ![X0]: (ssList(skaf63(X0)))),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f32])).
% 36.75/10.15 fof(f229,plain,(
% 36.75/10.15 ![X0]: (ssItem(skaf60(X0)))),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f35])).
% 36.75/10.15 fof(f231,plain,(
% 36.75/10.15 ![X0]: (ssList(skaf58(X0)))),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f37])).
% 36.75/10.15 fof(f232,plain,(
% 36.75/10.15 ![X0]: (ssList(skaf57(X0)))),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f38])).
% 36.75/10.15 fof(f233,plain,(
% 36.75/10.15 ![X0]: (ssList(skaf56(X0)))),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f39])).
% 36.75/10.15 fof(f234,plain,(
% 36.75/10.15 ![X0]: (ssItem(skaf55(X0)))),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f40])).
% 36.75/10.15 fof(f235,plain,(
% 36.75/10.15 ![X0]: (ssItem(skaf54(X0)))),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f41])).
% 36.75/10.15 fof(f241,plain,(
% 36.75/10.15 ![X0]: (ssItem(skaf44(X0)))),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f47])).
% 36.75/10.15 fof(f244,plain,(
% 36.75/10.15 ![X0,X1]: (ssList(skaf46(X0,X1)))),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f50])).
% 36.75/10.15 fof(f245,plain,(
% 36.75/10.15 ![X0,X1]: (ssList(skaf45(X0,X1)))),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f51])).
% 36.75/10.15 fof(f280,plain,(
% 36.75/10.15 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X1,X0)))),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f85])).
% 36.75/10.15 fof(f286,plain,(
% 36.75/10.15 ![X0]: (~leq(skaf64(X0),skaf65(X0))|~ssList(X0)|totalorderedP(X0))),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f91])).
% 36.75/10.15 fof(f300,plain,(
% 36.75/10.15 ![X0,X1]: (~lt(X0,X1)|~ssItem(X1)|~ssItem(X0)|leq(X0,X1))),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f103])).
% 36.75/10.15 fof(f389,plain,(
% 36.75/10.15 ![X0]: (~ssList(X0)|totalorderedP(X0)|app(app(skaf66(X0),cons(skaf64(X0),skaf67(X0))),cons(skaf65(X0),skaf68(X0)))=X0)),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f164])).
% 36.75/10.15 fof(f415,plain,(
% 36.75/10.15 ![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))),
% 36.75/10.15 inference(miniscoping,[status(thm)],[f181])).
% 36.75/10.15 fof(f416,plain,(
% 36.75/10.15 ![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))),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f415])).
% 36.75/10.15 fof(f425,plain,(
% 36.75/10.15 ssList(sk1)),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f186])).
% 36.75/10.15 fof(f426,plain,(
% 36.75/10.15 ssList(sk2)),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f187])).
% 36.75/10.15 fof(f429,plain,(
% 36.75/10.15 sk2=sk4),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f190])).
% 36.75/10.15 fof(f430,plain,(
% 36.75/10.15 sk1=sk3),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f191])).
% 36.75/10.15 fof(f431,plain,(
% 36.75/10.15 segmentP(sk4,sk3)),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f192])).
% 36.75/10.15 fof(f432,plain,(
% 36.75/10.15 strictorderedP(sk3)),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f193])).
% 36.75/10.15 fof(f433,plain,(
% 36.75/10.15 ~segmentP(sk2,sk1)|~totalorderedP(sk1)),
% 36.75/10.15 inference(cnf_transformation,[status(thm)],[f194])).
% 36.75/10.15 fof(f441,definition,(
% 36.75/10.15 sQ2_spl <=> (segmentP(sk2,sk1))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f443,plain,(
% 36.75/10.15 ~segmentP(sk2,sk1)|sQ2_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f441])).
% 36.75/10.15 fof(f444,definition,(
% 36.75/10.15 sQ3_spl <=> (totalorderedP(sk1))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f447,plain,(
% 36.75/10.15 ~sQ2_spl|~sQ3_spl),
% 36.75/10.15 inference(split_clause,[status(thm)],[f433,f441,f444])).
% 36.75/10.15 fof(f472,plain,(
% 36.75/10.15 ![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))),
% 36.75/10.15 inference(destructive_equality_resolution,[status(thm)],[f416])).
% 36.75/10.15 fof(f479,plain,(
% 36.75/10.15 strictorderedP(sk1)),
% 36.75/10.15 inference(forward_demodulation,[status(thm)],[f430,f432])).
% 36.75/10.15 fof(f480,plain,(
% 36.75/10.15 segmentP(sk2,sk3)),
% 36.75/10.15 inference(forward_demodulation,[status(thm)],[f429,f431])).
% 36.75/10.15 fof(f481,plain,(
% 36.75/10.15 segmentP(sk2,sk1)),
% 36.75/10.15 inference(forward_demodulation,[status(thm)],[f430,f480])).
% 36.75/10.15 fof(f482,plain,(
% 36.75/10.15 $false|sQ2_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f443,f481])).
% 36.75/10.15 fof(f483,plain,(
% 36.75/10.15 sQ2_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f482])).
% 36.75/10.15 fof(f502,definition,(
% 36.75/10.15 sQ7_spl <=> (ssList(sk1))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f504,plain,(
% 36.75/10.15 ~ssList(sk1)|sQ7_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f502])).
% 36.75/10.15 fof(f547,plain,(
% 36.75/10.15 $false|sQ7_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f504,f425])).
% 36.75/10.15 fof(f548,plain,(
% 36.75/10.15 sQ7_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f547])).
% 36.75/10.15 fof(f7410,definition,(
% 36.75/10.15 sQ741_spl <=> (ssItem(skac2))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ741_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f7412,plain,(
% 36.75/10.15 ~ssItem(skac2)|sQ741_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f7410])).
% 36.75/10.15 fof(f7863,definition,(
% 36.75/10.15 sQ808_spl <=> (ssItem(skac3))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ808_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f7865,plain,(
% 36.75/10.15 ~ssItem(skac3)|sQ808_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f7863])).
% 36.75/10.15 fof(f9170,plain,(
% 36.75/10.15 totalorderedP(sk1)|app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1)))=sk1),
% 36.75/10.15 inference(resolution,[status(thm)],[f389,f425])).
% 36.75/10.15 fof(f9191,definition,(
% 36.75/10.15 sQ921_spl <=> (app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1)))=sk1)),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ921_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f9192,plain,(
% 36.75/10.15 app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1)))=sk1|~sQ921_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f9191])).
% 36.75/10.15 fof(f9194,plain,(
% 36.75/10.15 sQ3_spl|sQ921_spl),
% 36.75/10.15 inference(split_clause,[status(thm)],[f9170,f444,f9191])).
% 36.75/10.15 fof(f10740,definition,(
% 36.75/10.15 ![X0]: (sQ1049_spl <=> (~app(X0,sk1)=app(X0,sk1)|~ssList(X0)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1049_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f10741,plain,(
% 36.75/10.15 ![X0]: (~app(X0,sk1)=app(X0,sk1)|~ssList(X0)|~sQ1049_spl)),
% 36.75/10.15 inference(component_clause,[status(thm)],[f10740])).
% 36.75/10.15 fof(f12238,definition,(
% 36.75/10.15 sQ1064_spl <=> (app(sk1,sk1)=app(sk1,sk1))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1064_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f12240,plain,(
% 36.75/10.15 ~app(sk1,sk1)=app(sk1,sk1)|sQ1064_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f12238])).
% 36.75/10.15 fof(f13359,definition,(
% 36.75/10.15 sQ1073_spl <=> (app(sk2,sk2)=app(sk2,sk2))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1073_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f13361,plain,(
% 36.75/10.15 ~app(sk2,sk2)=app(sk2,sk2)|sQ1073_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f13359])).
% 36.75/10.15 fof(f14768,definition,(
% 36.75/10.15 sQ1124_spl <=> (ssList(skaf68(sk1)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1124_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f14770,plain,(
% 36.75/10.15 ~ssList(skaf68(sk1))|sQ1124_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f14768])).
% 36.75/10.15 fof(f14771,definition,(
% 36.75/10.15 sQ1125_spl <=> (ssList(skaf67(sk1)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1125_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f14773,plain,(
% 36.75/10.15 ~ssList(skaf67(sk1))|sQ1125_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f14771])).
% 36.75/10.15 fof(f14774,definition,(
% 36.75/10.15 sQ1126_spl <=> (ssList(skaf66(sk1)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1126_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f14776,plain,(
% 36.75/10.15 ~ssList(skaf66(sk1))|sQ1126_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f14774])).
% 36.75/10.15 fof(f14780,definition,(
% 36.75/10.15 sQ1128_spl <=> (leq(skaf64(sk1),skaf65(sk1)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1128_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f14781,plain,(
% 36.75/10.15 leq(skaf64(sk1),skaf65(sk1))|~sQ1128_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f14780])).
% 36.75/10.15 fof(f14784,definition,(
% 36.75/10.15 sQ1129_spl <=> (lt(skaf64(sk1),skaf65(sk1)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1129_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f14785,plain,(
% 36.75/10.15 lt(skaf64(sk1),skaf65(sk1))|~sQ1129_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f14784])).
% 36.75/10.15 fof(f14834,plain,(
% 36.75/10.15 $false|sQ1124_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f14770,f221])).
% 36.75/10.15 fof(f14835,plain,(
% 36.75/10.15 sQ1124_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f14834])).
% 36.75/10.15 fof(f14836,plain,(
% 36.75/10.15 $false|sQ1126_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f14776,f223])).
% 36.75/10.15 fof(f14837,plain,(
% 36.75/10.15 sQ1126_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f14836])).
% 36.75/10.15 fof(f14843,plain,(
% 36.75/10.15 $false|sQ1125_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f14773,f222])).
% 36.75/10.15 fof(f14844,plain,(
% 36.75/10.15 sQ1125_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f14843])).
% 36.75/10.15 fof(f15402,definition,(
% 36.75/10.15 sQ1166_spl <=> (ssItem(skaf65(sk1)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1166_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f15404,plain,(
% 36.75/10.15 ~ssItem(skaf65(sk1))|sQ1166_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f15402])).
% 36.75/10.15 fof(f15419,plain,(
% 36.75/10.15 $false|sQ1166_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f15404,f224])).
% 36.75/10.15 fof(f15420,plain,(
% 36.75/10.15 sQ1166_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f15419])).
% 36.75/10.15 fof(f15451,plain,(
% 36.75/10.15 ![X0,X1,X2,X3,X4]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssItem(X3)|~strictorderedP(app(app(X2,cons(skaf64(X4),X1)),cons(X3,X0)))|~ssList(app(app(X2,cons(skaf64(X4),X1)),cons(X3,X0)))|lt(skaf64(X4),X3))),
% 36.75/10.15 inference(resolution,[status(thm)],[f225,f472])).
% 36.75/10.15 fof(f15737,definition,(
% 36.75/10.15 sQ1171_spl <=> (ssItem(skaf64(sk2)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1171_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f15739,plain,(
% 36.75/10.15 ~ssItem(skaf64(sk2))|sQ1171_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f15737])).
% 36.75/10.15 fof(f15744,definition,(
% 36.75/10.15 sQ1173_spl <=> (ssItem(skaf64(sk1)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1173_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f15746,plain,(
% 36.75/10.15 ~ssItem(skaf64(sk1))|sQ1173_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f15744])).
% 36.75/10.15 fof(f15815,plain,(
% 36.75/10.15 $false|sQ1173_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f15746,f225])).
% 36.75/10.15 fof(f15816,plain,(
% 36.75/10.15 sQ1173_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f15815])).
% 36.75/10.15 fof(f15817,plain,(
% 36.75/10.15 $false|sQ1171_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f15739,f225])).
% 36.75/10.15 fof(f15818,plain,(
% 36.75/10.15 sQ1171_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f15817])).
% 36.75/10.15 fof(f15905,plain,(
% 36.75/10.15 ~ssList(sk1)|totalorderedP(sk1)|~sQ1128_spl),
% 36.75/10.15 inference(resolution,[status(thm)],[f14781,f286])).
% 36.75/10.15 fof(f15907,plain,(
% 36.75/10.15 ~sQ7_spl|sQ3_spl|~sQ1128_spl),
% 36.75/10.15 inference(split_clause,[status(thm)],[f15905,f502,f444,f14780])).
% 36.75/10.15 fof(f15923,definition,(
% 36.75/10.15 sQ1204_spl <=> (ssList(skaf58(sk1)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1204_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f15925,plain,(
% 36.75/10.15 ~ssList(skaf58(sk1))|sQ1204_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f15923])).
% 36.75/10.15 fof(f15926,definition,(
% 36.75/10.15 sQ1205_spl <=> (ssList(skaf57(sk1)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1205_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f15928,plain,(
% 36.75/10.15 ~ssList(skaf57(sk1))|sQ1205_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f15926])).
% 36.75/10.15 fof(f15929,definition,(
% 36.75/10.15 sQ1206_spl <=> (ssList(skaf56(sk1)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1206_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f15931,plain,(
% 36.75/10.15 ~ssList(skaf56(sk1))|sQ1206_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f15929])).
% 36.75/10.15 fof(f15932,definition,(
% 36.75/10.15 sQ1207_spl <=> (ssItem(skaf55(sk1)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1207_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f15934,plain,(
% 36.75/10.15 ~ssItem(skaf55(sk1))|sQ1207_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f15932])).
% 36.75/10.15 fof(f15935,definition,(
% 36.75/10.15 sQ1208_spl <=> (ssItem(skaf54(sk1)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1208_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f15937,plain,(
% 36.75/10.15 ~ssItem(skaf54(sk1))|sQ1208_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f15935])).
% 36.75/10.15 fof(f15991,plain,(
% 36.75/10.15 $false|sQ1207_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f15934,f234])).
% 36.75/10.15 fof(f15992,plain,(
% 36.75/10.15 sQ1207_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f15991])).
% 36.75/10.15 fof(f15993,plain,(
% 36.75/10.15 $false|sQ1204_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f15925,f231])).
% 36.75/10.15 fof(f15994,plain,(
% 36.75/10.15 sQ1204_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f15993])).
% 36.75/10.15 fof(f15995,plain,(
% 36.75/10.15 $false|sQ1206_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f15931,f233])).
% 36.75/10.15 fof(f15996,plain,(
% 36.75/10.15 sQ1206_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f15995])).
% 36.75/10.15 fof(f16000,plain,(
% 36.75/10.15 $false|sQ1208_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f15937,f235])).
% 36.75/10.15 fof(f16001,plain,(
% 36.75/10.15 sQ1208_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f16000])).
% 36.75/10.15 fof(f16002,plain,(
% 36.75/10.15 $false|sQ1205_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f15928,f232])).
% 36.75/10.15 fof(f16003,plain,(
% 36.75/10.15 sQ1205_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f16002])).
% 36.75/10.15 fof(f16129,plain,(
% 36.75/10.15 $false|sQ1073_spl),
% 36.75/10.15 inference(trivial_equality_resolution,[status(thm)],[f13361])).
% 36.75/10.15 fof(f16130,plain,(
% 36.75/10.15 sQ1073_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f16129])).
% 36.75/10.15 fof(f16131,plain,(
% 36.75/10.15 $false|sQ1064_spl),
% 36.75/10.15 inference(trivial_equality_resolution,[status(thm)],[f12240])).
% 36.75/10.15 fof(f16132,plain,(
% 36.75/10.15 sQ1064_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f16131])).
% 36.75/10.15 fof(f16134,plain,(
% 36.75/10.15 ![X0]: (~ssList(X0)|~sQ1049_spl)),
% 36.75/10.15 inference(trivial_equality_resolution,[status(thm)],[f10741])).
% 36.75/10.15 fof(f16136,plain,(
% 36.75/10.15 $false|sQ808_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f7865,f203])).
% 36.75/10.15 fof(f16137,plain,(
% 36.75/10.15 sQ808_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f16136])).
% 36.75/10.15 fof(f16138,plain,(
% 36.75/10.15 $false|sQ741_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f7412,f204])).
% 36.75/10.15 fof(f16139,plain,(
% 36.75/10.15 sQ741_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f16138])).
% 36.75/10.15 fof(f16176,plain,(
% 36.75/10.15 $false|~sQ1049_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f425,f16134])).
% 36.75/10.15 fof(f16177,plain,(
% 36.75/10.15 ~sQ1049_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f16176])).
% 36.75/10.15 fof(f16336,definition,(
% 36.75/10.15 sQ1237_spl <=> (ssList(skaf63(sk1)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1237_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f16338,plain,(
% 36.75/10.15 ~ssList(skaf63(sk1))|sQ1237_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f16336])).
% 36.75/10.15 fof(f16342,definition,(
% 36.75/10.15 sQ1239_spl <=> (ssItem(skaf60(sk1)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1239_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f16344,plain,(
% 36.75/10.15 ~ssItem(skaf60(sk1))|sQ1239_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f16342])).
% 36.75/10.15 fof(f16349,plain,(
% 36.75/10.15 $false|sQ1239_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f16344,f229])).
% 36.75/10.15 fof(f16350,plain,(
% 36.75/10.15 sQ1239_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f16349])).
% 36.75/10.15 fof(f16353,plain,(
% 36.75/10.15 $false|sQ1237_spl),
% 36.75/10.15 inference(backward_subsumption_resolution,[status(thm)],[f16338,f226])).
% 36.75/10.15 fof(f16363,plain,(
% 36.75/10.15 sQ1237_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f16353])).
% 36.75/10.15 fof(f16495,definition,(
% 36.75/10.15 sQ1245_spl <=> (ssList(skaf58(sk2)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1245_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f16497,plain,(
% 36.75/10.15 ~ssList(skaf58(sk2))|sQ1245_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f16495])).
% 36.75/10.15 fof(f16501,definition,(
% 36.75/10.15 sQ1247_spl <=> (ssItem(skaf55(sk2)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1247_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f16503,plain,(
% 36.75/10.15 ~ssItem(skaf55(sk2))|sQ1247_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f16501])).
% 36.75/10.15 fof(f16509,plain,(
% 36.75/10.15 $false|sQ1247_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f16503,f234])).
% 36.75/10.15 fof(f16510,plain,(
% 36.75/10.15 sQ1247_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f16509])).
% 36.75/10.15 fof(f16511,plain,(
% 36.75/10.15 $false|sQ1245_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f16497,f231])).
% 36.75/10.15 fof(f16512,plain,(
% 36.75/10.15 sQ1245_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f16511])).
% 36.75/10.15 fof(f16658,definition,(
% 36.75/10.15 sQ1254_spl <=> (ssList(skaf63(sk2)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1254_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f16660,plain,(
% 36.75/10.15 ~ssList(skaf63(sk2))|sQ1254_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f16658])).
% 36.75/10.15 fof(f16664,definition,(
% 36.75/10.15 sQ1256_spl <=> (ssItem(skaf60(sk2)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1256_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f16666,plain,(
% 36.75/10.15 ~ssItem(skaf60(sk2))|sQ1256_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f16664])).
% 36.75/10.15 fof(f16672,plain,(
% 36.75/10.15 $false|sQ1256_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f16666,f229])).
% 36.75/10.15 fof(f16673,plain,(
% 36.75/10.15 sQ1256_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f16672])).
% 36.75/10.15 fof(f16674,plain,(
% 36.75/10.15 $false|sQ1254_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f16660,f226])).
% 36.75/10.15 fof(f16675,plain,(
% 36.75/10.15 sQ1254_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f16674])).
% 36.75/10.15 fof(f16682,plain,(
% 36.75/10.15 ~ssItem(skaf65(sk1))|~ssItem(skaf64(sk1))|leq(skaf64(sk1),skaf65(sk1))|~sQ1129_spl),
% 36.75/10.15 inference(resolution,[status(thm)],[f14785,f300])).
% 36.75/10.15 fof(f16687,plain,(
% 36.75/10.15 ~sQ1166_spl|~sQ1173_spl|sQ1128_spl|~sQ1129_spl),
% 36.75/10.15 inference(split_clause,[status(thm)],[f16682,f15402,f15744,f14780,f14784])).
% 36.75/10.15 fof(f18133,definition,(
% 36.75/10.15 ![X2]: (sQ1343_spl <=> (~ssItem(X2)|~ssItem(X2)|~ssItem(X2)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1343_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f18134,plain,(
% 36.75/10.15 ![X0]: (~ssItem(X0)|~ssItem(X0)|~ssItem(X0)|~sQ1343_spl)),
% 36.75/10.15 inference(component_clause,[status(thm)],[f18133])).
% 36.75/10.15 fof(f18143,plain,(
% 36.75/10.15 ![X0]: (~ssItem(X0)|~sQ1343_spl)),
% 36.75/10.15 inference(duplicate_literals_removal,[status(thm)],[f18134])).
% 36.75/10.15 fof(f18206,plain,(
% 36.75/10.15 $false|~sQ1343_spl),
% 36.75/10.15 inference(backward_subsumption_resolution,[status(thm)],[f241,f18143])).
% 36.75/10.15 fof(f18226,plain,(
% 36.75/10.15 ~sQ1343_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f18206])).
% 36.75/10.15 fof(f18652,definition,(
% 36.75/10.15 sQ1352_spl <=> (ssItem(skaf44(sk2)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1352_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f18654,plain,(
% 36.75/10.15 ~ssItem(skaf44(sk2))|sQ1352_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f18652])).
% 36.75/10.15 fof(f18667,plain,(
% 36.75/10.15 $false|sQ1352_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f18654,f241])).
% 36.75/10.15 fof(f18668,plain,(
% 36.75/10.15 sQ1352_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f18667])).
% 36.75/10.15 fof(f19338,definition,(
% 36.75/10.15 sQ1394_spl <=> (ssList(app(sk1,sk1)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1394_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f19340,plain,(
% 36.75/10.15 ~ssList(app(sk1,sk1))|sQ1394_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f19338])).
% 36.75/10.15 fof(f19580,definition,(
% 36.75/10.15 sQ1425_spl <=> (ssList(app(sk1,sk2)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1425_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f19582,plain,(
% 36.75/10.15 ~ssList(app(sk1,sk2))|sQ1425_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f19580])).
% 36.75/10.15 fof(f19789,definition,(
% 36.75/10.15 sQ1452_spl <=> (ssList(skaf46(sk2,sk2)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1452_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f19791,plain,(
% 36.75/10.15 ~ssList(skaf46(sk2,sk2))|sQ1452_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f19789])).
% 36.75/10.15 fof(f19794,plain,(
% 36.75/10.15 $false|sQ1452_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f19791,f244])).
% 36.75/10.15 fof(f19795,plain,(
% 36.75/10.15 sQ1452_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f19794])).
% 36.75/10.15 fof(f19839,definition,(
% 36.75/10.15 sQ1454_spl <=> (ssList(skaf46(sk1,sk1)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1454_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f19841,plain,(
% 36.75/10.15 ~ssList(skaf46(sk1,sk1))|sQ1454_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f19839])).
% 36.75/10.15 fof(f19843,plain,(
% 36.75/10.15 $false|sQ1454_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f19841,f244])).
% 36.75/10.15 fof(f19844,plain,(
% 36.75/10.15 sQ1454_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f19843])).
% 36.75/10.15 fof(f20048,definition,(
% 36.75/10.15 sQ1474_spl <=> (ssList(skaf45(sk2,sk2)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1474_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f20050,plain,(
% 36.75/10.15 ~ssList(skaf45(sk2,sk2))|sQ1474_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f20048])).
% 36.75/10.15 fof(f20053,plain,(
% 36.75/10.15 $false|sQ1474_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f20050,f245])).
% 36.75/10.15 fof(f20054,plain,(
% 36.75/10.15 sQ1474_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f20053])).
% 36.75/10.15 fof(f20074,definition,(
% 36.75/10.15 sQ1478_spl <=> (ssList(skaf45(sk1,sk1)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1478_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f20076,plain,(
% 36.75/10.15 ~ssList(skaf45(sk1,sk1))|sQ1478_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f20074])).
% 36.75/10.15 fof(f20079,plain,(
% 36.75/10.15 $false|sQ1478_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f20076,f245])).
% 36.75/10.15 fof(f20080,plain,(
% 36.75/10.15 sQ1478_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f20079])).
% 36.75/10.15 fof(f20112,definition,(
% 36.75/10.15 sQ1480_spl <=> (ssList(app(sk2,sk1)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1480_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f20114,plain,(
% 36.75/10.15 ~ssList(app(sk2,sk1))|sQ1480_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f20112])).
% 36.75/10.15 fof(f20513,definition,(
% 36.75/10.15 sQ1529_spl <=> (ssList(app(sk2,sk2)))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ1529_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f20515,plain,(
% 36.75/10.15 ~ssList(app(sk2,sk2))|sQ1529_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f20513])).
% 36.75/10.15 fof(f20860,plain,(
% 36.75/10.15 ![X0]: (~ssList(X0)|ssList(app(sk1,X0)))),
% 36.75/10.15 inference(resolution,[status(thm)],[f280,f425])).
% 36.75/10.15 fof(f20861,plain,(
% 36.75/10.15 ![X0]: (~ssList(X0)|ssList(app(sk2,X0)))),
% 36.75/10.15 inference(resolution,[status(thm)],[f280,f426])).
% 36.75/10.15 fof(f20969,plain,(
% 36.75/10.15 ssList(app(sk1,sk1))),
% 36.75/10.15 inference(resolution,[status(thm)],[f20860,f425])).
% 36.75/10.15 fof(f20970,plain,(
% 36.75/10.15 ssList(app(sk1,sk2))),
% 36.75/10.15 inference(resolution,[status(thm)],[f20860,f426])).
% 36.75/10.15 fof(f20972,plain,(
% 36.75/10.15 $false|sQ1394_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f20969,f19340])).
% 36.75/10.15 fof(f20973,plain,(
% 36.75/10.15 sQ1394_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f20972])).
% 36.75/10.15 fof(f20974,plain,(
% 36.75/10.15 $false|sQ1425_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f20970,f19582])).
% 36.75/10.15 fof(f20975,plain,(
% 36.75/10.15 sQ1425_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f20974])).
% 36.75/10.15 fof(f24171,plain,(
% 36.75/10.15 ssList(app(sk2,sk1))),
% 36.75/10.15 inference(resolution,[status(thm)],[f20861,f425])).
% 36.75/10.15 fof(f24172,plain,(
% 36.75/10.15 ssList(app(sk2,sk2))),
% 36.75/10.15 inference(resolution,[status(thm)],[f20861,f426])).
% 36.75/10.15 fof(f24174,plain,(
% 36.75/10.15 $false|sQ1480_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f24171,f20114])).
% 36.75/10.15 fof(f24175,plain,(
% 36.75/10.15 sQ1480_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f24174])).
% 36.75/10.15 fof(f24176,plain,(
% 36.75/10.15 $false|sQ1529_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f24172,f20515])).
% 36.75/10.15 fof(f24177,plain,(
% 36.75/10.15 sQ1529_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f24176])).
% 36.75/10.15 fof(f27798,plain,(
% 36.75/10.15 ~ssList(skaf68(sk1))|~ssList(skaf67(sk1))|~ssList(skaf66(sk1))|~ssItem(skaf65(sk1))|~strictorderedP(app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1))))|~ssList(sk1)|lt(skaf64(sk1),skaf65(sk1))|~sQ921_spl),
% 36.75/10.15 inference(paramodulation,[status(thm)],[f9192,f15451])).
% 36.75/10.15 fof(f27816,definition,(
% 36.75/10.15 sQ2002_spl <=> (strictorderedP(app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1)))))),
% 36.75/10.15 introduced(definition,[new_symbols(definition,[sQ2002_spl])],[split_symbol_definition])).
% 36.75/10.15 fof(f27818,plain,(
% 36.75/10.15 ~strictorderedP(app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1))))|sQ2002_spl),
% 36.75/10.15 inference(component_clause,[status(thm)],[f27816])).
% 36.75/10.15 fof(f27819,plain,(
% 36.75/10.15 ~sQ1124_spl|~sQ1125_spl|~sQ1126_spl|~sQ1166_spl|~sQ2002_spl|~sQ7_spl|sQ1129_spl|~sQ921_spl),
% 36.75/10.15 inference(split_clause,[status(thm)],[f27798,f14768,f14771,f14774,f15402,f27816,f502,f14784,f9191])).
% 36.75/10.15 fof(f27873,plain,(
% 36.75/10.15 ~strictorderedP(sk1)|~sQ921_spl|sQ2002_spl),
% 36.75/10.15 inference(forward_demodulation,[status(thm)],[f9192,f27818])).
% 36.75/10.15 fof(f27874,plain,(
% 36.75/10.15 $false|~sQ921_spl|sQ2002_spl),
% 36.75/10.15 inference(forward_subsumption_resolution,[status(thm)],[f27873,f479])).
% 36.75/10.15 fof(f27875,plain,(
% 36.75/10.15 ~sQ921_spl|sQ2002_spl),
% 36.75/10.15 inference(contradiction_clause,[status(thm)],[f27874])).
% 36.75/10.15 fof(f27876,plain,(
% 36.75/10.15 $false),
% 36.75/10.15 inference(sat_refutation,[status(thm)],[f447,f483,f548,f9194,f14835,f14837,f14844,f15420,f15816,f15818,f15907,f15992,f15994,f15996,f16001,f16003,f16130,f16132,f16137,f16139,f16177,f16350,f16363,f16510,f16512,f16673,f16675,f16687,f18226,f18668,f19795,f19844,f20054,f20080,f20973,f20975,f24175,f24177,f27819,f27875])).
% 36.75/10.18 % SZS output end CNFRefutation for theBenchmark.p
% 36.75/10.19 % Elapsed time: 4.751394 seconds
% 36.75/10.19 % CPU time: 37.346428 seconds
% 36.75/10.19 % Total memory used: 397.800 MB
% 36.75/10.19 % Net memory used: 380.722 MB
%------------------------------------------------------------------------------