%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC378-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 : n004.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:19 PM UTC 2026
% Result : Unsatisfiable 26.39s 3.93s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWC378-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.19/0.44 % Computer : n004.cluster.edu
% 0.19/0.44 % Model : x86_64 x86_64
% 0.19/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.44 % Memory : 8046.5625MB
% 0.19/0.44 % OS : Linux 6.8.0-71-generic
% 0.19/0.44 % CPULimit : 300
% 0.19/0.44 % WCLimit : 300
% 0.19/0.44 % DateTime : Mon Sep 21 08:19:34 UTC 2026
% 0.19/0.44 % CPUTime :
% 0.19/0.47 % Drodi V4.1.1
% 26.39/3.93 % Refutation found
% 26.39/3.93 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 26.39/3.93 % SZS output start CNFRefutation for theBenchmark
% 26.39/3.93 fof(f8,axiom,(
% 26.39/3.93 ssList(nil) ),
% 26.39/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.39/3.93 fof(f14,axiom,(
% 26.39/3.93 (![U]: (ssList(skaf81(U)) ))),
% 26.39/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.39/3.93 fof(f53,axiom,(
% 26.39/3.93 (![U,V]: (ssList(skaf42(U,V)) ))),
% 26.39/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.39/3.93 fof(f85,axiom,(
% 26.39/3.93 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| ssList(app(V,U)) ) ))),
% 26.39/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.39/3.93 fof(f140,axiom,(
% 26.39/3.93 (![U,V,W]: (( ~ memberP(U,V)| ~ ssList(W)| ~ ssList(U)| ~ ssItem(V)| memberP(app(U,W),V) ) ))),
% 26.39/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.39/3.93 fof(f141,axiom,(
% 26.39/3.93 (![U,V,W]: (( ~ memberP(U,V)| ~ ssList(U)| ~ ssList(W)| ~ ssItem(V)| memberP(app(W,U),V) ) ))),
% 26.39/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.39/3.93 fof(f143,axiom,(
% 26.39/3.93 (![U,V,W]: (( app(U,V) != W| ~ ssList(U)| ~ ssList(V)| ~ ssList(W)| rearsegP(W,V) ) ))),
% 26.39/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.39/3.93 fof(f144,axiom,(
% 26.39/3.93 (![U,V,W]: (( app(U,V) != W| ~ ssList(V)| ~ ssList(U)| ~ ssList(W)| frontsegP(W,U) ) ))),
% 26.39/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.39/3.93 fof(f150,axiom,(
% 26.39/3.93 (![U,V,W]: (( app(U,V) != app(U,W)| ~ ssList(V)| ~ ssList(U)| ~ ssList(W)| V = W ) ))),
% 26.39/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.39/3.93 fof(f158,axiom,(
% 26.39/3.93 (![U,V,W]: (( ~ memberP(app(U,V),W)| ~ ssList(V)| ~ ssList(U)| ~ ssItem(W)| memberP(V,W)| memberP(U,W) ) ))),
% 26.39/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.39/3.93 fof(f188,negated_conjecture,(
% 26.39/3.93 ssList(sk3) ),
% 26.39/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.39/3.93 fof(f189,negated_conjecture,(
% 26.39/3.93 ssList(sk4) ),
% 26.39/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.39/3.93 fof(f190,negated_conjecture,(
% 26.39/3.93 sk2 = sk4 ),
% 26.39/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.39/3.93 fof(f191,negated_conjecture,(
% 26.39/3.93 sk1 = sk3 ),
% 26.39/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.39/3.93 fof(f192,negated_conjecture,(
% 26.39/3.93 ssList(sk5) ),
% 26.39/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.39/3.93 fof(f193,negated_conjecture,(
% 26.39/3.93 ssList(sk6) ),
% 26.39/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.39/3.93 fof(f194,negated_conjecture,(
% 26.39/3.93 app(sk5,sk6) = sk4 ),
% 26.39/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.39/3.93 fof(f195,negated_conjecture,(
% 26.39/3.93 app(sk6,sk5) = sk3 ),
% 26.39/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.39/3.93 fof(f196,negated_conjecture,(
% 26.39/3.93 ssItem(sk7) ),
% 26.39/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.39/3.93 fof(f197,negated_conjecture,(
% 26.39/3.93 ( memberP(sk2,sk7)| memberP(sk1,sk7) ) ),
% 26.39/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.39/3.93 fof(f198,negated_conjecture,(
% 26.39/3.93 ( ~ memberP(sk2,sk7)| ~ memberP(sk1,sk7) ) ),
% 26.39/3.93 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 26.39/3.93 fof(f206,plain,(
% 26.39/3.93 ssList(nil)),
% 26.39/3.93 inference(cnf_transformation,[status(thm)],[f8])).
% 26.39/3.93 fof(f212,plain,(
% 26.39/3.93 ![X0]: (ssList(skaf81(X0)))),
% 26.39/3.93 inference(cnf_transformation,[status(thm)],[f14])).
% 26.39/3.93 fof(f251,plain,(
% 26.39/3.93 ![X0,X1]: (ssList(skaf42(X0,X1)))),
% 26.39/3.93 inference(cnf_transformation,[status(thm)],[f53])).
% 26.39/3.93 fof(f284,plain,(
% 26.39/3.93 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X1,X0)))),
% 26.39/3.93 inference(cnf_transformation,[status(thm)],[f85])).
% 26.39/3.93 fof(f353,plain,(
% 26.39/3.93 ![X0,X1,X2]: (~memberP(X0,X1)|~ssList(X2)|~ssList(X0)|~ssItem(X1)|memberP(app(X0,X2),X1))),
% 26.39/3.93 inference(cnf_transformation,[status(thm)],[f140])).
% 26.39/3.93 fof(f354,plain,(
% 26.39/3.93 ![X0,X1,X2]: (~memberP(X0,X1)|~ssList(X0)|~ssList(X2)|~ssItem(X1)|memberP(app(X2,X0),X1))),
% 26.39/3.93 inference(cnf_transformation,[status(thm)],[f141])).
% 26.39/3.93 fof(f356,plain,(
% 26.39/3.93 ![V,W]: ((((![U]: (~app(U,V)=W|~ssList(U)))|~ssList(V))|~ssList(W))|rearsegP(W,V))),
% 26.39/3.93 inference(miniscoping,[status(thm)],[f143])).
% 26.39/3.93 fof(f357,plain,(
% 26.39/3.93 ![X0,X1,X2]: (~app(X0,X1)=X2|~ssList(X0)|~ssList(X1)|~ssList(X2)|rearsegP(X2,X1))),
% 26.39/3.93 inference(cnf_transformation,[status(thm)],[f356])).
% 26.39/3.93 fof(f358,plain,(
% 26.39/3.93 ![U,W]: ((((![V]: (~app(U,V)=W|~ssList(V)))|~ssList(U))|~ssList(W))|frontsegP(W,U))),
% 26.39/3.93 inference(miniscoping,[status(thm)],[f144])).
% 26.39/3.93 fof(f359,plain,(
% 26.39/3.93 ![X0,X1,X2]: (~app(X0,X1)=X2|~ssList(X1)|~ssList(X0)|~ssList(X2)|frontsegP(X2,X0))),
% 26.39/3.93 inference(cnf_transformation,[status(thm)],[f358])).
% 26.39/3.93 fof(f368,plain,(
% 26.39/3.93 ![V,W]: (((![U]: ((~app(U,V)=app(U,W)|~ssList(V))|~ssList(U)))|~ssList(W))|V=W)),
% 26.39/3.93 inference(miniscoping,[status(thm)],[f150])).
% 26.39/3.93 fof(f369,plain,(
% 26.39/3.93 ![X0,X1,X2]: (~app(X0,X1)=app(X0,X2)|~ssList(X1)|~ssList(X0)|~ssList(X2)|X1=X2)),
% 26.39/3.93 inference(cnf_transformation,[status(thm)],[f368])).
% 26.39/3.93 fof(f383,plain,(
% 26.39/3.93 ![U,W]: ((![V]: ((((~memberP(app(U,V),W)|~ssList(V))|~ssList(U))|~ssItem(W))|memberP(V,W)))|memberP(U,W))),
% 26.39/3.93 inference(miniscoping,[status(thm)],[f158])).
% 26.39/3.93 fof(f384,plain,(
% 26.39/3.93 ![X0,X1,X2]: (~memberP(app(X0,X1),X2)|~ssList(X1)|~ssList(X0)|~ssItem(X2)|memberP(X1,X2)|memberP(X0,X2))),
% 26.39/3.93 inference(cnf_transformation,[status(thm)],[f383])).
% 26.39/3.93 fof(f431,plain,(
% 26.39/3.93 ssList(sk3)),
% 26.39/3.93 inference(cnf_transformation,[status(thm)],[f188])).
% 26.39/3.93 fof(f432,plain,(
% 26.39/3.93 ssList(sk4)),
% 26.39/3.93 inference(cnf_transformation,[status(thm)],[f189])).
% 26.39/3.93 fof(f433,plain,(
% 26.39/3.93 sk2=sk4),
% 26.39/3.93 inference(cnf_transformation,[status(thm)],[f190])).
% 26.39/3.93 fof(f434,plain,(
% 26.39/3.93 sk1=sk3),
% 26.39/3.93 inference(cnf_transformation,[status(thm)],[f191])).
% 26.39/3.93 fof(f435,plain,(
% 26.39/3.93 ssList(sk5)),
% 26.39/3.93 inference(cnf_transformation,[status(thm)],[f192])).
% 26.39/3.93 fof(f436,plain,(
% 26.39/3.93 ssList(sk6)),
% 26.39/3.93 inference(cnf_transformation,[status(thm)],[f193])).
% 26.39/3.93 fof(f437,plain,(
% 26.39/3.93 app(sk5,sk6)=sk4),
% 26.39/3.93 inference(cnf_transformation,[status(thm)],[f194])).
% 26.39/3.93 fof(f438,plain,(
% 26.39/3.93 app(sk6,sk5)=sk3),
% 26.39/3.93 inference(cnf_transformation,[status(thm)],[f195])).
% 26.39/3.93 fof(f439,plain,(
% 26.39/3.93 ssItem(sk7)),
% 26.39/3.93 inference(cnf_transformation,[status(thm)],[f196])).
% 26.39/3.93 fof(f440,plain,(
% 26.39/3.93 memberP(sk2,sk7)|memberP(sk1,sk7)),
% 26.39/3.93 inference(cnf_transformation,[status(thm)],[f197])).
% 26.39/3.93 fof(f441,plain,(
% 26.39/3.93 ~memberP(sk2,sk7)|~memberP(sk1,sk7)),
% 26.39/3.93 inference(cnf_transformation,[status(thm)],[f198])).
% 26.39/3.93 fof(f449,definition,(
% 26.39/3.93 sQ2_spl <=> (memberP(sk2,sk7))),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f450,plain,(
% 26.39/3.93 memberP(sk2,sk7)|~sQ2_spl),
% 26.39/3.93 inference(component_clause,[status(thm)],[f449])).
% 26.39/3.93 fof(f451,plain,(
% 26.39/3.93 ~memberP(sk2,sk7)|sQ2_spl),
% 26.39/3.93 inference(component_clause,[status(thm)],[f449])).
% 26.39/3.93 fof(f452,definition,(
% 26.39/3.93 sQ3_spl <=> (memberP(sk1,sk7))),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f453,plain,(
% 26.39/3.93 memberP(sk1,sk7)|~sQ3_spl),
% 26.39/3.93 inference(component_clause,[status(thm)],[f452])).
% 26.39/3.93 fof(f454,plain,(
% 26.39/3.93 ~memberP(sk1,sk7)|sQ3_spl),
% 26.39/3.93 inference(component_clause,[status(thm)],[f452])).
% 26.39/3.93 fof(f455,plain,(
% 26.39/3.93 sQ2_spl|sQ3_spl),
% 26.39/3.93 inference(split_clause,[status(thm)],[f440,f449,f452])).
% 26.39/3.93 fof(f456,plain,(
% 26.39/3.93 ~sQ2_spl|~sQ3_spl),
% 26.39/3.93 inference(split_clause,[status(thm)],[f441,f449,f452])).
% 26.39/3.93 fof(f471,plain,(
% 26.39/3.93 ![X0,X1]: (~ssList(X0)|~ssList(X1)|~ssList(app(X0,X1))|rearsegP(app(X0,X1),X1))),
% 26.39/3.93 inference(destructive_equality_resolution,[status(thm)],[f357])).
% 26.39/3.93 fof(f472,plain,(
% 26.39/3.93 ![X0,X1]: (~ssList(X0)|~ssList(X1)|rearsegP(app(X0,X1),X1))),
% 26.39/3.93 inference(forward_subsumption_resolution,[status(thm)],[f471,f284])).
% 26.39/3.93 fof(f473,plain,(
% 26.39/3.93 ![X1,X0]: (~ssList(X1)|~ssList(X0)|~ssList(app(X0,X1))|frontsegP(app(X0,X1),X0))),
% 26.39/3.93 inference(destructive_equality_resolution,[status(thm)],[f359])).
% 26.39/3.93 fof(f474,plain,(
% 26.39/3.93 ![X0,X1]: (~ssList(X0)|~ssList(X1)|frontsegP(app(X1,X0),X1))),
% 26.39/3.93 inference(forward_subsumption_resolution,[status(thm)],[f473,f284])).
% 26.39/3.93 fof(f491,plain,(
% 26.39/3.93 ~memberP(sk4,sk7)|sQ2_spl),
% 26.39/3.93 inference(forward_demodulation,[status(thm)],[f433,f451])).
% 26.39/3.93 fof(f492,plain,(
% 26.39/3.93 memberP(sk3,sk7)|~sQ3_spl),
% 26.39/3.93 inference(forward_demodulation,[status(thm)],[f434,f453])).
% 26.39/3.93 fof(f493,plain,(
% 26.39/3.93 ~ssList(sk5)|~ssList(sk6)|ssList(sk3)),
% 26.39/3.93 inference(paramodulation,[status(thm)],[f438,f284])).
% 26.39/3.93 fof(f494,plain,(
% 26.39/3.93 ~ssList(sk6)|~ssList(sk5)|ssList(sk4)),
% 26.39/3.93 inference(paramodulation,[status(thm)],[f437,f284])).
% 26.39/3.93 fof(f495,definition,(
% 26.39/3.93 sQ4_spl <=> (ssList(sk5))),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f497,plain,(
% 26.39/3.93 ~ssList(sk5)|sQ4_spl),
% 26.39/3.93 inference(component_clause,[status(thm)],[f495])).
% 26.39/3.93 fof(f498,definition,(
% 26.39/3.93 sQ5_spl <=> (ssList(sk6))),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f500,plain,(
% 26.39/3.93 ~ssList(sk6)|sQ5_spl),
% 26.39/3.93 inference(component_clause,[status(thm)],[f498])).
% 26.39/3.93 fof(f501,definition,(
% 26.39/3.93 sQ6_spl <=> (ssList(sk3))),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f504,plain,(
% 26.39/3.93 ~sQ4_spl|~sQ5_spl|sQ6_spl),
% 26.39/3.93 inference(split_clause,[status(thm)],[f493,f495,f498,f501])).
% 26.39/3.93 fof(f505,definition,(
% 26.39/3.93 sQ7_spl <=> (ssList(sk4))),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f508,plain,(
% 26.39/3.93 ~sQ5_spl|~sQ4_spl|sQ7_spl),
% 26.39/3.93 inference(split_clause,[status(thm)],[f494,f498,f495,f505])).
% 26.39/3.93 fof(f509,plain,(
% 26.39/3.93 $false|sQ4_spl),
% 26.39/3.93 inference(forward_subsumption_resolution,[status(thm)],[f497,f435])).
% 26.39/3.93 fof(f510,plain,(
% 26.39/3.93 sQ4_spl),
% 26.39/3.93 inference(contradiction_clause,[status(thm)],[f509])).
% 26.39/3.93 fof(f511,plain,(
% 26.39/3.93 memberP(sk4,sk7)|~sQ2_spl),
% 26.39/3.93 inference(forward_demodulation,[status(thm)],[f433,f450])).
% 26.39/3.93 fof(f512,plain,(
% 26.39/3.93 ~memberP(sk3,sk7)|sQ3_spl),
% 26.39/3.93 inference(forward_demodulation,[status(thm)],[f434,f454])).
% 26.39/3.93 fof(f513,plain,(
% 26.39/3.93 $false|sQ5_spl),
% 26.39/3.93 inference(forward_subsumption_resolution,[status(thm)],[f500,f436])).
% 26.39/3.93 fof(f514,plain,(
% 26.39/3.93 sQ5_spl),
% 26.39/3.93 inference(contradiction_clause,[status(thm)],[f513])).
% 26.39/3.93 fof(f515,plain,(
% 26.39/3.93 ~ssList(sk6)|~ssList(sk5)|rearsegP(sk3,sk5)),
% 26.39/3.93 inference(paramodulation,[status(thm)],[f438,f472])).
% 26.39/3.93 fof(f516,plain,(
% 26.39/3.93 ~ssList(sk5)|~ssList(sk6)|rearsegP(sk4,sk6)),
% 26.39/3.93 inference(paramodulation,[status(thm)],[f437,f472])).
% 26.39/3.93 fof(f517,definition,(
% 26.39/3.93 sQ8_spl <=> (rearsegP(sk3,sk5))),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f520,plain,(
% 26.39/3.93 ~sQ5_spl|~sQ4_spl|sQ8_spl),
% 26.39/3.93 inference(split_clause,[status(thm)],[f515,f498,f495,f517])).
% 26.39/3.93 fof(f521,definition,(
% 26.39/3.93 sQ9_spl <=> (rearsegP(sk4,sk6))),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f524,plain,(
% 26.39/3.93 ~sQ4_spl|~sQ5_spl|sQ9_spl),
% 26.39/3.93 inference(split_clause,[status(thm)],[f516,f495,f498,f521])).
% 26.39/3.93 fof(f525,plain,(
% 26.39/3.93 ~ssList(sk5)|~ssList(sk6)|frontsegP(sk3,sk6)),
% 26.39/3.93 inference(paramodulation,[status(thm)],[f438,f474])).
% 26.39/3.93 fof(f526,plain,(
% 26.39/3.93 ~ssList(sk6)|~ssList(sk5)|frontsegP(sk4,sk5)),
% 26.39/3.93 inference(paramodulation,[status(thm)],[f437,f474])).
% 26.39/3.93 fof(f527,definition,(
% 26.39/3.93 sQ10_spl <=> (frontsegP(sk3,sk6))),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f530,plain,(
% 26.39/3.93 ~sQ4_spl|~sQ5_spl|sQ10_spl),
% 26.39/3.93 inference(split_clause,[status(thm)],[f525,f495,f498,f527])).
% 26.39/3.93 fof(f531,definition,(
% 26.39/3.93 sQ11_spl <=> (frontsegP(sk4,sk5))),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f534,plain,(
% 26.39/3.93 ~sQ5_spl|~sQ4_spl|sQ11_spl),
% 26.39/3.93 inference(split_clause,[status(thm)],[f526,f498,f495,f531])).
% 26.39/3.93 fof(f537,plain,(
% 26.39/3.93 ![X0,X1]: (~app(X0,X1)=app(X0,nil)|~ssList(X1)|~ssList(X0)|X1=nil)),
% 26.39/3.93 inference(resolution,[status(thm)],[f369,f206])).
% 26.39/3.93 fof(f541,plain,(
% 26.39/3.93 ![X0,X1]: (~app(X0,X1)=app(X0,sk4)|~ssList(X1)|~ssList(X0)|X1=sk4)),
% 26.39/3.93 inference(resolution,[status(thm)],[f369,f432])).
% 26.39/3.93 fof(f542,plain,(
% 26.39/3.93 ![X0,X1]: (~app(X0,X1)=app(X0,sk3)|~ssList(X1)|~ssList(X0)|X1=sk3)),
% 26.39/3.93 inference(resolution,[status(thm)],[f369,f431])).
% 26.39/3.93 fof(f545,plain,(
% 26.39/3.93 ![X0]: (~app(X0,nil)=app(X0,nil)|~ssList(X0)|nil=nil)),
% 26.39/3.93 inference(resolution,[status(thm)],[f537,f206])).
% 26.39/3.93 fof(f551,definition,(
% 26.39/3.93 ![X0]: (sQ12_spl <=> (~app(X0,nil)=app(X0,nil)|~ssList(X0)))),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f552,plain,(
% 26.39/3.93 ![X0]: (~app(X0,nil)=app(X0,nil)|~ssList(X0)|~sQ12_spl)),
% 26.39/3.93 inference(component_clause,[status(thm)],[f551])).
% 26.39/3.93 fof(f554,definition,(
% 26.39/3.93 sQ13_spl <=> (nil=nil)),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f557,plain,(
% 26.39/3.93 sQ12_spl|sQ13_spl),
% 26.39/3.93 inference(split_clause,[status(thm)],[f545,f551,f554])).
% 26.39/3.93 fof(f586,plain,(
% 26.39/3.93 $false|~sQ12_spl),
% 26.39/3.93 inference(backward_subsumption_resolution,[status(thm)],[f212,f618])).
% 26.39/3.93 fof(f618,plain,(
% 26.39/3.93 ![X0]: (~ssList(X0)|~sQ12_spl)),
% 26.39/3.93 inference(trivial_equality_resolution,[status(thm)],[f552])).
% 26.39/3.93 fof(f619,plain,(
% 26.39/3.93 ~sQ12_spl),
% 26.39/3.93 inference(contradiction_clause,[status(thm)],[f586])).
% 26.39/3.93 fof(f634,definition,(
% 26.39/3.93 ![X0]: (sQ22_spl <=> (~app(X0,sk3)=app(X0,sk3)|~ssList(X0)))),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f635,plain,(
% 26.39/3.93 ![X0]: (~app(X0,sk3)=app(X0,sk3)|~ssList(X0)|~sQ22_spl)),
% 26.39/3.93 inference(component_clause,[status(thm)],[f634])).
% 26.39/3.93 fof(f637,definition,(
% 26.39/3.93 sQ23_spl <=> (sk3=sk3)),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f663,plain,(
% 26.39/3.93 $false|~sQ22_spl),
% 26.39/3.93 inference(backward_subsumption_resolution,[status(thm)],[f431,f695])).
% 26.39/3.93 fof(f695,plain,(
% 26.39/3.93 ![X0]: (~ssList(X0)|~sQ22_spl)),
% 26.39/3.93 inference(trivial_equality_resolution,[status(thm)],[f635])).
% 26.39/3.93 fof(f696,plain,(
% 26.39/3.93 ~sQ22_spl),
% 26.39/3.93 inference(contradiction_clause,[status(thm)],[f663])).
% 26.39/3.93 fof(f740,plain,(
% 26.39/3.93 ![X0]: (~ssList(sk3)|~ssList(X0)|sk3=sk3)),
% 26.39/3.93 inference(equality_resolution,[status(thm)],[f542])).
% 26.39/3.93 fof(f749,definition,(
% 26.39/3.93 ![X0]: (sQ32_spl <=> (~ssList(X0)))),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f750,plain,(
% 26.39/3.93 ![X0]: (~ssList(X0)|~sQ32_spl)),
% 26.39/3.93 inference(component_clause,[status(thm)],[f749])).
% 26.39/3.93 fof(f752,plain,(
% 26.39/3.93 ~sQ6_spl|sQ32_spl|sQ23_spl),
% 26.39/3.93 inference(split_clause,[status(thm)],[f740,f501,f749,f637])).
% 26.39/3.93 fof(f841,plain,(
% 26.39/3.93 ![X0]: (~memberP(sk6,X0)|~ssList(sk5)|~ssList(sk6)|~ssItem(X0)|memberP(sk3,X0))),
% 26.39/3.93 inference(paramodulation,[status(thm)],[f438,f353])).
% 26.39/3.93 fof(f845,definition,(
% 26.39/3.93 ![X0]: (sQ33_spl <=> (~memberP(sk6,X0)|~ssItem(X0)|memberP(sk3,X0)))),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f846,plain,(
% 26.39/3.93 ![X0]: (~memberP(sk6,X0)|~ssItem(X0)|memberP(sk3,X0)|~sQ33_spl)),
% 26.39/3.93 inference(component_clause,[status(thm)],[f845])).
% 26.39/3.93 fof(f848,plain,(
% 26.39/3.93 sQ33_spl|~sQ4_spl|~sQ5_spl),
% 26.39/3.93 inference(split_clause,[status(thm)],[f841,f845,f495,f498])).
% 26.39/3.93 fof(f852,plain,(
% 26.39/3.93 ![X0]: (~memberP(sk5,X0)|~ssList(sk6)|~ssList(sk5)|~ssItem(X0)|memberP(sk4,X0))),
% 26.39/3.93 inference(paramodulation,[status(thm)],[f437,f353])).
% 26.39/3.93 fof(f856,definition,(
% 26.39/3.93 ![X0]: (sQ34_spl <=> (~memberP(sk5,X0)|~ssItem(X0)|memberP(sk4,X0)))),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f857,plain,(
% 26.39/3.93 ![X0]: (~memberP(sk5,X0)|~ssItem(X0)|memberP(sk4,X0)|~sQ34_spl)),
% 26.39/3.93 inference(component_clause,[status(thm)],[f856])).
% 26.39/3.93 fof(f859,plain,(
% 26.39/3.93 sQ34_spl|~sQ5_spl|~sQ4_spl),
% 26.39/3.93 inference(split_clause,[status(thm)],[f852,f856,f498,f495])).
% 26.39/3.93 fof(f863,plain,(
% 26.39/3.93 ![X0]: (~memberP(sk6,X0)|~ssList(sk6)|~ssList(sk5)|~ssItem(X0)|memberP(sk4,X0))),
% 26.39/3.93 inference(paramodulation,[status(thm)],[f437,f354])).
% 26.39/3.93 fof(f864,plain,(
% 26.39/3.93 ![X0]: (~memberP(sk5,X0)|~ssList(sk5)|~ssList(sk6)|~ssItem(X0)|memberP(sk3,X0))),
% 26.39/3.93 inference(paramodulation,[status(thm)],[f438,f354])).
% 26.39/3.93 fof(f865,definition,(
% 26.39/3.93 ![X0]: (sQ35_spl <=> (~memberP(sk6,X0)|~ssItem(X0)|memberP(sk4,X0)))),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f866,plain,(
% 26.39/3.93 ![X0]: (~memberP(sk6,X0)|~ssItem(X0)|memberP(sk4,X0)|~sQ35_spl)),
% 26.39/3.93 inference(component_clause,[status(thm)],[f865])).
% 26.39/3.93 fof(f868,plain,(
% 26.39/3.93 sQ35_spl|~sQ5_spl|~sQ4_spl),
% 26.39/3.93 inference(split_clause,[status(thm)],[f863,f865,f498,f495])).
% 26.39/3.93 fof(f869,definition,(
% 26.39/3.93 ![X0]: (sQ36_spl <=> (~memberP(sk5,X0)|~ssItem(X0)|memberP(sk3,X0)))),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f870,plain,(
% 26.39/3.93 ![X0]: (~memberP(sk5,X0)|~ssItem(X0)|memberP(sk3,X0)|~sQ36_spl)),
% 26.39/3.93 inference(component_clause,[status(thm)],[f869])).
% 26.39/3.93 fof(f872,plain,(
% 26.39/3.93 sQ36_spl|~sQ4_spl|~sQ5_spl),
% 26.39/3.93 inference(split_clause,[status(thm)],[f864,f869,f495,f498])).
% 26.39/3.93 fof(f1214,plain,(
% 26.39/3.93 ![X0]: (~memberP(sk4,X0)|~ssList(sk6)|~ssList(sk5)|~ssItem(X0)|memberP(sk6,X0)|memberP(sk5,X0))),
% 26.39/3.93 inference(paramodulation,[status(thm)],[f437,f384])).
% 26.39/3.93 fof(f1215,plain,(
% 26.39/3.93 ![X0]: (~memberP(sk3,X0)|~ssList(sk5)|~ssList(sk6)|~ssItem(X0)|memberP(sk5,X0)|memberP(sk6,X0))),
% 26.39/3.93 inference(paramodulation,[status(thm)],[f438,f384])).
% 26.39/3.93 fof(f1217,definition,(
% 26.39/3.93 ![X0]: (sQ39_spl <=> (~memberP(sk4,X0)|~ssItem(X0)|memberP(sk6,X0)|memberP(sk5,X0)))),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f1218,plain,(
% 26.39/3.93 ![X0]: (~memberP(sk4,X0)|~ssItem(X0)|memberP(sk6,X0)|memberP(sk5,X0)|~sQ39_spl)),
% 26.39/3.93 inference(component_clause,[status(thm)],[f1217])).
% 26.39/3.93 fof(f1220,plain,(
% 26.39/3.93 sQ39_spl|~sQ5_spl|~sQ4_spl),
% 26.39/3.93 inference(split_clause,[status(thm)],[f1214,f1217,f498,f495])).
% 26.39/3.93 fof(f1221,definition,(
% 26.39/3.93 ![X0]: (sQ40_spl <=> (~memberP(sk3,X0)|~ssItem(X0)|memberP(sk5,X0)|memberP(sk6,X0)))),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f1222,plain,(
% 26.39/3.93 ![X0]: (~memberP(sk3,X0)|~ssItem(X0)|memberP(sk5,X0)|memberP(sk6,X0)|~sQ40_spl)),
% 26.39/3.93 inference(component_clause,[status(thm)],[f1221])).
% 26.39/3.93 fof(f1224,plain,(
% 26.39/3.93 sQ40_spl|~sQ4_spl|~sQ5_spl),
% 26.39/3.93 inference(split_clause,[status(thm)],[f1215,f1221,f495,f498])).
% 26.39/3.93 fof(f1258,plain,(
% 26.39/3.93 ![X0]: (~ssList(sk4)|~ssList(X0)|sk4=sk4)),
% 26.39/3.93 inference(equality_resolution,[status(thm)],[f541])).
% 26.39/3.93 fof(f1273,definition,(
% 26.39/3.93 sQ45_spl <=> (sk4=sk4)),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f1276,plain,(
% 26.39/3.93 ~sQ7_spl|sQ32_spl|sQ45_spl),
% 26.39/3.93 inference(split_clause,[status(thm)],[f1258,f505,f749,f1273])).
% 26.39/3.93 fof(f1277,plain,(
% 26.39/3.93 $false|~sQ32_spl),
% 26.39/3.93 inference(backward_subsumption_resolution,[status(thm)],[f251,f750])).
% 26.39/3.93 fof(f1309,plain,(
% 26.39/3.93 ~sQ32_spl),
% 26.39/3.93 inference(contradiction_clause,[status(thm)],[f1277])).
% 26.39/3.93 fof(f1323,plain,(
% 26.39/3.93 ~ssItem(sk7)|memberP(sk6,sk7)|memberP(sk5,sk7)|~sQ39_spl|~sQ2_spl),
% 26.39/3.93 inference(resolution,[status(thm)],[f1218,f511])).
% 26.39/3.93 fof(f1324,definition,(
% 26.39/3.93 sQ46_spl <=> (ssItem(sk7))),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f1326,plain,(
% 26.39/3.93 ~ssItem(sk7)|sQ46_spl),
% 26.39/3.93 inference(component_clause,[status(thm)],[f1324])).
% 26.39/3.93 fof(f1327,definition,(
% 26.39/3.93 sQ47_spl <=> (memberP(sk6,sk7))),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f1328,plain,(
% 26.39/3.93 memberP(sk6,sk7)|~sQ47_spl),
% 26.39/3.93 inference(component_clause,[status(thm)],[f1327])).
% 26.39/3.93 fof(f1330,definition,(
% 26.39/3.93 sQ48_spl <=> (memberP(sk5,sk7))),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f1331,plain,(
% 26.39/3.93 memberP(sk5,sk7)|~sQ48_spl),
% 26.39/3.93 inference(component_clause,[status(thm)],[f1330])).
% 26.39/3.93 fof(f1333,plain,(
% 26.39/3.93 ~sQ46_spl|sQ47_spl|sQ48_spl|~sQ39_spl|~sQ2_spl),
% 26.39/3.93 inference(split_clause,[status(thm)],[f1323,f1324,f1327,f1330,f1217,f449])).
% 26.39/3.93 fof(f1334,plain,(
% 26.39/3.93 ~ssItem(sk7)|memberP(sk4,sk7)|~sQ48_spl|~sQ34_spl),
% 26.39/3.93 inference(resolution,[status(thm)],[f1331,f857])).
% 26.39/3.93 fof(f1335,plain,(
% 26.39/3.93 ~ssItem(sk7)|memberP(sk3,sk7)|~sQ48_spl|~sQ36_spl),
% 26.39/3.93 inference(resolution,[status(thm)],[f1331,f870])).
% 26.39/3.93 fof(f1336,definition,(
% 26.39/3.93 sQ49_spl <=> (memberP(sk4,sk7))),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f1337,plain,(
% 26.39/3.93 memberP(sk4,sk7)|~sQ49_spl),
% 26.39/3.93 inference(component_clause,[status(thm)],[f1336])).
% 26.39/3.93 fof(f1339,plain,(
% 26.39/3.93 ~sQ46_spl|sQ49_spl|~sQ48_spl|~sQ34_spl),
% 26.39/3.93 inference(split_clause,[status(thm)],[f1334,f1324,f1336,f1330,f856])).
% 26.39/3.93 fof(f1340,definition,(
% 26.39/3.93 sQ50_spl <=> (memberP(sk3,sk7))),
% 26.39/3.93 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 26.39/3.93 fof(f1341,plain,(
% 26.39/3.93 memberP(sk3,sk7)|~sQ50_spl),
% 26.39/3.93 inference(component_clause,[status(thm)],[f1340])).
% 26.39/3.93 fof(f1343,plain,(
% 26.39/3.93 ~sQ46_spl|sQ50_spl|~sQ48_spl|~sQ36_spl),
% 26.39/3.93 inference(split_clause,[status(thm)],[f1335,f1324,f1340,f1330,f869])).
% 26.39/3.93 fof(f1344,plain,(
% 26.39/3.93 $false|sQ46_spl),
% 26.39/3.93 inference(forward_subsumption_resolution,[status(thm)],[f1326,f439])).
% 26.39/3.93 fof(f1345,plain,(
% 26.39/3.93 sQ46_spl),
% 26.39/3.93 inference(contradiction_clause,[status(thm)],[f1344])).
% 26.39/3.93 fof(f1346,plain,(
% 26.39/3.93 $false|sQ3_spl|~sQ50_spl),
% 26.39/3.93 inference(forward_subsumption_resolution,[status(thm)],[f1341,f512])).
% 26.39/3.93 fof(f1347,plain,(
% 26.39/3.93 sQ3_spl|~sQ50_spl),
% 26.39/3.93 inference(contradiction_clause,[status(thm)],[f1346])).
% 26.39/3.93 fof(f1428,plain,(
% 26.39/3.93 ~ssItem(sk7)|memberP(sk5,sk7)|memberP(sk6,sk7)|~sQ40_spl|~sQ3_spl),
% 26.39/3.96 inference(resolution,[status(thm)],[f1222,f492])).
% 26.39/3.96 fof(f1429,plain,(
% 26.39/3.96 ~sQ46_spl|sQ48_spl|sQ47_spl|~sQ40_spl|~sQ3_spl),
% 26.39/3.96 inference(split_clause,[status(thm)],[f1428,f1324,f1330,f1327,f1221,f452])).
% 26.39/3.96 fof(f1430,plain,(
% 26.39/3.96 $false|sQ2_spl|~sQ49_spl),
% 26.39/3.96 inference(forward_subsumption_resolution,[status(thm)],[f1337,f491])).
% 26.39/3.96 fof(f1431,plain,(
% 26.39/3.96 sQ2_spl|~sQ49_spl),
% 26.39/3.96 inference(contradiction_clause,[status(thm)],[f1430])).
% 26.39/3.96 fof(f1432,plain,(
% 26.39/3.96 ~ssItem(sk7)|memberP(sk3,sk7)|~sQ47_spl|~sQ33_spl),
% 26.39/3.96 inference(resolution,[status(thm)],[f1328,f846])).
% 26.39/3.96 fof(f1433,plain,(
% 26.39/3.96 ~ssItem(sk7)|memberP(sk4,sk7)|~sQ47_spl|~sQ35_spl),
% 26.39/3.96 inference(resolution,[status(thm)],[f1328,f866])).
% 26.39/3.96 fof(f1434,plain,(
% 26.39/3.96 ~sQ46_spl|sQ50_spl|~sQ47_spl|~sQ33_spl),
% 26.39/3.96 inference(split_clause,[status(thm)],[f1432,f1324,f1340,f1327,f845])).
% 26.39/3.96 fof(f1435,plain,(
% 26.39/3.96 ~sQ46_spl|sQ49_spl|~sQ47_spl|~sQ35_spl),
% 26.39/3.96 inference(split_clause,[status(thm)],[f1433,f1324,f1336,f1327,f865])).
% 26.39/3.96 fof(f1436,plain,(
% 26.39/3.96 $false),
% 26.39/3.96 inference(sat_refutation,[status(thm)],[f455,f456,f504,f508,f510,f514,f520,f524,f530,f534,f557,f619,f696,f752,f848,f859,f868,f872,f1220,f1224,f1276,f1309,f1333,f1339,f1343,f1345,f1347,f1429,f1431,f1434,f1435])).
% 26.39/3.96 % SZS output end CNFRefutation for theBenchmark.p
% 16.50/4.00 % Elapsed time: 3.540719 seconds
% 16.50/4.00 % CPU time: 27.344429 seconds
% 16.50/4.00 % Total memory used: 320.812 MB
% 16.50/4.00 % Net memory used: 306.510 MB
%------------------------------------------------------------------------------