%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC070-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 : n012.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:41:30 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC070-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n012.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 07:52:51 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.13/0.37 % Drodi V4.1.1
% 0.13/0.49 % Refutation found
% 0.13/0.49 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.49 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.49 fof(f8,axiom,(
% 0.13/0.49 ssList(nil) ),
% 0.13/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.49 fof(f50,axiom,(
% 0.13/0.49 (![U,V]: (ssList(skaf46(U,V)) ))),
% 0.13/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.49 fof(f51,axiom,(
% 0.13/0.49 (![U,V]: (ssList(skaf45(U,V)) ))),
% 0.13/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.49 fof(f56,axiom,(
% 0.13/0.49 (![U]: (( ~ ssList(U)| segmentP(U,nil) ) ))),
% 0.13/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.49 fof(f57,axiom,(
% 0.13/0.49 (![U]: (( ~ ssList(U)| segmentP(U,U) ) ))),
% 0.13/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.49 fof(f59,axiom,(
% 0.13/0.49 (![U]: (( ~ ssList(U)| rearsegP(U,U) ) ))),
% 0.13/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.49 fof(f73,axiom,(
% 0.13/0.49 (![U]: (( ~ ssList(U)| app(U,nil) = U ) ))),
% 0.13/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.49 fof(f74,axiom,(
% 0.13/0.49 (![U]: (( ~ ssList(U)| app(nil,U) = U ) ))),
% 0.13/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.49 fof(f80,axiom,(
% 0.13/0.49 (![U]: (( ~ segmentP(nil,U)| ~ ssList(U)| nil = U ) ))),
% 0.13/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.49 fof(f84,axiom,(
% 0.13/0.49 (![U]: (( ~ frontsegP(nil,U)| ~ ssList(U)| nil = U ) ))),
% 0.13/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.49 fof(f127,axiom,(
% 0.13/0.49 (![U,V]: (( ~ segmentP(U,V)| ~ segmentP(V,U)| ~ ssList(U)| ~ ssList(V)| V = U ) ))),
% 0.13/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.49 fof(f131,axiom,(
% 0.13/0.49 (![U,V]: (( ~ rearsegP(U,V)| ~ ssList(V)| ~ ssList(U)| app(skaf46(U,V),V) = U ) ))),
% 0.13/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.49 fof(f132,axiom,(
% 0.13/0.49 (![U,V]: (( ~ frontsegP(U,V)| ~ ssList(V)| ~ ssList(U)| app(V,skaf45(U,V)) = U ) ))),
% 0.13/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.49 fof(f137,axiom,(
% 0.13/0.49 (![U,V,W]: (( ~ frontsegP(U,V)| ~ ssList(W)| ~ ssList(V)| ~ ssList(U)| frontsegP(app(U,W),V) ) ))),
% 0.13/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.49 fof(f144,axiom,(
% 0.13/0.49 (![U,V,W]: (( app(U,V) != W| ~ ssList(V)| ~ ssList(U)| ~ ssList(W)| frontsegP(W,U) ) ))),
% 0.13/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.49 fof(f172,axiom,(
% 0.13/0.49 (![U,V,W,X]: (( ~ segmentP(U,V)| ~ ssList(W)| ~ ssList(X)| ~ ssList(V)| ~ ssList(U)| segmentP(app(app(X,U),W),V) ) ))),
% 0.13/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.49 fof(f186,negated_conjecture,(
% 0.13/0.49 ssList(sk1) ),
% 0.13/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.49 fof(f187,negated_conjecture,(
% 0.13/0.49 ssList(sk2) ),
% 0.13/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.49 fof(f190,negated_conjecture,(
% 0.13/0.49 sk2 = sk4 ),
% 0.13/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.49 fof(f191,negated_conjecture,(
% 0.13/0.49 sk1 = sk3 ),
% 0.13/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.49 fof(f192,negated_conjecture,(
% 0.13/0.49 (![A]: (( ~ ssList(A)| ~ neq(A,nil)| ~ segmentP(sk2,A)| ~ segmentP(sk1,A) ) ))),
% 0.13/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.49 fof(f193,negated_conjecture,(
% 0.13/0.49 ( nil != sk2| nil != sk1 ) ),
% 0.13/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.49 fof(f194,negated_conjecture,(
% 0.13/0.49 ( nil = sk4| neq(sk3,nil) ) ),
% 0.13/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.49 fof(f195,negated_conjecture,(
% 0.13/0.49 ( nil = sk4| frontsegP(sk4,sk3) ) ),
% 0.13/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.49 fof(f196,negated_conjecture,(
% 0.13/0.49 ( nil = sk3| neq(sk3,nil) ) ),
% 0.13/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.49 fof(f197,negated_conjecture,(
% 0.13/0.49 ( nil = sk3| frontsegP(sk4,sk3) ) ),
% 0.13/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.49 fof(f205,plain,(
% 0.13/0.49 ssList(nil)),
% 0.13/0.49 inference(cnf_transformation,[status(thm)],[f8])).
% 0.13/0.49 fof(f247,plain,(
% 0.13/0.49 ![X0,X1]: (ssList(skaf46(X0,X1)))),
% 0.13/0.49 inference(cnf_transformation,[status(thm)],[f50])).
% 0.13/0.49 fof(f248,plain,(
% 0.13/0.49 ![X0,X1]: (ssList(skaf45(X0,X1)))),
% 0.13/0.49 inference(cnf_transformation,[status(thm)],[f51])).
% 0.13/0.49 fof(f253,plain,(
% 0.13/0.49 ![X0]: (~ssList(X0)|segmentP(X0,nil))),
% 0.13/0.49 inference(cnf_transformation,[status(thm)],[f56])).
% 0.13/0.49 fof(f254,plain,(
% 0.13/0.49 ![X0]: (~ssList(X0)|segmentP(X0,X0))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f57])).
% 0.13/0.50 fof(f256,plain,(
% 0.13/0.50 ![X0]: (~ssList(X0)|rearsegP(X0,X0))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f59])).
% 0.13/0.50 fof(f271,plain,(
% 0.13/0.50 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f73])).
% 0.13/0.50 fof(f272,plain,(
% 0.13/0.50 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f74])).
% 0.13/0.50 fof(f278,plain,(
% 0.13/0.50 ![X0]: (~segmentP(nil,X0)|~ssList(X0)|nil=X0)),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f80])).
% 0.13/0.50 fof(f282,plain,(
% 0.13/0.50 ![X0]: (~frontsegP(nil,X0)|~ssList(X0)|nil=X0)),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f84])).
% 0.13/0.50 fof(f337,plain,(
% 0.13/0.50 ![X0,X1]: (~segmentP(X0,X1)|~segmentP(X1,X0)|~ssList(X0)|~ssList(X1)|X1=X0)),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f127])).
% 0.13/0.50 fof(f341,plain,(
% 0.13/0.50 ![X0,X1]: (~rearsegP(X0,X1)|~ssList(X1)|~ssList(X0)|app(skaf46(X0,X1),X1)=X0)),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f131])).
% 0.13/0.50 fof(f342,plain,(
% 0.13/0.50 ![X0,X1]: (~frontsegP(X0,X1)|~ssList(X1)|~ssList(X0)|app(X1,skaf45(X0,X1))=X0)),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f132])).
% 0.13/0.50 fof(f349,plain,(
% 0.13/0.50 ![X0,X1,X2]: (~frontsegP(X0,X1)|~ssList(X2)|~ssList(X1)|~ssList(X0)|frontsegP(app(X0,X2),X1))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f137])).
% 0.13/0.50 fof(f357,plain,(
% 0.13/0.50 ![U,W]: ((((![V]: (~app(U,V)=W|~ssList(V)))|~ssList(U))|~ssList(W))|frontsegP(W,U))),
% 0.13/0.50 inference(miniscoping,[status(thm)],[f144])).
% 0.13/0.50 fof(f358,plain,(
% 0.13/0.50 ![X0,X1,X2]: (~app(X0,X1)=X2|~ssList(X1)|~ssList(X0)|~ssList(X2)|frontsegP(X2,X0))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f357])).
% 0.13/0.50 fof(f402,plain,(
% 0.13/0.50 ![X0,X1,X2,X3]: (~segmentP(X0,X1)|~ssList(X2)|~ssList(X3)|~ssList(X1)|~ssList(X0)|segmentP(app(app(X3,X0),X2),X1))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f172])).
% 0.13/0.50 fof(f428,plain,(
% 0.13/0.50 ssList(sk1)),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f186])).
% 0.13/0.50 fof(f429,plain,(
% 0.13/0.50 ssList(sk2)),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f187])).
% 0.13/0.50 fof(f432,plain,(
% 0.13/0.50 sk2=sk4),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f190])).
% 0.13/0.50 fof(f433,plain,(
% 0.13/0.50 sk1=sk3),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f191])).
% 0.13/0.50 fof(f434,plain,(
% 0.13/0.50 ![X0]: (~ssList(X0)|~neq(X0,nil)|~segmentP(sk2,X0)|~segmentP(sk1,X0))),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f192])).
% 0.13/0.50 fof(f435,plain,(
% 0.13/0.50 ~nil=sk2|~nil=sk1),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f193])).
% 0.13/0.50 fof(f436,plain,(
% 0.13/0.50 nil=sk4|neq(sk3,nil)),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f194])).
% 0.13/0.50 fof(f437,plain,(
% 0.13/0.50 nil=sk4|frontsegP(sk4,sk3)),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f195])).
% 0.13/0.50 fof(f438,plain,(
% 0.13/0.50 nil=sk3|neq(sk3,nil)),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f196])).
% 0.13/0.50 fof(f439,plain,(
% 0.13/0.50 nil=sk3|frontsegP(sk4,sk3)),
% 0.13/0.50 inference(cnf_transformation,[status(thm)],[f197])).
% 0.13/0.50 fof(f447,definition,(
% 0.13/0.50 sQ2_spl <=> (nil=sk2)),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f450,definition,(
% 0.13/0.50 sQ3_spl <=> (nil=sk1)),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f453,plain,(
% 0.13/0.50 ~sQ2_spl|~sQ3_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f435,f447,f450])).
% 0.13/0.50 fof(f454,definition,(
% 0.13/0.50 sQ4_spl <=> (nil=sk4)),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f455,plain,(
% 0.13/0.50 nil=sk4|~sQ4_spl),
% 0.13/0.50 inference(component_clause,[status(thm)],[f454])).
% 0.13/0.50 fof(f457,definition,(
% 0.13/0.50 sQ5_spl <=> (neq(sk3,nil))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f458,plain,(
% 0.13/0.50 neq(sk3,nil)|~sQ5_spl),
% 0.13/0.50 inference(component_clause,[status(thm)],[f457])).
% 0.13/0.50 fof(f460,plain,(
% 0.13/0.50 sQ4_spl|sQ5_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f436,f454,f457])).
% 0.13/0.50 fof(f461,definition,(
% 0.13/0.50 sQ6_spl <=> (frontsegP(sk4,sk3))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f462,plain,(
% 0.13/0.50 frontsegP(sk4,sk3)|~sQ6_spl),
% 0.13/0.50 inference(component_clause,[status(thm)],[f461])).
% 0.13/0.50 fof(f464,plain,(
% 0.13/0.50 sQ4_spl|sQ6_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f437,f454,f461])).
% 0.13/0.50 fof(f465,definition,(
% 0.13/0.50 sQ7_spl <=> (nil=sk3)),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f466,plain,(
% 0.13/0.50 nil=sk3|~sQ7_spl),
% 0.13/0.50 inference(component_clause,[status(thm)],[f465])).
% 0.13/0.50 fof(f468,plain,(
% 0.13/0.50 sQ7_spl|sQ5_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f438,f465,f457])).
% 0.13/0.50 fof(f469,plain,(
% 0.13/0.50 sQ7_spl|sQ6_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f439,f465,f461])).
% 0.13/0.50 fof(f482,plain,(
% 0.13/0.50 ~segmentP(nil,nil)|nil=nil),
% 0.13/0.50 inference(resolution,[status(thm)],[f278,f205])).
% 0.13/0.50 fof(f483,plain,(
% 0.13/0.50 ~segmentP(nil,sk2)|nil=sk2),
% 0.13/0.50 inference(resolution,[status(thm)],[f278,f429])).
% 0.13/0.50 fof(f484,plain,(
% 0.13/0.50 ~segmentP(nil,sk1)|nil=sk1),
% 0.13/0.50 inference(resolution,[status(thm)],[f278,f428])).
% 0.13/0.50 fof(f485,definition,(
% 0.13/0.50 sQ8_spl <=> (segmentP(nil,nil))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f486,plain,(
% 0.13/0.50 segmentP(nil,nil)|~sQ8_spl),
% 0.13/0.50 inference(component_clause,[status(thm)],[f485])).
% 0.13/0.50 fof(f487,plain,(
% 0.13/0.50 ~segmentP(nil,nil)|sQ8_spl),
% 0.13/0.50 inference(component_clause,[status(thm)],[f485])).
% 0.13/0.50 fof(f488,definition,(
% 0.13/0.50 sQ9_spl <=> (nil=nil)),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f491,plain,(
% 0.13/0.50 ~sQ8_spl|sQ9_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f482,f485,f488])).
% 0.13/0.50 fof(f492,definition,(
% 0.13/0.50 sQ10_spl <=> (segmentP(nil,sk2))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f495,plain,(
% 0.13/0.50 ~sQ10_spl|sQ2_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f483,f492,f447])).
% 0.13/0.50 fof(f496,definition,(
% 0.13/0.50 sQ11_spl <=> (segmentP(nil,sk1))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f498,plain,(
% 0.13/0.50 ~segmentP(nil,sk1)|sQ11_spl),
% 0.13/0.50 inference(component_clause,[status(thm)],[f496])).
% 0.13/0.50 fof(f499,plain,(
% 0.13/0.50 ~sQ11_spl|sQ3_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f484,f496,f450])).
% 0.13/0.50 fof(f517,definition,(
% 0.13/0.50 sQ12_spl <=> (ssList(sk1))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f519,plain,(
% 0.13/0.50 ~ssList(sk1)|sQ12_spl),
% 0.13/0.50 inference(component_clause,[status(thm)],[f517])).
% 0.13/0.50 fof(f524,definition,(
% 0.13/0.50 sQ14_spl <=> (ssList(nil))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f526,plain,(
% 0.13/0.50 ~ssList(nil)|sQ14_spl),
% 0.13/0.50 inference(component_clause,[status(thm)],[f524])).
% 0.13/0.50 fof(f528,plain,(
% 0.13/0.50 $false|sQ12_spl),
% 0.13/0.50 inference(forward_subsumption_resolution,[status(thm)],[f519,f428])).
% 0.13/0.50 fof(f529,plain,(
% 0.13/0.50 sQ12_spl),
% 0.13/0.50 inference(contradiction_clause,[status(thm)],[f528])).
% 0.13/0.50 fof(f532,definition,(
% 0.13/0.50 sQ15_spl <=> (ssList(sk2))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f534,plain,(
% 0.13/0.50 ~ssList(sk2)|sQ15_spl),
% 0.13/0.50 inference(component_clause,[status(thm)],[f532])).
% 0.13/0.50 fof(f540,plain,(
% 0.13/0.50 $false|sQ14_spl),
% 0.13/0.50 inference(forward_subsumption_resolution,[status(thm)],[f526,f205])).
% 0.13/0.50 fof(f541,plain,(
% 0.13/0.50 sQ14_spl),
% 0.13/0.50 inference(contradiction_clause,[status(thm)],[f540])).
% 0.13/0.50 fof(f542,plain,(
% 0.13/0.50 $false|sQ15_spl),
% 0.13/0.50 inference(forward_subsumption_resolution,[status(thm)],[f534,f429])).
% 0.13/0.50 fof(f543,plain,(
% 0.13/0.50 sQ15_spl),
% 0.13/0.50 inference(contradiction_clause,[status(thm)],[f542])).
% 0.13/0.50 fof(f545,plain,(
% 0.13/0.50 ~ssList(nil)|sQ8_spl),
% 0.13/0.50 inference(resolution,[status(thm)],[f487,f253])).
% 0.13/0.50 fof(f549,plain,(
% 0.13/0.50 ~sQ14_spl|sQ8_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f545,f524,f485])).
% 0.13/0.50 fof(f560,plain,(
% 0.13/0.50 ~segmentP(sk1,sk1)|~sQ7_spl|sQ11_spl),
% 0.13/0.50 inference(backward_demodulation,[status(thm)],[f566,f498])).
% 0.13/0.50 fof(f566,plain,(
% 0.13/0.50 nil=sk1|~sQ7_spl),
% 0.13/0.50 inference(forward_demodulation,[status(thm)],[f433,f466])).
% 0.13/0.50 fof(f575,plain,(
% 0.13/0.50 neq(sk1,nil)|~sQ5_spl),
% 0.13/0.50 inference(forward_demodulation,[status(thm)],[f433,f458])).
% 0.13/0.50 fof(f576,plain,(
% 0.13/0.50 frontsegP(sk2,sk3)|~sQ6_spl),
% 0.13/0.50 inference(forward_demodulation,[status(thm)],[f432,f462])).
% 0.13/0.50 fof(f577,plain,(
% 0.13/0.50 frontsegP(sk2,sk1)|~sQ6_spl),
% 0.13/0.50 inference(forward_demodulation,[status(thm)],[f433,f576])).
% 0.13/0.50 fof(f578,plain,(
% 0.13/0.50 ~ssList(sk1)|~segmentP(sk2,sk1)|~segmentP(sk1,sk1)|~sQ5_spl),
% 0.13/0.50 inference(resolution,[status(thm)],[f434,f575])).
% 0.13/0.50 fof(f579,definition,(
% 0.13/0.50 sQ19_spl <=> (segmentP(sk2,sk1))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f582,definition,(
% 0.13/0.50 sQ20_spl <=> (segmentP(sk1,sk1))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f583,plain,(
% 0.13/0.50 segmentP(sk1,sk1)|~sQ20_spl),
% 0.13/0.50 inference(component_clause,[status(thm)],[f582])).
% 0.13/0.50 fof(f584,plain,(
% 0.13/0.50 ~segmentP(sk1,sk1)|sQ20_spl),
% 0.13/0.50 inference(component_clause,[status(thm)],[f582])).
% 0.13/0.50 fof(f585,plain,(
% 0.13/0.50 ~sQ12_spl|~sQ19_spl|~sQ20_spl|~sQ5_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f578,f517,f579,f582,f457])).
% 0.13/0.50 fof(f586,plain,(
% 0.13/0.50 nil=sk2|~sQ4_spl),
% 0.13/0.50 inference(forward_demodulation,[status(thm)],[f432,f455])).
% 0.13/0.50 fof(f591,plain,(
% 0.13/0.50 ~ssList(sk1)|sQ20_spl),
% 0.13/0.50 inference(resolution,[status(thm)],[f584,f254])).
% 0.13/0.50 fof(f596,plain,(
% 0.13/0.50 ~sQ12_spl|sQ20_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f591,f517,f582])).
% 0.13/0.50 fof(f598,plain,(
% 0.13/0.50 ~ssList(sk1)|~sQ7_spl|sQ11_spl),
% 0.13/0.50 inference(resolution,[status(thm)],[f560,f254])).
% 0.13/0.50 fof(f600,plain,(
% 0.13/0.50 ~sQ12_spl|~sQ7_spl|sQ11_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f598,f517,f465,f496])).
% 0.13/0.50 fof(f608,plain,(
% 0.13/0.50 ![X0,X1]: (~ssList(X0)|nil=X0|~app(X0,X1)=nil|~ssList(X1)|~ssList(X0)|~ssList(nil))),
% 0.13/0.50 inference(resolution,[status(thm)],[f282,f358])).
% 0.13/0.50 fof(f610,definition,(
% 0.13/0.50 ![X0,X1]: (sQ23_spl <=> (~ssList(X0)|nil=X0|~app(X0,X1)=nil|~ssList(X1)|~ssList(X0)))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f613,plain,(
% 0.13/0.50 sQ23_spl|~sQ14_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f608,f610,f524])).
% 0.13/0.50 fof(f624,plain,(
% 0.13/0.50 app(nil,nil)=nil),
% 0.13/0.50 inference(resolution,[status(thm)],[f271,f205])).
% 0.13/0.50 fof(f631,plain,(
% 0.13/0.50 app(sk2,nil)=sk2),
% 0.13/0.50 inference(resolution,[status(thm)],[f271,f429])).
% 0.13/0.50 fof(f632,plain,(
% 0.13/0.50 app(sk1,nil)=sk1),
% 0.13/0.50 inference(resolution,[status(thm)],[f271,f428])).
% 0.13/0.50 fof(f633,plain,(
% 0.13/0.50 ![X0]: (~frontsegP(nil,X0)|~ssList(nil)|~ssList(X0)|~ssList(nil)|frontsegP(nil,X0))),
% 0.13/0.50 inference(paramodulation,[status(thm)],[f624,f349])).
% 0.13/0.50 fof(f634,definition,(
% 0.13/0.50 ![X0]: (sQ24_spl <=> (~frontsegP(nil,X0)|~ssList(X0)|frontsegP(nil,X0)))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f637,plain,(
% 0.13/0.50 sQ24_spl|~sQ14_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f633,f634,f524])).
% 0.13/0.50 fof(f638,plain,(
% 0.13/0.50 ![X0]: (~frontsegP(sk2,X0)|~ssList(nil)|~ssList(X0)|~ssList(sk2)|frontsegP(sk2,X0))),
% 0.13/0.50 inference(paramodulation,[status(thm)],[f631,f349])).
% 0.13/0.50 fof(f639,definition,(
% 0.13/0.50 ![X0]: (sQ25_spl <=> (~frontsegP(sk2,X0)|~ssList(X0)|frontsegP(sk2,X0)))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f642,plain,(
% 0.13/0.50 sQ25_spl|~sQ14_spl|~sQ15_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f638,f639,f524,f532])).
% 0.13/0.50 fof(f643,plain,(
% 0.13/0.50 ![X0]: (~frontsegP(sk1,X0)|~ssList(nil)|~ssList(X0)|~ssList(sk1)|frontsegP(sk1,X0))),
% 0.13/0.50 inference(paramodulation,[status(thm)],[f632,f349])).
% 0.13/0.50 fof(f644,definition,(
% 0.13/0.50 ![X0]: (sQ26_spl <=> (~frontsegP(sk1,X0)|~ssList(X0)|frontsegP(sk1,X0)))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f647,plain,(
% 0.13/0.50 sQ26_spl|~sQ14_spl|~sQ12_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f643,f644,f524,f517])).
% 0.13/0.50 fof(f655,plain,(
% 0.13/0.50 app(nil,sk2)=sk2),
% 0.13/0.50 inference(resolution,[status(thm)],[f272,f429])).
% 0.13/0.50 fof(f656,plain,(
% 0.13/0.50 app(nil,sk1)=sk1),
% 0.13/0.50 inference(resolution,[status(thm)],[f272,f428])).
% 0.13/0.50 fof(f657,plain,(
% 0.13/0.50 ![X0]: (~frontsegP(nil,X0)|~ssList(sk2)|~ssList(X0)|~ssList(nil)|frontsegP(sk2,X0))),
% 0.13/0.50 inference(paramodulation,[status(thm)],[f655,f349])).
% 0.13/0.50 fof(f658,definition,(
% 0.13/0.50 ![X0]: (sQ27_spl <=> (~frontsegP(nil,X0)|~ssList(X0)|frontsegP(sk2,X0)))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f661,plain,(
% 0.13/0.50 sQ27_spl|~sQ15_spl|~sQ14_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f657,f658,f532,f524])).
% 0.13/0.50 fof(f662,plain,(
% 0.13/0.50 ![X0]: (~frontsegP(nil,X0)|~ssList(sk1)|~ssList(X0)|~ssList(nil)|frontsegP(sk1,X0))),
% 0.13/0.50 inference(paramodulation,[status(thm)],[f656,f349])).
% 0.13/0.50 fof(f663,definition,(
% 0.13/0.50 ![X0]: (sQ28_spl <=> (~frontsegP(nil,X0)|~ssList(X0)|frontsegP(sk1,X0)))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f666,plain,(
% 0.13/0.50 sQ28_spl|~sQ12_spl|~sQ14_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f662,f663,f517,f524])).
% 0.13/0.50 fof(f684,plain,(
% 0.13/0.50 segmentP(nil,sk2)|~sQ4_spl|~sQ8_spl),
% 0.13/0.50 inference(backward_demodulation,[status(thm)],[f586,f486])).
% 0.13/0.50 fof(f691,plain,(
% 0.13/0.50 sQ10_spl|~sQ4_spl|~sQ8_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f684,f492,f454,f485])).
% 0.13/0.50 fof(f841,plain,(
% 0.13/0.50 ~segmentP(sk1,sk1)|~ssList(sk1)|~ssList(sk1)|sk1=sk1|~sQ20_spl),
% 0.13/0.50 inference(resolution,[status(thm)],[f337,f583])).
% 0.13/0.50 fof(f852,definition,(
% 0.13/0.50 sQ33_spl <=> (sk1=sk1)),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f855,plain,(
% 0.13/0.50 ~sQ20_spl|~sQ12_spl|sQ33_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f841,f582,f517,f852])).
% 0.13/0.50 fof(f916,plain,(
% 0.13/0.50 ![X0]: (~ssList(X0)|~ssList(X0)|app(skaf46(X0,X0),X0)=X0|~ssList(X0))),
% 0.13/0.50 inference(resolution,[status(thm)],[f341,f256])).
% 0.13/0.50 fof(f917,plain,(
% 0.13/0.50 ![X0]: (~ssList(X0)|app(skaf46(X0,X0),X0)=X0)),
% 0.13/0.50 inference(duplicate_literals_removal,[status(thm)],[f916])).
% 0.13/0.50 fof(f926,plain,(
% 0.13/0.50 app(skaf46(sk1,sk1),sk1)=sk1),
% 0.13/0.50 inference(resolution,[status(thm)],[f917,f428])).
% 0.13/0.50 fof(f938,plain,(
% 0.13/0.50 ![X0]: (~frontsegP(skaf46(sk1,sk1),X0)|~ssList(sk1)|~ssList(X0)|~ssList(skaf46(sk1,sk1))|frontsegP(sk1,X0))),
% 0.13/0.50 inference(paramodulation,[status(thm)],[f926,f349])).
% 0.13/0.50 fof(f939,definition,(
% 0.13/0.50 sQ42_spl <=> (ssList(skaf46(sk1,sk1)))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f941,plain,(
% 0.13/0.50 ~ssList(skaf46(sk1,sk1))|sQ42_spl),
% 0.13/0.50 inference(component_clause,[status(thm)],[f939])).
% 0.13/0.50 fof(f943,definition,(
% 0.13/0.50 ![X0]: (sQ43_spl <=> (~frontsegP(skaf46(sk1,sk1),X0)|~ssList(X0)|frontsegP(sk1,X0)))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f946,plain,(
% 0.13/0.50 sQ43_spl|~sQ12_spl|~sQ42_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f938,f943,f517,f939])).
% 0.13/0.50 fof(f948,plain,(
% 0.13/0.50 ~ssList(sk1)|~ssList(sk2)|app(sk1,skaf45(sk2,sk1))=sk2|~sQ6_spl),
% 0.13/0.50 inference(resolution,[status(thm)],[f342,f577])).
% 0.13/0.50 fof(f957,definition,(
% 0.13/0.50 sQ45_spl <=> (app(sk1,skaf45(sk2,sk1))=sk2)),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f958,plain,(
% 0.13/0.50 app(sk1,skaf45(sk2,sk1))=sk2|~sQ45_spl),
% 0.13/0.50 inference(component_clause,[status(thm)],[f957])).
% 0.13/0.50 fof(f960,plain,(
% 0.13/0.50 ~sQ12_spl|~sQ15_spl|sQ45_spl|~sQ6_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f948,f517,f532,f957,f461])).
% 0.13/0.50 fof(f981,definition,(
% 0.13/0.50 sQ47_spl <=> (ssList(skaf45(sk2,sk1)))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f983,plain,(
% 0.13/0.50 ~ssList(skaf45(sk2,sk1))|sQ47_spl),
% 0.13/0.50 inference(component_clause,[status(thm)],[f981])).
% 0.13/0.50 fof(f989,plain,(
% 0.13/0.50 $false|sQ47_spl),
% 0.13/0.50 inference(forward_subsumption_resolution,[status(thm)],[f983,f248])).
% 0.13/0.50 fof(f990,plain,(
% 0.13/0.50 sQ47_spl),
% 0.13/0.50 inference(contradiction_clause,[status(thm)],[f989])).
% 0.13/0.50 fof(f1192,plain,(
% 0.13/0.50 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(sk1)|~ssList(sk1)|segmentP(app(app(X1,sk1),X0),sk1)|~sQ20_spl)),
% 0.13/0.50 inference(resolution,[status(thm)],[f402,f583])).
% 0.13/0.50 fof(f1200,definition,(
% 0.13/0.50 ![X0,X1]: (sQ53_spl <=> (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,sk1),X0),sk1)))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f1201,plain,(
% 0.13/0.50 ![X0,X1]: (~ssList(X0)|~ssList(X1)|segmentP(app(app(X1,sk1),X0),sk1)|~sQ53_spl)),
% 0.13/0.50 inference(component_clause,[status(thm)],[f1200])).
% 0.13/0.50 fof(f1203,plain,(
% 0.13/0.50 sQ53_spl|~sQ12_spl|~sQ20_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f1192,f1200,f517,f582])).
% 0.13/0.50 fof(f1226,plain,(
% 0.13/0.50 ![X0,X1,X2,X3]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~ssList(sk1)|~ssList(app(app(X1,sk1),X0))|segmentP(app(app(X3,app(app(X1,sk1),X0)),X2),sk1)|~sQ53_spl)),
% 0.13/0.50 inference(resolution,[status(thm)],[f1201,f402])).
% 0.13/0.50 fof(f1227,plain,(
% 0.13/0.50 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~segmentP(sk1,app(app(X1,sk1),X0))|~ssList(sk1)|~ssList(app(app(X1,sk1),X0))|app(app(X1,sk1),X0)=sk1|~sQ53_spl)),
% 0.13/0.50 inference(resolution,[status(thm)],[f1201,f337])).
% 0.13/0.50 fof(f1228,plain,(
% 0.13/0.50 ![X0]: (~ssList(X0)|~ssList(skaf46(sk1,sk1))|segmentP(app(sk1,X0),sk1)|~sQ53_spl)),
% 0.13/0.50 inference(paramodulation,[status(thm)],[f926,f1201])).
% 0.13/0.50 fof(f1230,definition,(
% 0.13/0.50 ![X0,X1,X2,X3]: (sQ56_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(X3)|~ssList(app(app(X1,sk1),X0))|segmentP(app(app(X3,app(app(X1,sk1),X0)),X2),sk1)))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f1233,plain,(
% 0.13/0.50 sQ56_spl|~sQ12_spl|~sQ53_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f1226,f1230,f517,f1200])).
% 0.13/0.50 fof(f1234,definition,(
% 0.13/0.50 ![X0,X1]: (sQ57_spl <=> (~ssList(X0)|~ssList(X1)|~segmentP(sk1,app(app(X1,sk1),X0))|~ssList(app(app(X1,sk1),X0))|app(app(X1,sk1),X0)=sk1))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f1237,plain,(
% 0.13/0.50 sQ57_spl|~sQ12_spl|~sQ53_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f1227,f1234,f517,f1200])).
% 0.13/0.50 fof(f1238,definition,(
% 0.13/0.50 ![X0]: (sQ58_spl <=> (~ssList(X0)|segmentP(app(sk1,X0),sk1)))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f1239,plain,(
% 0.13/0.50 ![X0]: (~ssList(X0)|segmentP(app(sk1,X0),sk1)|~sQ58_spl)),
% 0.13/0.50 inference(component_clause,[status(thm)],[f1238])).
% 0.13/0.50 fof(f1241,plain,(
% 0.13/0.50 sQ58_spl|~sQ42_spl|~sQ53_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f1228,f1238,f939,f1200])).
% 0.13/0.50 fof(f1243,plain,(
% 0.13/0.50 $false|sQ42_spl),
% 0.13/0.50 inference(forward_subsumption_resolution,[status(thm)],[f941,f247])).
% 0.13/0.50 fof(f1244,plain,(
% 0.13/0.50 sQ42_spl),
% 0.13/0.50 inference(contradiction_clause,[status(thm)],[f1243])).
% 0.13/0.50 fof(f1245,plain,(
% 0.13/0.50 ![X0,X1,X2]: (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(sk1)|~ssList(app(sk1,X0))|segmentP(app(app(X2,app(sk1,X0)),X1),sk1)|~sQ58_spl)),
% 0.13/0.50 inference(resolution,[status(thm)],[f1239,f402])).
% 0.13/0.50 fof(f1246,plain,(
% 0.13/0.50 ![X0]: (~ssList(X0)|~segmentP(sk1,app(sk1,X0))|~ssList(sk1)|~ssList(app(sk1,X0))|app(sk1,X0)=sk1|~sQ58_spl)),
% 0.13/0.50 inference(resolution,[status(thm)],[f1239,f337])).
% 0.13/0.50 fof(f1248,plain,(
% 0.13/0.50 ~ssList(skaf45(sk2,sk1))|segmentP(sk2,sk1)|~sQ58_spl|~sQ45_spl),
% 0.13/0.50 inference(paramodulation,[status(thm)],[f958,f1239])).
% 0.13/0.50 fof(f1250,definition,(
% 0.13/0.50 ![X0,X1,X2]: (sQ59_spl <=> (~ssList(X0)|~ssList(X1)|~ssList(X2)|~ssList(app(sk1,X0))|segmentP(app(app(X2,app(sk1,X0)),X1),sk1)))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f1253,plain,(
% 0.13/0.50 sQ59_spl|~sQ12_spl|~sQ58_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f1245,f1250,f517,f1238])).
% 0.13/0.50 fof(f1254,definition,(
% 0.13/0.50 ![X0]: (sQ60_spl <=> (~ssList(X0)|~segmentP(sk1,app(sk1,X0))|~ssList(app(sk1,X0))|app(sk1,X0)=sk1))),
% 0.13/0.50 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.13/0.50 fof(f1257,plain,(
% 0.13/0.50 sQ60_spl|~sQ12_spl|~sQ58_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f1246,f1254,f517,f1238])).
% 0.13/0.50 fof(f1259,plain,(
% 0.13/0.50 ~sQ47_spl|sQ19_spl|~sQ58_spl|~sQ45_spl),
% 0.13/0.50 inference(split_clause,[status(thm)],[f1248,f981,f579,f1238,f957])).
% 0.13/0.50 fof(f1261,plain,(
% 0.13/0.50 $false),
% 0.13/0.50 inference(sat_refutation,[status(thm)],[f453,f460,f464,f468,f469,f491,f495,f499,f529,f541,f543,f549,f585,f596,f600,f613,f637,f642,f647,f661,f666,f691,f855,f946,f960,f990,f1203,f1233,f1237,f1241,f1244,f1253,f1257,f1259])).
% 0.13/0.50 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.51 % Elapsed time: 0.155290 seconds
% 0.13/0.51 % CPU time: 0.955707 seconds
% 0.13/0.51 % Total memory used: 127.268 MB
% 0.13/0.51 % Net memory used: 125.980 MB
%------------------------------------------------------------------------------