%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC264-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 02:42:00 PM UTC 2026
% Result : Unsatisfiable 9.07s 1.63s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC264-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.41 % Computer : n002.cluster.edu
% 0.13/0.41 % Model : x86_64 x86_64
% 0.13/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.41 % Memory : 8046.5625MB
% 0.13/0.41 % OS : Linux 6.8.0-71-generic
% 0.13/0.41 % CPULimit : 300
% 0.13/0.41 % WCLimit : 300
% 0.13/0.41 % DateTime : Mon Sep 21 08:13:03 UTC 2026
% 0.13/0.41 % CPUTime :
% 0.18/0.44 % Drodi V4.1.1
% 9.07/1.63 % Refutation found
% 9.07/1.63 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 9.07/1.63 % SZS output start CNFRefutation for theBenchmark
% 9.07/1.63 fof(f8,axiom,(
% 9.07/1.63 ssList(nil) ),
% 9.07/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.63 fof(f27,axiom,(
% 9.07/1.63 (![U]: (ssList(skaf68(U)) ))),
% 9.07/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.63 fof(f28,axiom,(
% 9.07/1.63 (![U]: (ssList(skaf67(U)) ))),
% 9.07/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.63 fof(f29,axiom,(
% 9.07/1.63 (![U]: (ssList(skaf66(U)) ))),
% 9.07/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.63 fof(f30,axiom,(
% 9.07/1.63 (![U]: (ssItem(skaf65(U)) ))),
% 9.07/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.63 fof(f31,axiom,(
% 9.07/1.63 (![U]: (ssItem(skaf64(U)) ))),
% 9.07/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.63 fof(f42,axiom,(
% 9.07/1.63 (![U]: (ssList(skaf53(U)) ))),
% 9.07/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.63 fof(f43,axiom,(
% 9.07/1.63 (![U]: (ssList(skaf52(U)) ))),
% 9.07/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.63 fof(f44,axiom,(
% 9.07/1.63 (![U]: (ssList(skaf51(U)) ))),
% 9.07/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.63 fof(f45,axiom,(
% 9.07/1.63 (![U]: (ssItem(skaf50(U)) ))),
% 9.07/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.63 fof(f46,axiom,(
% 9.07/1.63 (![U]: (ssItem(skaf49(U)) ))),
% 9.07/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.63 fof(f73,axiom,(
% 9.07/1.63 (![U]: (( ~ ssList(U)| app(U,nil) = U ) ))),
% 9.07/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.63 fof(f74,axiom,(
% 9.07/1.63 (![U]: (( ~ ssList(U)| app(nil,U) = U ) ))),
% 9.07/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.63 fof(f85,axiom,(
% 9.07/1.63 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| ssList(app(V,U)) ) ))),
% 9.07/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.63 fof(f91,axiom,(
% 9.07/1.63 (![U]: (( ~ leq(skaf64(U),skaf65(U))| ~ ssList(U)| totalorderedP(U) ) ))),
% 9.07/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.63 fof(f103,axiom,(
% 9.07/1.63 (![U,V]: (( ~ lt(U,V)| ~ ssItem(V)| ~ ssItem(U)| leq(U,V) ) ))),
% 9.07/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.63 fof(f164,axiom,(
% 9.07/1.63 (![U]: (( ~ ssList(U)| totalorderedP(U)| app(app(skaf66(U),cons(skaf64(U),skaf67(U))),cons(skaf65(U),skaf68(U))) = U ) ))),
% 9.07/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.63 fof(f181,axiom,(
% 9.07/1.63 (![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) ) ))),
% 9.07/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.63 fof(f186,negated_conjecture,(
% 9.07/1.63 ssList(sk1) ),
% 9.07/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.63 fof(f187,negated_conjecture,(
% 9.07/1.63 ssList(sk2) ),
% 9.07/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.63 fof(f191,negated_conjecture,(
% 9.07/1.63 sk1 = sk3 ),
% 9.07/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.63 fof(f192,negated_conjecture,(
% 9.07/1.63 strictorderedP(sk3) ),
% 9.07/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.63 fof(f193,negated_conjecture,(
% 9.07/1.63 ~ totalorderedP(sk1) ),
% 9.07/1.63 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 9.07/1.63 fof(f201,plain,(
% 9.07/1.63 ssList(nil)),
% 9.07/1.63 inference(cnf_transformation,[status(thm)],[f8])).
% 9.07/1.63 fof(f220,plain,(
% 9.07/1.63 ![X0]: (ssList(skaf68(X0)))),
% 9.07/1.63 inference(cnf_transformation,[status(thm)],[f27])).
% 9.07/1.63 fof(f221,plain,(
% 9.07/1.63 ![X0]: (ssList(skaf67(X0)))),
% 9.07/1.63 inference(cnf_transformation,[status(thm)],[f28])).
% 9.07/1.63 fof(f222,plain,(
% 9.07/1.63 ![X0]: (ssList(skaf66(X0)))),
% 9.07/1.63 inference(cnf_transformation,[status(thm)],[f29])).
% 9.07/1.63 fof(f223,plain,(
% 9.07/1.63 ![X0]: (ssItem(skaf65(X0)))),
% 9.07/1.63 inference(cnf_transformation,[status(thm)],[f30])).
% 9.07/1.63 fof(f224,plain,(
% 9.07/1.63 ![X0]: (ssItem(skaf64(X0)))),
% 9.07/1.63 inference(cnf_transformation,[status(thm)],[f31])).
% 9.07/1.63 fof(f235,plain,(
% 9.07/1.63 ![X0]: (ssList(skaf53(X0)))),
% 9.07/1.63 inference(cnf_transformation,[status(thm)],[f42])).
% 9.07/1.63 fof(f236,plain,(
% 9.07/1.63 ![X0]: (ssList(skaf52(X0)))),
% 9.07/1.63 inference(cnf_transformation,[status(thm)],[f43])).
% 9.07/1.63 fof(f237,plain,(
% 9.07/1.63 ![X0]: (ssList(skaf51(X0)))),
% 9.07/1.63 inference(cnf_transformation,[status(thm)],[f44])).
% 9.07/1.63 fof(f238,plain,(
% 9.07/1.63 ![X0]: (ssItem(skaf50(X0)))),
% 9.07/1.63 inference(cnf_transformation,[status(thm)],[f45])).
% 9.07/1.63 fof(f239,plain,(
% 9.07/1.63 ![X0]: (ssItem(skaf49(X0)))),
% 9.07/1.63 inference(cnf_transformation,[status(thm)],[f46])).
% 9.07/1.63 fof(f267,plain,(
% 9.07/1.63 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 9.07/1.63 inference(cnf_transformation,[status(thm)],[f73])).
% 9.07/1.63 fof(f268,plain,(
% 9.07/1.63 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 9.07/1.63 inference(cnf_transformation,[status(thm)],[f74])).
% 9.07/1.63 fof(f279,plain,(
% 9.07/1.63 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X1,X0)))),
% 9.07/1.63 inference(cnf_transformation,[status(thm)],[f85])).
% 9.07/1.63 fof(f285,plain,(
% 9.07/1.63 ![X0]: (~leq(skaf64(X0),skaf65(X0))|~ssList(X0)|totalorderedP(X0))),
% 9.07/1.63 inference(cnf_transformation,[status(thm)],[f91])).
% 9.07/1.63 fof(f299,plain,(
% 9.07/1.63 ![X0,X1]: (~lt(X0,X1)|~ssItem(X1)|~ssItem(X0)|leq(X0,X1))),
% 9.07/1.63 inference(cnf_transformation,[status(thm)],[f103])).
% 9.07/1.63 fof(f388,plain,(
% 9.07/1.63 ![X0]: (~ssList(X0)|totalorderedP(X0)|app(app(skaf66(X0),cons(skaf64(X0),skaf67(X0))),cons(skaf65(X0),skaf68(X0)))=X0)),
% 9.07/1.63 inference(cnf_transformation,[status(thm)],[f164])).
% 9.07/1.63 fof(f414,plain,(
% 9.07/1.63 ![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))),
% 9.07/1.63 inference(miniscoping,[status(thm)],[f181])).
% 9.07/1.63 fof(f415,plain,(
% 9.07/1.63 ![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))),
% 9.07/1.63 inference(cnf_transformation,[status(thm)],[f414])).
% 9.07/1.63 fof(f424,plain,(
% 9.07/1.63 ssList(sk1)),
% 9.07/1.63 inference(cnf_transformation,[status(thm)],[f186])).
% 9.07/1.63 fof(f425,plain,(
% 9.07/1.63 ssList(sk2)),
% 9.07/1.63 inference(cnf_transformation,[status(thm)],[f187])).
% 9.07/1.63 fof(f429,plain,(
% 9.07/1.63 sk1=sk3),
% 9.07/1.63 inference(cnf_transformation,[status(thm)],[f191])).
% 9.07/1.63 fof(f430,plain,(
% 9.07/1.63 strictorderedP(sk3)),
% 9.07/1.63 inference(cnf_transformation,[status(thm)],[f192])).
% 9.07/1.63 fof(f431,plain,(
% 9.07/1.63 ~totalorderedP(sk1)),
% 9.07/1.63 inference(cnf_transformation,[status(thm)],[f193])).
% 9.07/1.63 fof(f463,plain,(
% 9.07/1.63 ![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))),
% 9.07/1.63 inference(destructive_equality_resolution,[status(thm)],[f415])).
% 9.07/1.63 fof(f470,plain,(
% 9.07/1.63 strictorderedP(sk1)),
% 9.07/1.63 inference(forward_demodulation,[status(thm)],[f429,f430])).
% 9.07/1.63 fof(f472,definition,(
% 9.07/1.63 sQ2_spl <=> (ssList(nil))),
% 9.07/1.63 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 9.07/1.63 fof(f474,plain,(
% 9.07/1.63 ~ssList(nil)|sQ2_spl),
% 9.07/1.63 inference(component_clause,[status(thm)],[f472])).
% 9.07/1.63 fof(f555,plain,(
% 9.07/1.63 app(sk1,nil)=sk1),
% 9.07/1.63 inference(resolution,[status(thm)],[f267,f424])).
% 9.07/1.63 fof(f584,plain,(
% 9.07/1.63 app(nil,sk2)=sk2),
% 9.07/1.63 inference(resolution,[status(thm)],[f268,f425])).
% 9.07/1.63 fof(f601,plain,(
% 9.07/1.63 $false|sQ2_spl),
% 9.07/1.63 inference(forward_subsumption_resolution,[status(thm)],[f474,f201])).
% 9.07/1.63 fof(f602,plain,(
% 9.07/1.63 sQ2_spl),
% 9.07/1.63 inference(contradiction_clause,[status(thm)],[f601])).
% 9.07/1.63 fof(f641,plain,(
% 9.07/1.63 ![X0]: (~ssList(X0)|ssList(app(sk1,X0)))),
% 9.07/1.63 inference(resolution,[status(thm)],[f279,f424])).
% 9.07/1.63 fof(f659,plain,(
% 9.07/1.63 ~ssList(nil)|ssList(sk1)),
% 9.07/1.63 inference(paramodulation,[status(thm)],[f555,f641])).
% 9.07/1.63 fof(f660,definition,(
% 9.07/1.63 sQ9_spl <=> (ssList(sk1))),
% 9.07/1.63 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 9.07/1.63 fof(f663,plain,(
% 9.07/1.63 ~sQ2_spl|sQ9_spl),
% 9.07/1.63 inference(split_clause,[status(thm)],[f659,f472,f660])).
% 9.07/1.63 fof(f1450,definition,(
% 9.07/1.63 sQ69_spl <=> (totalorderedP(sk1))),
% 9.07/1.63 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 9.07/1.63 fof(f1451,plain,(
% 9.07/1.63 totalorderedP(sk1)|~sQ69_spl),
% 9.07/1.63 inference(component_clause,[status(thm)],[f1450])).
% 9.07/1.63 fof(f3586,plain,(
% 9.07/1.63 totalorderedP(sk1)|app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1)))=sk1),
% 9.07/1.63 inference(resolution,[status(thm)],[f388,f424])).
% 9.07/1.63 fof(f3628,definition,(
% 9.07/1.63 sQ201_spl <=> (app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1)))=sk1)),
% 9.07/1.63 introduced(definition,[new_symbols(definition,[sQ201_spl])],[split_symbol_definition])).
% 9.07/1.63 fof(f3629,plain,(
% 9.07/1.63 app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1)))=sk1|~sQ201_spl),
% 9.07/1.63 inference(component_clause,[status(thm)],[f3628])).
% 9.07/1.63 fof(f3631,plain,(
% 9.07/1.63 sQ69_spl|sQ201_spl),
% 9.07/1.63 inference(split_clause,[status(thm)],[f3586,f1450,f3628])).
% 9.07/1.63 fof(f3643,plain,(
% 9.07/1.63 $false|~sQ69_spl),
% 9.07/1.63 inference(forward_subsumption_resolution,[status(thm)],[f1451,f431])).
% 9.07/1.63 fof(f3644,plain,(
% 9.07/1.63 ~sQ69_spl),
% 9.07/1.63 inference(contradiction_clause,[status(thm)],[f3643])).
% 9.07/1.63 fof(f5038,definition,(
% 9.07/1.63 ![X0]: (sQ335_spl <=> (~app(X0,sk2)=sk2|~ssList(X0)))),
% 9.07/1.63 introduced(definition,[new_symbols(definition,[sQ335_spl])],[split_symbol_definition])).
% 9.07/1.63 fof(f5039,plain,(
% 9.07/1.63 ![X0]: (~app(X0,sk2)=sk2|~ssList(X0)|~sQ335_spl)),
% 9.07/1.63 inference(component_clause,[status(thm)],[f5038])).
% 9.07/1.63 fof(f7241,plain,(
% 9.07/1.63 ~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))|~sQ201_spl),
% 9.07/1.63 inference(paramodulation,[status(thm)],[f3629,f463])).
% 9.07/1.63 fof(f7249,definition,(
% 9.07/1.63 sQ438_spl <=> (ssList(skaf68(sk1)))),
% 9.07/1.63 introduced(definition,[new_symbols(definition,[sQ438_spl])],[split_symbol_definition])).
% 9.07/1.63 fof(f7251,plain,(
% 9.07/1.63 ~ssList(skaf68(sk1))|sQ438_spl),
% 9.07/1.63 inference(component_clause,[status(thm)],[f7249])).
% 9.07/1.63 fof(f7252,definition,(
% 9.07/1.63 sQ439_spl <=> (ssList(skaf67(sk1)))),
% 9.07/1.63 introduced(definition,[new_symbols(definition,[sQ439_spl])],[split_symbol_definition])).
% 9.07/1.63 fof(f7254,plain,(
% 9.07/1.63 ~ssList(skaf67(sk1))|sQ439_spl),
% 9.07/1.63 inference(component_clause,[status(thm)],[f7252])).
% 9.07/1.63 fof(f7255,definition,(
% 9.07/1.63 sQ440_spl <=> (ssList(skaf66(sk1)))),
% 9.07/1.63 introduced(definition,[new_symbols(definition,[sQ440_spl])],[split_symbol_definition])).
% 9.07/1.63 fof(f7257,plain,(
% 9.07/1.63 ~ssList(skaf66(sk1))|sQ440_spl),
% 9.07/1.63 inference(component_clause,[status(thm)],[f7255])).
% 9.07/1.63 fof(f7258,definition,(
% 9.07/1.63 sQ441_spl <=> (ssItem(skaf65(sk1)))),
% 9.07/1.63 introduced(definition,[new_symbols(definition,[sQ441_spl])],[split_symbol_definition])).
% 9.07/1.63 fof(f7260,plain,(
% 9.07/1.63 ~ssItem(skaf65(sk1))|sQ441_spl),
% 9.07/1.63 inference(component_clause,[status(thm)],[f7258])).
% 9.07/1.63 fof(f7261,definition,(
% 9.07/1.63 sQ442_spl <=> (ssItem(skaf64(sk1)))),
% 9.07/1.63 introduced(definition,[new_symbols(definition,[sQ442_spl])],[split_symbol_definition])).
% 9.07/1.63 fof(f7263,plain,(
% 9.07/1.63 ~ssItem(skaf64(sk1))|sQ442_spl),
% 9.07/1.63 inference(component_clause,[status(thm)],[f7261])).
% 9.07/1.63 fof(f7267,definition,(
% 9.07/1.63 sQ444_spl <=> (leq(skaf64(sk1),skaf65(sk1)))),
% 9.07/1.63 introduced(definition,[new_symbols(definition,[sQ444_spl])],[split_symbol_definition])).
% 9.07/1.63 fof(f7268,plain,(
% 9.07/1.63 leq(skaf64(sk1),skaf65(sk1))|~sQ444_spl),
% 9.07/1.63 inference(component_clause,[status(thm)],[f7267])).
% 9.07/1.63 fof(f7271,definition,(
% 9.07/1.63 sQ445_spl <=> (strictorderedP(app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1)))))),
% 9.07/1.63 introduced(definition,[new_symbols(definition,[sQ445_spl])],[split_symbol_definition])).
% 9.07/1.63 fof(f7273,plain,(
% 9.07/1.63 ~strictorderedP(app(app(skaf66(sk1),cons(skaf64(sk1),skaf67(sk1))),cons(skaf65(sk1),skaf68(sk1))))|sQ445_spl),
% 9.07/1.63 inference(component_clause,[status(thm)],[f7271])).
% 9.07/1.63 fof(f7274,definition,(
% 9.07/1.63 sQ446_spl <=> (lt(skaf64(sk1),skaf65(sk1)))),
% 9.07/1.63 introduced(definition,[new_symbols(definition,[sQ446_spl])],[split_symbol_definition])).
% 9.07/1.63 fof(f7275,plain,(
% 9.07/1.63 lt(skaf64(sk1),skaf65(sk1))|~sQ446_spl),
% 9.07/1.63 inference(component_clause,[status(thm)],[f7274])).
% 9.07/1.63 fof(f7277,plain,(
% 9.07/1.63 ~sQ438_spl|~sQ439_spl|~sQ440_spl|~sQ441_spl|~sQ442_spl|~sQ445_spl|~sQ9_spl|sQ446_spl|~sQ201_spl),
% 9.07/1.63 inference(split_clause,[status(thm)],[f7241,f7249,f7252,f7255,f7258,f7261,f7271,f660,f7274,f3628])).
% 9.07/1.63 fof(f7315,plain,(
% 9.07/1.63 $false|sQ441_spl),
% 9.07/1.63 inference(forward_subsumption_resolution,[status(thm)],[f7260,f223])).
% 9.07/1.63 fof(f7316,plain,(
% 9.07/1.63 sQ441_spl),
% 9.07/1.63 inference(contradiction_clause,[status(thm)],[f7315])).
% 9.07/1.63 fof(f7317,plain,(
% 9.07/1.63 $false|sQ438_spl),
% 9.07/1.63 inference(forward_subsumption_resolution,[status(thm)],[f7251,f220])).
% 9.07/1.63 fof(f7318,plain,(
% 9.07/1.63 sQ438_spl),
% 9.07/1.63 inference(contradiction_clause,[status(thm)],[f7317])).
% 9.07/1.63 fof(f7319,plain,(
% 9.07/1.63 $false|sQ442_spl),
% 9.07/1.63 inference(forward_subsumption_resolution,[status(thm)],[f7263,f224])).
% 9.07/1.63 fof(f7320,plain,(
% 9.07/1.63 sQ442_spl),
% 9.07/1.63 inference(contradiction_clause,[status(thm)],[f7319])).
% 9.07/1.63 fof(f7321,plain,(
% 9.07/1.63 $false|sQ440_spl),
% 9.07/1.63 inference(forward_subsumption_resolution,[status(thm)],[f7257,f222])).
% 9.07/1.63 fof(f7322,plain,(
% 9.07/1.63 sQ440_spl),
% 9.07/1.63 inference(contradiction_clause,[status(thm)],[f7321])).
% 9.07/1.63 fof(f7323,plain,(
% 9.07/1.63 $false|sQ439_spl),
% 9.07/1.63 inference(forward_subsumption_resolution,[status(thm)],[f7254,f221])).
% 9.07/1.63 fof(f7324,plain,(
% 9.07/1.63 sQ439_spl),
% 9.07/1.63 inference(contradiction_clause,[status(thm)],[f7323])).
% 9.07/1.63 fof(f7327,plain,(
% 9.07/1.63 ~strictorderedP(sk1)|~sQ201_spl|sQ445_spl),
% 9.07/1.63 inference(forward_demodulation,[status(thm)],[f3629,f7273])).
% 9.07/1.63 fof(f7328,plain,(
% 9.07/1.63 $false|~sQ201_spl|sQ445_spl),
% 9.07/1.63 inference(forward_subsumption_resolution,[status(thm)],[f7327,f470])).
% 9.07/1.63 fof(f7329,plain,(
% 9.07/1.63 ~sQ201_spl|sQ445_spl),
% 9.07/1.63 inference(contradiction_clause,[status(thm)],[f7328])).
% 9.07/1.63 fof(f8270,plain,(
% 9.07/1.63 ~app(nil,sk2)=sk2|~sQ335_spl),
% 9.07/1.63 inference(resolution,[status(thm)],[f5039,f201])).
% 9.07/1.63 fof(f8272,plain,(
% 9.07/1.63 ~sk2=sk2|~sQ335_spl),
% 9.07/1.63 inference(forward_demodulation,[status(thm)],[f584,f8270])).
% 9.07/1.63 fof(f8273,plain,(
% 9.07/1.63 $false|~sQ335_spl),
% 9.07/1.63 inference(trivial_equality_resolution,[status(thm)],[f8272])).
% 9.07/1.63 fof(f8274,plain,(
% 9.07/1.63 ~sQ335_spl),
% 9.07/1.63 inference(contradiction_clause,[status(thm)],[f8273])).
% 9.07/1.63 fof(f8377,definition,(
% 9.07/1.63 sQ480_spl <=> (ssList(skaf53(sk2)))),
% 9.07/1.63 introduced(definition,[new_symbols(definition,[sQ480_spl])],[split_symbol_definition])).
% 9.07/1.63 fof(f8379,plain,(
% 9.07/1.63 ~ssList(skaf53(sk2))|sQ480_spl),
% 9.07/1.63 inference(component_clause,[status(thm)],[f8377])).
% 9.07/1.63 fof(f8380,definition,(
% 9.07/1.63 sQ481_spl <=> (ssList(skaf52(sk2)))),
% 9.07/1.63 introduced(definition,[new_symbols(definition,[sQ481_spl])],[split_symbol_definition])).
% 9.07/1.63 fof(f8382,plain,(
% 9.07/1.63 ~ssList(skaf52(sk2))|sQ481_spl),
% 9.07/1.63 inference(component_clause,[status(thm)],[f8380])).
% 9.07/1.63 fof(f8383,definition,(
% 9.07/1.63 sQ482_spl <=> (ssList(skaf51(sk2)))),
% 9.07/1.63 introduced(definition,[new_symbols(definition,[sQ482_spl])],[split_symbol_definition])).
% 9.07/1.63 fof(f8385,plain,(
% 9.07/1.63 ~ssList(skaf51(sk2))|sQ482_spl),
% 9.07/1.63 inference(component_clause,[status(thm)],[f8383])).
% 9.07/1.63 fof(f8386,definition,(
% 9.07/1.63 sQ483_spl <=> (ssItem(skaf50(sk2)))),
% 9.07/1.63 introduced(definition,[new_symbols(definition,[sQ483_spl])],[split_symbol_definition])).
% 9.07/1.63 fof(f8388,plain,(
% 9.07/1.63 ~ssItem(skaf50(sk2))|sQ483_spl),
% 9.07/1.63 inference(component_clause,[status(thm)],[f8386])).
% 9.07/1.63 fof(f8389,definition,(
% 9.07/1.63 sQ484_spl <=> (ssItem(skaf49(sk2)))),
% 9.07/1.63 introduced(definition,[new_symbols(definition,[sQ484_spl])],[split_symbol_definition])).
% 9.07/1.63 fof(f8391,plain,(
% 9.07/1.63 ~ssItem(skaf49(sk2))|sQ484_spl),
% 9.07/1.63 inference(component_clause,[status(thm)],[f8389])).
% 9.07/1.63 fof(f8444,plain,(
% 9.07/1.63 $false|sQ483_spl),
% 9.07/1.63 inference(forward_subsumption_resolution,[status(thm)],[f8388,f238])).
% 9.07/1.63 fof(f8445,plain,(
% 9.07/1.63 sQ483_spl),
% 9.07/1.63 inference(contradiction_clause,[status(thm)],[f8444])).
% 9.07/1.63 fof(f8446,plain,(
% 9.07/1.63 $false|sQ480_spl),
% 9.07/1.63 inference(forward_subsumption_resolution,[status(thm)],[f8379,f235])).
% 9.07/1.63 fof(f8447,plain,(
% 9.07/1.63 sQ480_spl),
% 9.07/1.63 inference(contradiction_clause,[status(thm)],[f8446])).
% 9.07/1.63 fof(f8448,plain,(
% 9.07/1.63 $false|sQ484_spl),
% 9.07/1.63 inference(forward_subsumption_resolution,[status(thm)],[f8391,f239])).
% 9.07/1.63 fof(f8449,plain,(
% 9.07/1.63 sQ484_spl),
% 9.07/1.63 inference(contradiction_clause,[status(thm)],[f8448])).
% 9.07/1.63 fof(f8450,plain,(
% 9.07/1.63 $false|sQ482_spl),
% 9.07/1.63 inference(forward_subsumption_resolution,[status(thm)],[f8385,f237])).
% 9.07/1.63 fof(f8451,plain,(
% 9.07/1.63 sQ482_spl),
% 9.07/1.63 inference(contradiction_clause,[status(thm)],[f8450])).
% 9.07/1.63 fof(f8452,plain,(
% 9.07/1.63 $false|sQ481_spl),
% 9.07/1.63 inference(forward_subsumption_resolution,[status(thm)],[f8382,f236])).
% 9.07/1.63 fof(f8453,plain,(
% 9.07/1.63 sQ481_spl),
% 9.07/1.63 inference(contradiction_clause,[status(thm)],[f8452])).
% 9.07/1.63 fof(f10483,plain,(
% 9.07/1.63 ~ssList(sk1)|totalorderedP(sk1)|~sQ444_spl),
% 9.07/1.63 inference(resolution,[status(thm)],[f7268,f285])).
% 9.07/1.63 fof(f10489,plain,(
% 9.07/1.63 ~sQ9_spl|sQ69_spl|~sQ444_spl),
% 9.07/1.63 inference(split_clause,[status(thm)],[f10483,f660,f1450,f7267])).
% 9.07/1.63 fof(f11404,plain,(
% 9.07/1.63 ~ssItem(skaf65(sk1))|~ssItem(skaf64(sk1))|leq(skaf64(sk1),skaf65(sk1))|~sQ446_spl),
% 9.07/1.63 inference(resolution,[status(thm)],[f299,f7275])).
% 9.07/1.63 fof(f11406,plain,(
% 9.07/1.63 ~sQ441_spl|~sQ442_spl|sQ444_spl|~sQ446_spl),
% 9.07/1.63 inference(split_clause,[status(thm)],[f11404,f7258,f7261,f7267,f7274])).
% 9.07/1.63 fof(f11408,plain,(
% 9.07/1.63 $false),
% 9.07/1.63 inference(sat_refutation,[status(thm)],[f602,f663,f3631,f3644,f7277,f7316,f7318,f7320,f7322,f7324,f7329,f8274,f8445,f8447,f8449,f8451,f8453,f10489,f11406])).
% 9.07/1.64 % SZS output end CNFRefutation for theBenchmark.p
% 9.07/1.66 % Elapsed time: 1.222569 seconds
% 9.07/1.66 % CPU time: 9.399539 seconds
% 9.07/1.66 % Total memory used: 244.205 MB
% 9.07/1.66 % Net memory used: 237.290 MB
%------------------------------------------------------------------------------