%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC336-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 : n026.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:11 PM UTC 2026
% Result : Unsatisfiable 0.16s 0.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC336-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.16/0.41 % Computer : n026.cluster.edu
% 0.16/0.41 % Model : x86_64 x86_64
% 0.16/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.41 % Memory : 8046.5625MB
% 0.16/0.41 % OS : Linux 6.8.0-71-generic
% 0.16/0.41 % CPULimit : 300
% 0.16/0.41 % WCLimit : 300
% 0.16/0.41 % DateTime : Mon Sep 21 08:19:21 UTC 2026
% 0.16/0.41 % CPUTime :
% 0.16/0.44 % Drodi V4.1.1
% 0.16/0.60 % Refutation found
% 0.16/0.60 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.16/0.60 % SZS output start CNFRefutation for theBenchmark
% 0.16/0.60 fof(f4,axiom,(
% 0.16/0.60 totalorderedP(nil) ),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f8,axiom,(
% 0.16/0.60 ssList(nil) ),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f56,axiom,(
% 0.16/0.60 (![U]: (( ~ ssList(U)| segmentP(U,nil) ) ))),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f57,axiom,(
% 0.16/0.60 (![U]: (( ~ ssList(U)| segmentP(U,U) ) ))),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f67,axiom,(
% 0.16/0.60 (![U]: (( ~ ssItem(U)| totalorderedP(cons(U,nil)) ) ))),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f75,axiom,(
% 0.16/0.60 (![U]: (( ~ ssList(U)| ssList(tl(U))| nil = U ) ))),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f76,axiom,(
% 0.16/0.60 (![U]: (( ~ ssList(U)| ssItem(hd(U))| nil = U ) ))),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f80,axiom,(
% 0.16/0.60 (![U]: (( ~ segmentP(nil,U)| ~ ssList(U)| nil = U ) ))),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f119,axiom,(
% 0.16/0.60 (![U,V]: (( app(U,V) != nil| ~ ssList(V)| ~ ssList(U)| nil = V ) ))),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f127,axiom,(
% 0.16/0.60 (![U,V]: (( ~ segmentP(U,V)| ~ segmentP(V,U)| ~ ssList(U)| ~ ssList(V)| V = U ) ))),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f152,axiom,(
% 0.16/0.60 (![U,V,W]: (( ~ segmentP(U,V)| ~ segmentP(V,W)| ~ ssList(W)| ~ ssList(V)| ~ ssList(U)| segmentP(U,W) ) ))),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f172,axiom,(
% 0.16/0.60 (![U,V,W,X]: (( ~ segmentP(U,V)| ~ ssList(W)| ~ ssList(X)| ~ ssList(V)| ~ ssList(U)| segmentP(app(app(X,U),W),V) ) ))),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f173,axiom,(
% 0.16/0.60 (![U,V,W,X]: (( app(app(U,V),W) != X| ~ ssList(W)| ~ ssList(U)| ~ ssList(V)| ~ ssList(X)| segmentP(X,V) ) ))),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f186,negated_conjecture,(
% 0.16/0.60 ssList(sk1) ),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f187,negated_conjecture,(
% 0.16/0.60 ssList(sk2) ),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f189,negated_conjecture,(
% 0.16/0.60 ssList(sk4) ),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f190,negated_conjecture,(
% 0.16/0.60 sk2 = sk4 ),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f191,negated_conjecture,(
% 0.16/0.60 sk1 = sk3 ),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f193,negated_conjecture,(
% 0.16/0.60 ( ssItem(sk5)| nil = sk3 ) ),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f200,negated_conjecture,(
% 0.16/0.60 ( ssList(sk6)| nil = sk3 ) ),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f201,negated_conjecture,(
% 0.16/0.60 ( ssList(sk7)| nil = sk3 ) ),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f202,negated_conjecture,(
% 0.16/0.60 ( cons(sk5,nil) = sk3| nil = sk3 ) ),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f203,negated_conjecture,(
% 0.16/0.60 ( app(app(sk6,sk3),sk7) = sk4| nil = sk3 ) ),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f206,negated_conjecture,(
% 0.16/0.60 ( ~ segmentP(sk2,sk1)| ~ totalorderedP(sk1) ) ),
% 0.16/0.60 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.16/0.60 fof(f210,plain,(
% 0.16/0.60 totalorderedP(nil)),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f4])).
% 0.16/0.60 fof(f214,plain,(
% 0.16/0.60 ssList(nil)),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f8])).
% 0.16/0.60 fof(f262,plain,(
% 0.16/0.60 ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f56])).
% 0.16/0.60 fof(f263,plain,(
% 0.16/0.60 ![X0]: (~ssList(X0)|segmentP(X0,X0))),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f57])).
% 0.16/0.60 fof(f273,plain,(
% 0.16/0.60 ![X0]: (~ssItem(X0)|totalorderedP(cons(X0,nil)))),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f67])).
% 0.16/0.60 fof(f282,plain,(
% 0.16/0.60 ![X0]: (~ssList(X0)|ssList(tl(X0))|nil=X0)),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f75])).
% 0.16/0.60 fof(f283,plain,(
% 0.16/0.60 ![X0]: (~ssList(X0)|ssItem(hd(X0))|nil=X0)),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f76])).
% 0.16/0.60 fof(f287,plain,(
% 0.16/0.60 ![X0]: (~segmentP(nil,X0)|~ssList(X0)|nil=X0)),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f80])).
% 0.16/0.60 fof(f335,plain,(
% 0.16/0.60 ![V]: ((![U]: ((~app(U,V)=nil|~ssList(V))|~ssList(U)))|nil=V)),
% 0.16/0.60 inference(miniscoping,[status(thm)],[f119])).
% 0.16/0.60 fof(f336,plain,(
% 0.16/0.60 ![X0,X1]: (~app(X0,X1)=nil|~ssList(X1)|~ssList(X0)|nil=X1)),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f335])).
% 0.16/0.60 fof(f346,plain,(
% 0.16/0.60 ![X0,X1]: (~segmentP(X0,X1)|~segmentP(X1,X0)|~ssList(X0)|~ssList(X1)|X1=X0)),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f127])).
% 0.16/0.60 fof(f380,plain,(
% 0.16/0.60 ![U,W]: (((![V]: (((~segmentP(U,V)|~segmentP(V,W))|~ssList(W))|~ssList(V)))|~ssList(U))|segmentP(U,W))),
% 0.16/0.60 inference(miniscoping,[status(thm)],[f152])).
% 0.16/0.60 fof(f381,plain,(
% 0.16/0.60 ![X0,X1,X2]: (~segmentP(X0,X1)|~segmentP(X1,X2)|~ssList(X2)|~ssList(X1)|~ssList(X0)|segmentP(X0,X2))),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f380])).
% 0.16/0.60 fof(f411,plain,(
% 0.16/0.60 ![X0,X1,X2,X3]: (~segmentP(X0,X1)|~ssList(X2)|~ssList(X3)|~ssList(X1)|~ssList(X0)|segmentP(app(app(X3,X0),X2),X1))),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f172])).
% 0.16/0.60 fof(f412,plain,(
% 0.16/0.60 ![V,X]: ((((![U]: ((![W]: (~app(app(U,V),W)=X|~ssList(W)))|~ssList(U)))|~ssList(V))|~ssList(X))|segmentP(X,V))),
% 0.16/0.60 inference(miniscoping,[status(thm)],[f173])).
% 0.16/0.60 fof(f413,plain,(
% 0.16/0.60 ![X0,X1,X2,X3]: (~app(app(X0,X1),X2)=X3|~ssList(X2)|~ssList(X0)|~ssList(X1)|~ssList(X3)|segmentP(X3,X1))),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f412])).
% 0.16/0.60 fof(f437,plain,(
% 0.16/0.60 ssList(sk1)),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f186])).
% 0.16/0.60 fof(f438,plain,(
% 0.16/0.60 ssList(sk2)),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f187])).
% 0.16/0.60 fof(f440,plain,(
% 0.16/0.60 ssList(sk4)),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f189])).
% 0.16/0.60 fof(f441,plain,(
% 0.16/0.60 sk2=sk4),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f190])).
% 0.16/0.60 fof(f442,plain,(
% 0.16/0.60 sk1=sk3),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f191])).
% 0.16/0.60 fof(f444,plain,(
% 0.16/0.60 ssItem(sk5)|nil=sk3),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f193])).
% 0.16/0.60 fof(f453,plain,(
% 0.16/0.60 ssList(sk6)|nil=sk3),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f200])).
% 0.16/0.60 fof(f454,plain,(
% 0.16/0.60 ssList(sk7)|nil=sk3),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f201])).
% 0.16/0.60 fof(f455,plain,(
% 0.16/0.60 cons(sk5,nil)=sk3|nil=sk3),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f202])).
% 0.16/0.60 fof(f456,plain,(
% 0.16/0.60 app(app(sk6,sk3),sk7)=sk4|nil=sk3),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f203])).
% 0.16/0.60 fof(f461,plain,(
% 0.16/0.60 ~segmentP(sk2,sk1)|~totalorderedP(sk1)),
% 0.16/0.60 inference(cnf_transformation,[status(thm)],[f206])).
% 0.16/0.60 fof(f469,definition,(
% 0.16/0.60 sQ2_spl <=> (ssItem(sk5))),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f470,plain,(
% 0.16/0.60 ssItem(sk5)|~sQ2_spl),
% 0.16/0.60 inference(component_clause,[status(thm)],[f469])).
% 0.16/0.60 fof(f476,definition,(
% 0.16/0.60 sQ4_spl <=> (nil=sk3)),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f477,plain,(
% 0.16/0.60 nil=sk3|~sQ4_spl),
% 0.16/0.60 inference(component_clause,[status(thm)],[f476])).
% 0.16/0.60 fof(f478,plain,(
% 0.16/0.60 ~nil=sk3|sQ4_spl),
% 0.16/0.60 inference(component_clause,[status(thm)],[f476])).
% 0.16/0.60 fof(f479,plain,(
% 0.16/0.60 sQ2_spl|sQ4_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f444,f469,f476])).
% 0.16/0.60 fof(f480,definition,(
% 0.16/0.60 sQ5_spl <=> (ssList(sk6))),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f484,definition,(
% 0.16/0.60 sQ6_spl <=> (ssList(sk7))),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f488,definition,(
% 0.16/0.60 sQ7_spl <=> (cons(sk5,nil)=sk3)),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f489,plain,(
% 0.16/0.60 cons(sk5,nil)=sk3|~sQ7_spl),
% 0.16/0.60 inference(component_clause,[status(thm)],[f488])).
% 0.16/0.60 fof(f492,definition,(
% 0.16/0.60 sQ8_spl <=> (app(app(sk6,sk3),sk7)=sk4)),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f493,plain,(
% 0.16/0.60 app(app(sk6,sk3),sk7)=sk4|~sQ8_spl),
% 0.16/0.60 inference(component_clause,[status(thm)],[f492])).
% 0.16/0.60 fof(f504,plain,(
% 0.16/0.60 sQ5_spl|sQ4_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f453,f480,f476])).
% 0.16/0.60 fof(f505,plain,(
% 0.16/0.60 sQ6_spl|sQ4_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f454,f484,f476])).
% 0.16/0.60 fof(f506,plain,(
% 0.16/0.60 sQ7_spl|sQ4_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f455,f488,f476])).
% 0.16/0.60 fof(f507,plain,(
% 0.16/0.60 sQ8_spl|sQ4_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f456,f492,f476])).
% 0.16/0.60 fof(f510,definition,(
% 0.16/0.60 sQ11_spl <=> (segmentP(sk2,sk1))),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f512,plain,(
% 0.16/0.60 ~segmentP(sk2,sk1)|sQ11_spl),
% 0.16/0.60 inference(component_clause,[status(thm)],[f510])).
% 0.16/0.60 fof(f513,definition,(
% 0.16/0.60 sQ12_spl <=> (totalorderedP(sk1))),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f515,plain,(
% 0.16/0.60 ~totalorderedP(sk1)|sQ12_spl),
% 0.16/0.60 inference(component_clause,[status(thm)],[f513])).
% 0.16/0.60 fof(f516,plain,(
% 0.16/0.60 ~sQ11_spl|~sQ12_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f461,f510,f513])).
% 0.16/0.60 fof(f535,plain,(
% 0.16/0.60 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(app(X1,X2),X0))|segmentP(app(app(X1,X2),X0),X2))),
% 0.16/0.60 inference(destructive_equality_resolution,[status(thm)],[f413])).
% 0.16/0.60 fof(f546,plain,(
% 0.16/0.60 segmentP(nil,nil)),
% 0.16/0.60 inference(resolution,[status(thm)],[f262,f214])).
% 0.16/0.60 fof(f547,plain,(
% 0.16/0.60 segmentP(sk2,nil)),
% 0.16/0.60 inference(resolution,[status(thm)],[f262,f438])).
% 0.16/0.60 fof(f550,plain,(
% 0.16/0.60 segmentP(sk2,sk2)),
% 0.16/0.60 inference(resolution,[status(thm)],[f263,f438])).
% 0.16/0.60 fof(f555,plain,(
% 0.16/0.60 segmentP(sk4,nil)),
% 0.16/0.60 inference(resolution,[status(thm)],[f440,f262])).
% 0.16/0.60 fof(f565,plain,(
% 0.16/0.60 sk1=nil|~sQ4_spl),
% 0.16/0.60 inference(backward_demodulation,[status(thm)],[f477,f442])).
% 0.16/0.60 fof(f590,plain,(
% 0.16/0.60 ~totalorderedP(nil)|~sQ4_spl|sQ12_spl),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f565,f515])).
% 0.16/0.60 fof(f591,plain,(
% 0.16/0.60 $false|~sQ4_spl|sQ12_spl),
% 0.16/0.60 inference(forward_subsumption_resolution,[status(thm)],[f590,f210])).
% 0.16/0.60 fof(f592,plain,(
% 0.16/0.60 ~sQ4_spl|sQ12_spl),
% 0.16/0.60 inference(contradiction_clause,[status(thm)],[f591])).
% 0.16/0.60 fof(f593,plain,(
% 0.16/0.60 totalorderedP(cons(sk5,nil))|~sQ2_spl),
% 0.16/0.60 inference(resolution,[status(thm)],[f470,f273])).
% 0.16/0.60 fof(f623,plain,(
% 0.16/0.60 segmentP(sk1,sk1)),
% 0.16/0.60 inference(resolution,[status(thm)],[f437,f263])).
% 0.16/0.60 fof(f624,plain,(
% 0.16/0.60 segmentP(sk1,nil)),
% 0.16/0.60 inference(resolution,[status(thm)],[f437,f262])).
% 0.16/0.60 fof(f625,plain,(
% 0.16/0.60 ~nil=sk1|sQ4_spl),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f442,f478])).
% 0.16/0.60 fof(f660,plain,(
% 0.16/0.60 ~ssList(nil)|nil=nil),
% 0.16/0.60 inference(resolution,[status(thm)],[f546,f287])).
% 0.16/0.60 fof(f661,definition,(
% 0.16/0.60 sQ13_spl <=> (ssList(nil))),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f663,plain,(
% 0.16/0.60 ~ssList(nil)|sQ13_spl),
% 0.16/0.60 inference(component_clause,[status(thm)],[f661])).
% 0.16/0.60 fof(f664,definition,(
% 0.16/0.60 sQ14_spl <=> (nil=nil)),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f667,plain,(
% 0.16/0.60 ~sQ13_spl|sQ14_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f660,f661,f664])).
% 0.16/0.60 fof(f668,plain,(
% 0.16/0.60 $false|sQ13_spl),
% 0.16/0.60 inference(forward_subsumption_resolution,[status(thm)],[f663,f214])).
% 0.16/0.60 fof(f669,plain,(
% 0.16/0.60 sQ13_spl),
% 0.16/0.60 inference(contradiction_clause,[status(thm)],[f668])).
% 0.16/0.60 fof(f782,plain,(
% 0.16/0.60 ~segmentP(sk2,nil)|~sQ4_spl|sQ11_spl),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f565,f512])).
% 0.16/0.60 fof(f783,plain,(
% 0.16/0.60 segmentP(sk2,nil)),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f441,f555])).
% 0.16/0.60 fof(f784,plain,(
% 0.16/0.60 $false|~sQ4_spl|sQ11_spl),
% 0.16/0.60 inference(forward_subsumption_resolution,[status(thm)],[f783,f782])).
% 0.16/0.60 fof(f785,plain,(
% 0.16/0.60 ~sQ4_spl|sQ11_spl),
% 0.16/0.60 inference(contradiction_clause,[status(thm)],[f784])).
% 0.16/0.60 fof(f786,plain,(
% 0.16/0.60 app(app(sk6,sk3),sk7)=sk2|~sQ8_spl),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f441,f493])).
% 0.16/0.60 fof(f817,plain,(
% 0.16/0.60 ![X0]: (~app(X0,sk1)=nil|~ssList(X0)|nil=sk1)),
% 0.16/0.60 inference(resolution,[status(thm)],[f336,f437])).
% 0.16/0.60 fof(f842,definition,(
% 0.16/0.60 ![X0]: (sQ15_spl <=> (~app(X0,sk1)=nil|~ssList(X0)))),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f845,definition,(
% 0.16/0.60 sQ16_spl <=> (nil=sk1)),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f846,plain,(
% 0.16/0.60 nil=sk1|~sQ16_spl),
% 0.16/0.60 inference(component_clause,[status(thm)],[f845])).
% 0.16/0.60 fof(f848,plain,(
% 0.16/0.60 sQ15_spl|sQ16_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f817,f842,f845])).
% 0.16/0.60 fof(f852,definition,(
% 0.16/0.60 sQ18_spl <=> (nil=sk2)),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f953,plain,(
% 0.16/0.60 cons(sk5,nil)=sk1|~sQ7_spl),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f442,f489])).
% 0.16/0.60 fof(f963,plain,(
% 0.16/0.60 ~segmentP(nil,sk2)|~ssList(sk2)|~ssList(nil)|nil=sk2),
% 0.16/0.60 inference(resolution,[status(thm)],[f346,f547])).
% 0.16/0.60 fof(f964,plain,(
% 0.16/0.60 ~segmentP(sk2,sk2)|~ssList(sk2)|~ssList(sk2)|sk2=sk2),
% 0.16/0.60 inference(resolution,[status(thm)],[f346,f550])).
% 0.16/0.60 fof(f988,definition,(
% 0.16/0.60 sQ31_spl <=> (segmentP(nil,sk2))),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f991,definition,(
% 0.16/0.60 sQ32_spl <=> (ssList(sk2))),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f993,plain,(
% 0.16/0.60 ~ssList(sk2)|sQ32_spl),
% 0.16/0.60 inference(component_clause,[status(thm)],[f991])).
% 0.16/0.60 fof(f994,plain,(
% 0.16/0.60 ~sQ31_spl|~sQ32_spl|~sQ13_spl|sQ18_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f963,f988,f991,f661,f852])).
% 0.16/0.60 fof(f995,definition,(
% 0.16/0.60 sQ33_spl <=> (segmentP(sk2,sk2))),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f997,plain,(
% 0.16/0.60 ~segmentP(sk2,sk2)|sQ33_spl),
% 0.16/0.60 inference(component_clause,[status(thm)],[f995])).
% 0.16/0.60 fof(f998,definition,(
% 0.16/0.60 sQ34_spl <=> (sk2=sk2)),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f1001,plain,(
% 0.16/0.60 ~sQ33_spl|~sQ32_spl|sQ34_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f964,f995,f991,f998])).
% 0.16/0.60 fof(f1006,plain,(
% 0.16/0.60 $false|sQ32_spl),
% 0.16/0.60 inference(forward_subsumption_resolution,[status(thm)],[f993,f438])).
% 0.16/0.60 fof(f1007,plain,(
% 0.16/0.60 sQ32_spl),
% 0.16/0.60 inference(contradiction_clause,[status(thm)],[f1006])).
% 0.16/0.60 fof(f1012,plain,(
% 0.16/0.60 $false|sQ33_spl),
% 0.16/0.60 inference(forward_subsumption_resolution,[status(thm)],[f997,f550])).
% 0.16/0.60 fof(f1013,plain,(
% 0.16/0.60 sQ33_spl),
% 0.16/0.60 inference(contradiction_clause,[status(thm)],[f1012])).
% 0.16/0.60 fof(f1249,plain,(
% 0.16/0.60 totalorderedP(sk1)|~sQ7_spl|~sQ2_spl),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f953,f593])).
% 0.16/0.60 fof(f1250,plain,(
% 0.16/0.60 $false|sQ12_spl|~sQ7_spl|~sQ2_spl),
% 0.16/0.60 inference(forward_subsumption_resolution,[status(thm)],[f1249,f515])).
% 0.16/0.60 fof(f1251,plain,(
% 0.16/0.60 sQ12_spl|~sQ7_spl|~sQ2_spl),
% 0.16/0.60 inference(contradiction_clause,[status(thm)],[f1250])).
% 0.16/0.60 fof(f1310,plain,(
% 0.16/0.60 ~segmentP(sk1,sk1)|~ssList(sk1)|~ssList(sk1)|sk1=sk1),
% 0.16/0.60 inference(resolution,[status(thm)],[f623,f346])).
% 0.16/0.60 fof(f1311,definition,(
% 0.16/0.60 sQ37_spl <=> (segmentP(sk1,sk1))),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f1313,plain,(
% 0.16/0.60 ~segmentP(sk1,sk1)|sQ37_spl),
% 0.16/0.60 inference(component_clause,[status(thm)],[f1311])).
% 0.16/0.60 fof(f1314,definition,(
% 0.16/0.60 sQ38_spl <=> (ssList(sk1))),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f1316,plain,(
% 0.16/0.60 ~ssList(sk1)|sQ38_spl),
% 0.16/0.60 inference(component_clause,[status(thm)],[f1314])).
% 0.16/0.60 fof(f1317,definition,(
% 0.16/0.60 sQ39_spl <=> (sk1=sk1)),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f1320,plain,(
% 0.16/0.60 ~sQ37_spl|~sQ38_spl|sQ39_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f1310,f1311,f1314,f1317])).
% 0.16/0.60 fof(f1472,plain,(
% 0.16/0.60 ssList(tl(sk1))|nil=sk1),
% 0.16/0.60 inference(resolution,[status(thm)],[f282,f437])).
% 0.16/0.60 fof(f1494,definition,(
% 0.16/0.60 sQ40_spl <=> (ssList(tl(sk1)))),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f1497,plain,(
% 0.16/0.60 sQ40_spl|sQ16_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f1472,f1494,f845])).
% 0.16/0.60 fof(f1502,plain,(
% 0.16/0.60 $false|sQ4_spl|~sQ16_spl),
% 0.16/0.60 inference(forward_subsumption_resolution,[status(thm)],[f846,f625])).
% 0.16/0.60 fof(f1503,plain,(
% 0.16/0.60 sQ4_spl|~sQ16_spl),
% 0.16/0.60 inference(contradiction_clause,[status(thm)],[f1502])).
% 0.16/0.60 fof(f1511,plain,(
% 0.16/0.60 ssItem(hd(sk1))|nil=sk1),
% 0.16/0.60 inference(resolution,[status(thm)],[f283,f437])).
% 0.16/0.60 fof(f1533,definition,(
% 0.16/0.60 sQ42_spl <=> (ssItem(hd(sk1)))),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f1536,plain,(
% 0.16/0.60 sQ42_spl|sQ16_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f1511,f1533,f845])).
% 0.16/0.60 fof(f1543,plain,(
% 0.16/0.60 ~segmentP(nil,sk1)|~ssList(sk1)|~ssList(nil)|nil=sk1),
% 0.16/0.60 inference(resolution,[status(thm)],[f624,f346])).
% 0.16/0.60 fof(f1544,definition,(
% 0.16/0.60 sQ44_spl <=> (segmentP(nil,sk1))),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f1547,plain,(
% 0.16/0.60 ~sQ44_spl|~sQ38_spl|~sQ13_spl|sQ16_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f1543,f1544,f1314,f661,f845])).
% 0.16/0.60 fof(f1548,plain,(
% 0.16/0.60 $false|sQ38_spl),
% 0.16/0.60 inference(forward_subsumption_resolution,[status(thm)],[f1316,f437])).
% 0.16/0.60 fof(f1549,plain,(
% 0.16/0.60 sQ38_spl),
% 0.16/0.60 inference(contradiction_clause,[status(thm)],[f1548])).
% 0.16/0.60 fof(f1550,plain,(
% 0.16/0.60 $false|sQ37_spl),
% 0.16/0.60 inference(forward_subsumption_resolution,[status(thm)],[f1313,f623])).
% 0.16/0.60 fof(f1551,plain,(
% 0.16/0.60 sQ37_spl),
% 0.16/0.60 inference(contradiction_clause,[status(thm)],[f1550])).
% 0.16/0.60 fof(f1553,plain,(
% 0.16/0.60 ![X0]: (~segmentP(nil,X0)|~ssList(X0)|~ssList(nil)|~ssList(sk1)|segmentP(sk1,X0))),
% 0.16/0.60 inference(resolution,[status(thm)],[f381,f624])).
% 0.16/0.60 fof(f1554,plain,(
% 0.16/0.60 ![X0]: (~segmentP(sk1,X0)|~ssList(X0)|~ssList(sk1)|~ssList(sk1)|segmentP(sk1,X0))),
% 0.16/0.60 inference(resolution,[status(thm)],[f381,f623])).
% 0.16/0.60 fof(f1555,plain,(
% 0.16/0.60 ![X0]: (~segmentP(nil,X0)|~ssList(X0)|~ssList(nil)|~ssList(nil)|segmentP(nil,X0))),
% 0.16/0.60 inference(resolution,[status(thm)],[f381,f546])).
% 0.16/0.60 fof(f1556,definition,(
% 0.16/0.60 ![X0]: (sQ45_spl <=> (~segmentP(nil,X0)|~ssList(X0)|segmentP(sk1,X0)))),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f1559,plain,(
% 0.16/0.60 sQ45_spl|~sQ13_spl|~sQ38_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f1553,f1556,f661,f1314])).
% 0.16/0.60 fof(f1560,definition,(
% 0.16/0.60 ![X0]: (sQ46_spl <=> (~segmentP(sk1,X0)|~ssList(X0)|segmentP(sk1,X0)))),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f1563,plain,(
% 0.16/0.60 sQ46_spl|~sQ38_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f1554,f1560,f1314])).
% 0.16/0.60 fof(f1564,definition,(
% 0.16/0.60 ![X0]: (sQ47_spl <=> (~segmentP(nil,X0)|~ssList(X0)|segmentP(nil,X0)))),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f1567,plain,(
% 0.16/0.60 sQ47_spl|~sQ13_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f1555,f1564,f661])).
% 0.16/0.60 fof(f1604,plain,(
% 0.16/0.60 app(app(sk6,sk1),sk7)=sk2|~sQ8_spl),
% 0.16/0.60 inference(forward_demodulation,[status(thm)],[f442,f786])).
% 0.16/0.60 fof(f1905,plain,(
% 0.16/0.60 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(sk1)|segmentP(app(app(X1,sk1),X0),nil))),
% 0.16/0.60 inference(resolution,[status(thm)],[f411,f624])).
% 0.16/0.60 fof(f1906,plain,(
% 0.16/0.60 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(sk1)|~ssList(sk1)|segmentP(app(app(X1,sk1),X0),sk1))),
% 0.16/0.60 inference(resolution,[status(thm)],[f411,f623])).
% 0.16/0.60 fof(f1907,plain,(
% 0.16/0.60 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(nil)|~ssList(nil)|segmentP(app(app(X1,nil),X0),nil))),
% 0.16/0.60 inference(resolution,[status(thm)],[f411,f546])).
% 0.16/0.60 fof(f1908,definition,(
% 0.16/0.60 ![X0,X1]: (sQ77_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,sk1),X0),nil)))),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f1911,plain,(
% 0.16/0.60 sQ77_spl|~sQ13_spl|~sQ38_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f1905,f1908,f661,f1314])).
% 0.16/0.60 fof(f1912,definition,(
% 0.16/0.60 ![X0,X1]: (sQ78_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,sk1),X0),sk1)))),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f1915,plain,(
% 0.16/0.60 sQ78_spl|~sQ38_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f1906,f1912,f1314])).
% 0.16/0.60 fof(f1916,definition,(
% 0.16/0.60 ![X0,X1]: (sQ79_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,nil),X0),nil)))),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.16/0.60 fof(f1919,plain,(
% 0.16/0.60 sQ79_spl|~sQ13_spl),
% 0.16/0.60 inference(split_clause,[status(thm)],[f1907,f1916,f661])).
% 0.16/0.60 fof(f2115,plain,(
% 0.16/0.60 ~ssList(sk7)|~ssList(sk6)|~ssList(sk1)|~ssList(sk2)|segmentP(app(app(sk6,sk1),sk7),sk1)|~sQ8_spl),
% 0.16/0.60 inference(paramodulation,[status(thm)],[f1604,f535])).
% 0.16/0.60 fof(f2118,definition,(
% 0.16/0.60 sQ91_spl <=> (segmentP(app(app(sk6,sk1),sk7),sk1))),
% 0.16/0.60 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 0.16/0.61 fof(f2119,plain,(
% 0.16/0.61 segmentP(app(app(sk6,sk1),sk7),sk1)|~sQ91_spl),
% 0.16/0.61 inference(component_clause,[status(thm)],[f2118])).
% 0.16/0.61 fof(f2121,plain,(
% 0.16/0.61 ~sQ6_spl|~sQ5_spl|~sQ38_spl|~sQ32_spl|sQ91_spl|~sQ8_spl),
% 0.16/0.61 inference(split_clause,[status(thm)],[f2115,f484,f480,f1314,f991,f2118,f492])).
% 0.16/0.61 fof(f2133,plain,(
% 0.16/0.61 segmentP(sk2,sk1)|~sQ8_spl|~sQ91_spl),
% 0.16/0.61 inference(forward_demodulation,[status(thm)],[f1604,f2119])).
% 0.16/0.61 fof(f2134,plain,(
% 0.16/0.61 $false|sQ11_spl|~sQ8_spl|~sQ91_spl),
% 0.16/0.61 inference(forward_subsumption_resolution,[status(thm)],[f2133,f512])).
% 0.16/0.61 fof(f2135,plain,(
% 0.16/0.61 sQ11_spl|~sQ8_spl|~sQ91_spl),
% 0.16/0.61 inference(contradiction_clause,[status(thm)],[f2134])).
% 0.16/0.61 fof(f2136,plain,(
% 0.16/0.61 $false),
% 0.16/0.61 inference(sat_refutation,[status(thm)],[f479,f504,f505,f506,f507,f516,f592,f667,f669,f785,f848,f994,f1001,f1007,f1013,f1251,f1320,f1497,f1503,f1536,f1547,f1549,f1551,f1559,f1563,f1567,f1911,f1915,f1919,f2121,f2135])).
% 0.16/0.61 % SZS output end CNFRefutation for theBenchmark.p
% 0.16/0.61 % Elapsed time: 0.191738 seconds
% 0.16/0.61 % CPU time: 1.135559 seconds
% 0.16/0.61 % Total memory used: 125.104 MB
% 0.16/0.61 % Net memory used: 124.286 MB
%------------------------------------------------------------------------------