%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC204-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 : 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:41:51 PM UTC 2026
% Result : Unsatisfiable 30.38s 4.30s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC204-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.33 % Computer : n002.cluster.edu
% 0.08/0.33 % Model : x86_64 x86_64
% 0.08/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.33 % Memory : 8046.5625MB
% 0.08/0.33 % OS : Linux 6.8.0-71-generic
% 0.08/0.33 % CPULimit : 300
% 0.08/0.33 % WCLimit : 300
% 0.08/0.33 % DateTime : Mon Sep 21 08:07:47 UTC 2026
% 0.08/0.33 % CPUTime :
% 0.08/0.35 % Drodi V4.1.1
% 30.38/4.30 % Refutation found
% 30.38/4.30 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 30.38/4.30 % SZS output start CNFRefutation for theBenchmark
% 30.38/4.30 fof(f8,axiom,(
% 30.38/4.30 ssList(nil) ),
% 30.38/4.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.38/4.30 fof(f9,axiom,(
% 30.38/4.30 ssItem(skac3) ),
% 30.38/4.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.38/4.30 fof(f10,axiom,(
% 30.38/4.30 ssItem(skac2) ),
% 30.38/4.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.38/4.30 fof(f13,axiom,(
% 30.38/4.30 (![U]: (ssList(skaf82(U)) ))),
% 30.38/4.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.38/4.30 fof(f74,axiom,(
% 30.38/4.30 (![U]: (( ~ ssList(U)| app(nil,U) = U ) ))),
% 30.38/4.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.38/4.30 fof(f75,axiom,(
% 30.38/4.30 (![U]: (( ~ ssList(U)| ssList(tl(U))| nil = U ) ))),
% 30.38/4.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.38/4.30 fof(f76,axiom,(
% 30.38/4.30 (![U]: (( ~ ssList(U)| ssItem(hd(U))| nil = U ) ))),
% 30.38/4.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.38/4.30 fof(f85,axiom,(
% 30.38/4.30 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| ssList(app(V,U)) ) ))),
% 30.38/4.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.38/4.30 fof(f86,axiom,(
% 30.38/4.30 (![U,V]: (( ~ ssItem(U)| ~ ssList(V)| ssList(cons(U,V)) ) ))),
% 30.38/4.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.38/4.30 fof(f99,axiom,(
% 30.38/4.30 (![U,V]: (( cons(U,V) != V| ~ ssItem(U)| ~ ssList(V) ) ))),
% 30.38/4.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.38/4.30 fof(f100,axiom,(
% 30.38/4.30 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| neq(V,U)| V = U ) ))),
% 30.38/4.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.38/4.30 fof(f104,axiom,(
% 30.38/4.30 (![U]: (( ~ ssList(U)| cons(hd(U),tl(U)) = U| nil = U ) ))),
% 30.38/4.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.38/4.30 fof(f186,negated_conjecture,(
% 30.38/4.30 ssList(sk1) ),
% 30.38/4.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.38/4.30 fof(f187,negated_conjecture,(
% 30.38/4.30 ssList(sk2) ),
% 30.38/4.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.38/4.30 fof(f190,negated_conjecture,(
% 30.38/4.30 sk2 = sk4 ),
% 30.38/4.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.38/4.30 fof(f191,negated_conjecture,(
% 30.38/4.30 sk1 = sk3 ),
% 30.38/4.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.38/4.30 fof(f192,negated_conjecture,(
% 30.38/4.30 ( neq(sk2,nil)| neq(sk2,nil) ) ),
% 30.38/4.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.38/4.30 fof(f196,negated_conjecture,(
% 30.38/4.30 (![A,B]: (( ~ ssList(A)| sk4 = A| ~ ssList(B)| tl(sk4) != B| app(sk3,B) != A| ~ neq(nil,sk4)| ~ neq(sk4,nil) ) ))),
% 30.38/4.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.38/4.30 fof(f197,negated_conjecture,(
% 30.38/4.30 ( ~ neq(sk1,nil)| ~ neq(sk4,nil) ) ),
% 30.38/4.30 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 30.38/4.30 fof(f205,plain,(
% 30.38/4.30 ssList(nil)),
% 30.38/4.30 inference(cnf_transformation,[status(thm)],[f8])).
% 30.38/4.30 fof(f206,plain,(
% 30.38/4.30 ssItem(skac3)),
% 30.38/4.30 inference(cnf_transformation,[status(thm)],[f9])).
% 30.38/4.30 fof(f207,plain,(
% 30.38/4.30 ssItem(skac2)),
% 30.38/4.30 inference(cnf_transformation,[status(thm)],[f10])).
% 30.38/4.30 fof(f210,plain,(
% 30.38/4.30 ![X0]: (ssList(skaf82(X0)))),
% 30.38/4.30 inference(cnf_transformation,[status(thm)],[f13])).
% 30.38/4.30 fof(f272,plain,(
% 30.38/4.30 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 30.38/4.30 inference(cnf_transformation,[status(thm)],[f74])).
% 30.38/4.30 fof(f273,plain,(
% 30.38/4.30 ![X0]: (~ssList(X0)|ssList(tl(X0))|nil=X0)),
% 30.38/4.30 inference(cnf_transformation,[status(thm)],[f75])).
% 30.38/4.30 fof(f274,plain,(
% 30.38/4.30 ![X0]: (~ssList(X0)|ssItem(hd(X0))|nil=X0)),
% 30.38/4.30 inference(cnf_transformation,[status(thm)],[f76])).
% 30.38/4.30 fof(f283,plain,(
% 30.38/4.30 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X1,X0)))),
% 30.38/4.30 inference(cnf_transformation,[status(thm)],[f85])).
% 30.38/4.30 fof(f284,plain,(
% 30.38/4.30 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|ssList(cons(X0,X1)))),
% 30.38/4.30 inference(cnf_transformation,[status(thm)],[f86])).
% 30.38/4.30 fof(f298,plain,(
% 30.38/4.30 ![V]: ((![U]: (~cons(U,V)=V|~ssItem(U)))|~ssList(V))),
% 30.38/4.30 inference(miniscoping,[status(thm)],[f99])).
% 30.38/4.30 fof(f299,plain,(
% 30.38/4.30 ![X0,X1]: (~cons(X0,X1)=X1|~ssItem(X0)|~ssList(X1))),
% 30.38/4.30 inference(cnf_transformation,[status(thm)],[f298])).
% 30.38/4.30 fof(f300,plain,(
% 30.38/4.30 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X1,X0)|X1=X0)),
% 30.38/4.30 inference(cnf_transformation,[status(thm)],[f100])).
% 30.38/4.30 fof(f304,plain,(
% 30.38/4.30 ![X0]: (~ssList(X0)|cons(hd(X0),tl(X0))=X0|nil=X0)),
% 30.38/4.30 inference(cnf_transformation,[status(thm)],[f104])).
% 30.38/4.30 fof(f428,plain,(
% 30.38/4.30 ssList(sk1)),
% 30.38/4.30 inference(cnf_transformation,[status(thm)],[f186])).
% 30.38/4.30 fof(f429,plain,(
% 30.38/4.30 ssList(sk2)),
% 30.38/4.30 inference(cnf_transformation,[status(thm)],[f187])).
% 30.38/4.30 fof(f432,plain,(
% 30.38/4.30 sk2=sk4),
% 30.38/4.30 inference(cnf_transformation,[status(thm)],[f190])).
% 30.38/4.30 fof(f433,plain,(
% 30.38/4.30 sk1=sk3),
% 30.38/4.30 inference(cnf_transformation,[status(thm)],[f191])).
% 30.38/4.30 fof(f434,plain,(
% 30.38/4.30 neq(sk2,nil)|neq(sk2,nil)),
% 30.38/4.30 inference(cnf_transformation,[status(thm)],[f192])).
% 30.38/4.30 fof(f439,plain,(
% 30.38/4.30 ((![A,B]: ((((~ssList(A)|sk4=A)|~ssList(B))|~tl(sk4)=B)|~app(sk3,B)=A))|~neq(nil,sk4))|~neq(sk4,nil)),
% 30.38/4.30 inference(miniscoping,[status(thm)],[f196])).
% 30.38/4.30 fof(f440,plain,(
% 30.38/4.30 ![X0,X1]: (~ssList(X0)|sk4=X0|~ssList(X1)|~tl(sk4)=X1|~app(sk3,X1)=X0|~neq(nil,sk4)|~neq(sk4,nil))),
% 30.38/4.30 inference(cnf_transformation,[status(thm)],[f439])).
% 30.38/4.30 fof(f441,plain,(
% 30.38/4.30 ~neq(sk1,nil)|~neq(sk4,nil)),
% 30.38/4.30 inference(cnf_transformation,[status(thm)],[f197])).
% 30.38/4.30 fof(f449,definition,(
% 30.38/4.30 sQ2_spl <=> (neq(sk2,nil))),
% 30.38/4.30 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 30.38/4.30 fof(f450,plain,(
% 30.38/4.30 neq(sk2,nil)|~sQ2_spl),
% 30.38/4.30 inference(component_clause,[status(thm)],[f449])).
% 30.38/4.30 fof(f452,plain,(
% 30.38/4.30 sQ2_spl),
% 30.38/4.30 inference(split_clause,[status(thm)],[f434,f449])).
% 30.38/4.30 fof(f453,definition,(
% 30.38/4.30 sQ3_spl <=> (neq(sk4,nil))),
% 30.38/4.30 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 30.38/4.30 fof(f455,plain,(
% 30.38/4.30 ~neq(sk4,nil)|sQ3_spl),
% 30.38/4.30 inference(component_clause,[status(thm)],[f453])).
% 30.38/4.30 fof(f457,definition,(
% 30.38/4.30 ![X0,X1]: (sQ4_spl <=> (~ssList(X0)|sk4=X0|~ssList(X1)|~tl(sk4)=X1|~app(sk3,X1)=X0))),
% 30.38/4.30 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 30.38/4.30 fof(f458,plain,(
% 30.38/4.30 ![X0,X1]: (~ssList(X0)|sk4=X0|~ssList(X1)|~tl(sk4)=X1|~app(sk3,X1)=X0|~sQ4_spl)),
% 30.38/4.30 inference(component_clause,[status(thm)],[f457])).
% 30.38/4.30 fof(f460,definition,(
% 30.38/4.30 sQ5_spl <=> (neq(nil,sk4))),
% 30.38/4.30 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 30.38/4.30 fof(f462,plain,(
% 30.38/4.30 ~neq(nil,sk4)|sQ5_spl),
% 30.38/4.30 inference(component_clause,[status(thm)],[f460])).
% 30.38/4.30 fof(f464,definition,(
% 30.38/4.30 sQ6_spl <=> (neq(sk1,nil))),
% 30.38/4.30 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 30.38/4.30 fof(f466,plain,(
% 30.38/4.30 ~neq(sk1,nil)|sQ6_spl),
% 30.38/4.30 inference(component_clause,[status(thm)],[f464])).
% 30.38/4.30 fof(f468,plain,(
% 30.38/4.30 sQ4_spl|~sQ5_spl|~sQ3_spl),
% 30.38/4.30 inference(split_clause,[status(thm)],[f440,f457,f460,f453])).
% 30.38/4.30 fof(f469,plain,(
% 30.38/4.30 ~sQ6_spl|~sQ3_spl),
% 30.38/4.30 inference(split_clause,[status(thm)],[f441,f464,f453])).
% 30.38/4.30 fof(f501,plain,(
% 30.38/4.30 ~neq(sk2,nil)|sQ3_spl),
% 30.38/4.30 inference(forward_demodulation,[status(thm)],[f432,f455])).
% 30.38/4.30 fof(f502,plain,(
% 30.38/4.30 $false|~sQ2_spl|sQ3_spl),
% 30.38/4.30 inference(forward_subsumption_resolution,[status(thm)],[f501,f450])).
% 30.38/4.30 fof(f503,plain,(
% 30.38/4.30 ~sQ2_spl|sQ3_spl),
% 30.38/4.30 inference(contradiction_clause,[status(thm)],[f502])).
% 30.38/4.30 fof(f504,plain,(
% 30.38/4.30 ![X0,X1]: (~ssList(X0)|sk2=X0|~ssList(X1)|~tl(sk4)=X1|~app(sk3,X1)=X0|~sQ4_spl)),
% 30.38/4.30 inference(forward_demodulation,[status(thm)],[f432,f458])).
% 30.38/4.30 fof(f505,plain,(
% 30.38/4.30 ![X0,X1]: (~ssList(X0)|sk2=X0|~ssList(X1)|~tl(sk2)=X1|~app(sk3,X1)=X0|~sQ4_spl)),
% 30.38/4.30 inference(forward_demodulation,[status(thm)],[f432,f504])).
% 30.38/4.30 fof(f506,plain,(
% 30.38/4.30 ![X0,X1]: (~ssList(X0)|sk2=X0|~ssList(X1)|~tl(sk2)=X1|~app(sk1,X1)=X0|~sQ4_spl)),
% 30.38/4.30 inference(forward_demodulation,[status(thm)],[f433,f505])).
% 30.38/4.30 fof(f507,plain,(
% 30.38/4.30 ~ssList(app(sk1,tl(sk2)))|sk2=app(sk1,tl(sk2))|~ssList(tl(sk2))|~sQ4_spl),
% 30.38/4.30 inference(destructive_equality_resolution,[status(thm)],[f506])).
% 30.38/4.30 fof(f535,plain,(
% 30.38/4.30 ~ssList(tl(sk2))|~ssList(sk1)|sk2=app(sk1,tl(sk2))|~ssList(tl(sk2))|~sQ4_spl),
% 30.38/4.30 inference(resolution,[status(thm)],[f283,f507])).
% 30.38/4.30 fof(f547,definition,(
% 30.38/4.30 sQ7_spl <=> (ssList(tl(sk2)))),
% 30.38/4.30 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 30.38/4.30 fof(f548,plain,(
% 30.38/4.30 ssList(tl(sk2))|~sQ7_spl),
% 30.38/4.30 inference(component_clause,[status(thm)],[f547])).
% 30.38/4.30 fof(f549,plain,(
% 30.38/4.30 ~ssList(tl(sk2))|sQ7_spl),
% 30.38/4.30 inference(component_clause,[status(thm)],[f547])).
% 30.38/4.30 fof(f550,definition,(
% 30.38/4.30 sQ8_spl <=> (ssList(sk1))),
% 30.38/4.30 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 30.38/4.30 fof(f552,plain,(
% 30.38/4.30 ~ssList(sk1)|sQ8_spl),
% 30.38/4.30 inference(component_clause,[status(thm)],[f550])).
% 30.38/4.30 fof(f553,definition,(
% 30.38/4.30 sQ9_spl <=> (sk2=app(sk1,tl(sk2)))),
% 30.38/4.30 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 30.38/4.30 fof(f554,plain,(
% 30.38/4.30 sk2=app(sk1,tl(sk2))|~sQ9_spl),
% 30.38/4.30 inference(component_clause,[status(thm)],[f553])).
% 30.38/4.30 fof(f556,plain,(
% 30.38/4.30 ~sQ7_spl|~sQ8_spl|sQ9_spl|~sQ4_spl),
% 30.38/4.30 inference(split_clause,[status(thm)],[f535,f547,f550,f553,f457])).
% 30.38/4.30 fof(f557,definition,(
% 30.38/4.30 sQ10_spl <=> (ssList(nil))),
% 30.38/4.30 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 30.38/4.30 fof(f559,plain,(
% 30.38/4.30 ~ssList(nil)|sQ10_spl),
% 30.38/4.30 inference(component_clause,[status(thm)],[f557])).
% 30.38/4.30 fof(f572,definition,(
% 30.38/4.30 sQ13_spl <=> (ssList(sk2))),
% 30.38/4.30 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 30.38/4.30 fof(f574,plain,(
% 30.38/4.30 ~ssList(sk2)|sQ13_spl),
% 30.38/4.30 inference(component_clause,[status(thm)],[f572])).
% 30.38/4.30 fof(f578,plain,(
% 30.38/4.30 ~neq(nil,sk2)|sQ5_spl),
% 30.38/4.30 inference(forward_demodulation,[status(thm)],[f432,f462])).
% 30.38/4.30 fof(f579,plain,(
% 30.38/4.30 $false|sQ10_spl),
% 30.38/4.30 inference(forward_subsumption_resolution,[status(thm)],[f559,f205])).
% 30.38/4.30 fof(f580,plain,(
% 30.38/4.30 sQ10_spl),
% 30.38/4.30 inference(contradiction_clause,[status(thm)],[f579])).
% 30.38/4.30 fof(f606,plain,(
% 30.38/4.30 ~ssList(sk2)|~ssList(nil)|nil=sk2|sQ5_spl),
% 30.38/4.30 inference(resolution,[status(thm)],[f300,f578])).
% 30.38/4.30 fof(f607,plain,(
% 30.38/4.30 ~ssList(nil)|~ssList(sk1)|sk1=nil|sQ6_spl),
% 30.38/4.30 inference(resolution,[status(thm)],[f300,f466])).
% 30.38/4.30 fof(f610,definition,(
% 30.38/4.30 sQ17_spl <=> (nil=sk2)),
% 30.38/4.30 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 30.38/4.30 fof(f611,plain,(
% 30.38/4.30 nil=sk2|~sQ17_spl),
% 30.38/4.30 inference(component_clause,[status(thm)],[f610])).
% 30.38/4.30 fof(f612,plain,(
% 30.38/4.30 ~nil=sk2|sQ17_spl),
% 30.38/4.30 inference(component_clause,[status(thm)],[f610])).
% 30.38/4.30 fof(f613,plain,(
% 30.38/4.30 ~sQ13_spl|~sQ10_spl|sQ17_spl|sQ5_spl),
% 30.38/4.30 inference(split_clause,[status(thm)],[f606,f572,f557,f610,f460])).
% 30.38/4.30 fof(f614,definition,(
% 30.38/4.30 sQ18_spl <=> (sk1=nil)),
% 30.38/4.30 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 30.38/4.30 fof(f615,plain,(
% 30.38/4.30 sk1=nil|~sQ18_spl),
% 30.38/4.30 inference(component_clause,[status(thm)],[f614])).
% 30.38/4.30 fof(f617,plain,(
% 30.38/4.30 ~sQ10_spl|~sQ8_spl|sQ18_spl|sQ6_spl),
% 30.38/4.30 inference(split_clause,[status(thm)],[f607,f557,f550,f614,f464])).
% 30.38/4.30 fof(f618,plain,(
% 30.38/4.30 $false|sQ8_spl),
% 30.38/4.30 inference(forward_subsumption_resolution,[status(thm)],[f552,f428])).
% 30.38/4.30 fof(f619,plain,(
% 30.38/4.30 sQ8_spl),
% 30.38/4.30 inference(contradiction_clause,[status(thm)],[f618])).
% 30.38/4.30 fof(f624,plain,(
% 30.38/4.30 $false|sQ13_spl),
% 30.38/4.30 inference(forward_subsumption_resolution,[status(thm)],[f574,f429])).
% 30.38/4.30 fof(f625,plain,(
% 30.38/4.30 sQ13_spl),
% 30.38/4.30 inference(contradiction_clause,[status(thm)],[f624])).
% 30.38/4.30 fof(f634,plain,(
% 30.38/4.30 ![X0]: (~ssList(X0)|ssList(tl(X0))|sk1=X0|~sQ18_spl)),
% 30.38/4.30 inference(backward_demodulation,[status(thm)],[f615,f273])).
% 30.38/4.30 fof(f649,plain,(
% 30.38/4.30 ![X0]: (~ssList(X0)|app(sk1,X0)=X0|~sQ18_spl)),
% 30.38/4.30 inference(backward_demodulation,[status(thm)],[f615,f272])).
% 30.38/4.30 fof(f651,plain,(
% 30.38/4.30 ~neq(sk1,sk1)|~sQ18_spl|sQ6_spl),
% 30.38/4.30 inference(backward_demodulation,[status(thm)],[f615,f466])).
% 30.38/4.30 fof(f652,plain,(
% 30.38/4.30 neq(sk2,sk1)|~sQ18_spl|~sQ2_spl),
% 30.38/4.30 inference(backward_demodulation,[status(thm)],[f615,f450])).
% 30.38/4.30 fof(f658,plain,(
% 30.38/4.30 sk1=sk2|~sQ18_spl|~sQ17_spl),
% 30.38/4.30 inference(forward_demodulation,[status(thm)],[f615,f611])).
% 30.38/4.30 fof(f671,plain,(
% 30.38/4.30 neq(sk1,sk1)|~sQ17_spl|~sQ18_spl|~sQ2_spl),
% 30.38/4.30 inference(forward_demodulation,[status(thm)],[f658,f652])).
% 30.38/4.30 fof(f672,plain,(
% 30.38/4.30 $false|sQ6_spl|~sQ17_spl|~sQ18_spl|~sQ2_spl),
% 30.38/4.30 inference(forward_subsumption_resolution,[status(thm)],[f671,f651])).
% 30.38/4.30 fof(f673,plain,(
% 30.38/4.30 sQ6_spl|~sQ17_spl|~sQ18_spl|~sQ2_spl),
% 30.38/4.30 inference(contradiction_clause,[status(thm)],[f672])).
% 30.38/4.30 fof(f674,plain,(
% 30.38/4.30 ~sk1=sk2|~sQ18_spl|sQ17_spl),
% 30.38/4.30 inference(forward_demodulation,[status(thm)],[f615,f612])).
% 30.38/4.30 fof(f683,plain,(
% 30.38/4.30 ![X0]: (~ssList(X0)|cons(hd(X0),tl(X0))=X0|sk1=X0|~sQ18_spl)),
% 30.38/4.30 inference(forward_demodulation,[status(thm)],[f615,f304])).
% 30.38/4.30 fof(f684,plain,(
% 30.38/4.30 cons(hd(sk2),tl(sk2))=sk2|sk1=sk2|~sQ18_spl),
% 30.38/4.30 inference(resolution,[status(thm)],[f683,f429])).
% 30.38/4.30 fof(f697,definition,(
% 30.38/4.30 sQ22_spl <=> (cons(hd(sk2),tl(sk2))=sk2)),
% 30.38/4.30 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 30.38/4.30 fof(f698,plain,(
% 30.38/4.30 cons(hd(sk2),tl(sk2))=sk2|~sQ22_spl),
% 30.38/4.30 inference(component_clause,[status(thm)],[f697])).
% 30.38/4.30 fof(f700,definition,(
% 30.38/4.30 sQ23_spl <=> (sk1=sk2)),
% 30.38/4.30 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 30.38/4.30 fof(f701,plain,(
% 30.38/4.30 sk1=sk2|~sQ23_spl),
% 30.38/4.30 inference(component_clause,[status(thm)],[f700])).
% 30.38/4.30 fof(f703,plain,(
% 30.38/4.30 sQ22_spl|sQ23_spl|~sQ18_spl),
% 30.38/4.30 inference(split_clause,[status(thm)],[f684,f697,f700,f614])).
% 30.38/4.30 fof(f723,plain,(
% 30.38/4.30 ~ssList(sk2)|sk1=sk2|~sQ18_spl|sQ7_spl),
% 30.38/4.30 inference(resolution,[status(thm)],[f634,f549])).
% 30.38/4.30 fof(f725,plain,(
% 30.38/4.30 ~sQ13_spl|sQ23_spl|~sQ18_spl|sQ7_spl),
% 30.38/4.30 inference(split_clause,[status(thm)],[f723,f572,f700,f614,f547])).
% 30.38/4.30 fof(f726,plain,(
% 30.38/4.30 $false|~sQ18_spl|sQ17_spl|~sQ23_spl),
% 30.38/4.30 inference(forward_subsumption_resolution,[status(thm)],[f701,f674])).
% 30.38/4.30 fof(f727,plain,(
% 30.38/4.30 ~sQ18_spl|sQ17_spl|~sQ23_spl),
% 30.38/4.30 inference(contradiction_clause,[status(thm)],[f726])).
% 30.38/4.30 fof(f740,plain,(
% 30.38/4.30 app(sk1,tl(sk2))=tl(sk2)|~sQ18_spl|~sQ7_spl),
% 30.38/4.30 inference(resolution,[status(thm)],[f649,f548])).
% 30.38/4.30 fof(f1541,plain,(
% 30.38/4.30 ![X0]: (~ssList(X0)|ssItem(hd(X0))|sk1=X0|~sQ18_spl)),
% 30.38/4.30 inference(forward_demodulation,[status(thm)],[f615,f274])).
% 30.38/4.30 fof(f1758,plain,(
% 30.38/4.30 ![X0]: (~ssList(X0)|ssList(cons(skac2,X0)))),
% 30.38/4.30 inference(resolution,[status(thm)],[f284,f207])).
% 30.38/4.30 fof(f1759,plain,(
% 30.38/4.30 ![X0]: (~ssList(X0)|ssList(cons(skac3,X0)))),
% 30.38/4.30 inference(resolution,[status(thm)],[f284,f206])).
% 30.38/4.30 fof(f1894,plain,(
% 30.38/4.30 ![X0]: (~cons(skac2,X0)=X0|~ssList(X0))),
% 30.38/4.30 inference(resolution,[status(thm)],[f299,f207])).
% 30.38/4.30 fof(f1929,plain,(
% 30.38/4.30 ~cons(skac2,sk1)=sk1),
% 30.38/4.30 inference(resolution,[status(thm)],[f1894,f428])).
% 30.38/4.30 fof(f1975,definition,(
% 30.38/4.30 sQ57_spl <=> (ssList(cons(skac2,sk2)))),
% 30.38/4.30 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 30.38/4.30 fof(f1977,plain,(
% 30.38/4.30 ~ssList(cons(skac2,sk2))|sQ57_spl),
% 30.38/4.30 inference(component_clause,[status(thm)],[f1975])).
% 30.38/4.30 fof(f1986,definition,(
% 30.38/4.30 sQ60_spl <=> (sk1=cons(skac2,sk1))),
% 30.38/4.30 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 30.38/4.30 fof(f1987,plain,(
% 30.38/4.30 sk1=cons(skac2,sk1)|~sQ60_spl),
% 30.38/4.30 inference(component_clause,[status(thm)],[f1986])).
% 30.38/4.30 fof(f2025,definition,(
% 30.38/4.30 sQ61_spl <=> (ssList(cons(skac3,sk2)))),
% 30.38/4.30 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 30.38/4.30 fof(f2027,plain,(
% 30.38/4.30 ~ssList(cons(skac3,sk2))|sQ61_spl),
% 30.38/4.30 inference(component_clause,[status(thm)],[f2025])).
% 30.38/4.30 fof(f2451,definition,(
% 30.38/4.30 sQ69_spl <=> (ssItem(skac3))),
% 30.38/4.30 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 30.38/4.30 fof(f2453,plain,(
% 30.38/4.30 ~ssItem(skac3)|sQ69_spl),
% 30.38/4.30 inference(component_clause,[status(thm)],[f2451])).
% 30.38/4.30 fof(f2458,definition,(
% 30.38/4.30 sQ71_spl <=> (ssItem(skac2))),
% 30.38/4.30 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 30.38/4.30 fof(f2460,plain,(
% 30.38/4.30 ~ssItem(skac2)|sQ71_spl),
% 30.38/4.30 inference(component_clause,[status(thm)],[f2458])).
% 30.38/4.30 fof(f2465,plain,(
% 30.38/4.30 $false|sQ69_spl),
% 30.38/4.30 inference(forward_subsumption_resolution,[status(thm)],[f2453,f206])).
% 30.38/4.30 fof(f2466,plain,(
% 30.38/4.30 sQ69_spl),
% 30.38/4.30 inference(contradiction_clause,[status(thm)],[f2465])).
% 30.38/4.30 fof(f2467,plain,(
% 30.38/4.30 $false|sQ71_spl),
% 30.38/4.30 inference(forward_subsumption_resolution,[status(thm)],[f2460,f207])).
% 30.38/4.30 fof(f2468,plain,(
% 30.38/4.30 sQ71_spl),
% 30.38/4.30 inference(contradiction_clause,[status(thm)],[f2467])).
% 30.38/4.30 fof(f2595,plain,(
% 30.38/4.30 $false|~sQ60_spl),
% 30.38/4.30 inference(forward_subsumption_resolution,[status(thm)],[f1987,f1929])).
% 30.38/4.30 fof(f2596,plain,(
% 30.38/4.30 ~sQ60_spl),
% 30.38/4.30 inference(contradiction_clause,[status(thm)],[f2595])).
% 30.38/4.30 fof(f3254,definition,(
% 30.38/4.30 sQ112_spl <=> (ssItem(hd(sk2)))),
% 30.38/4.30 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 30.38/4.30 fof(f3255,plain,(
% 30.38/4.30 ssItem(hd(sk2))|~sQ112_spl),
% 30.38/4.30 inference(component_clause,[status(thm)],[f3254])).
% 30.38/4.30 fof(f3256,plain,(
% 30.38/4.30 ~ssItem(hd(sk2))|sQ112_spl),
% 30.38/4.30 inference(component_clause,[status(thm)],[f3254])).
% 30.38/4.30 fof(f3268,plain,(
% 30.38/4.30 ~ssList(sk2)|sk1=sk2|sQ112_spl|~sQ18_spl),
% 30.38/4.30 inference(resolution,[status(thm)],[f3256,f1541])).
% 30.38/4.30 fof(f3269,plain,(
% 30.38/4.30 ~sQ13_spl|sQ23_spl|sQ112_spl|~sQ18_spl),
% 30.38/4.30 inference(split_clause,[status(thm)],[f3268,f572,f700,f3254,f614])).
% 24.35/4.34 fof(f12480,plain,(
% 24.35/4.34 sk2=tl(sk2)|~sQ9_spl|~sQ18_spl|~sQ7_spl),
% 24.35/4.34 inference(forward_demodulation,[status(thm)],[f554,f740])).
% 24.35/4.34 fof(f12511,plain,(
% 24.35/4.34 cons(hd(sk2),sk2)=sk2|~sQ9_spl|~sQ18_spl|~sQ7_spl|~sQ22_spl),
% 24.35/4.34 inference(backward_demodulation,[status(thm)],[f12480,f698])).
% 24.35/4.34 fof(f12556,plain,(
% 24.35/4.34 ![X0]: (~cons(hd(sk2),X0)=X0|~ssList(X0)|~sQ112_spl)),
% 24.35/4.34 inference(resolution,[status(thm)],[f299,f3255])).
% 24.35/4.34 fof(f15310,plain,(
% 24.35/4.34 ssList(cons(skac3,sk2))),
% 24.35/4.34 inference(resolution,[status(thm)],[f1759,f429])).
% 24.35/4.34 fof(f21300,plain,(
% 24.35/4.34 ssList(cons(skac2,sk2))),
% 24.35/4.34 inference(resolution,[status(thm)],[f1758,f429])).
% 24.35/4.34 fof(f21311,plain,(
% 24.35/4.34 ![X0]: (ssList(cons(skac2,skaf82(X0))))),
% 24.35/4.34 inference(resolution,[status(thm)],[f1758,f210])).
% 24.35/4.34 fof(f31651,definition,(
% 24.35/4.34 ![X0]: (sQ621_spl <=> (~app(X0,sk2)=app(X0,sk2)|~ssList(X0)))),
% 24.35/4.34 introduced(definition,[new_symbols(definition,[sQ621_spl])],[split_symbol_definition])).
% 24.35/4.34 fof(f31652,plain,(
% 24.35/4.34 ![X0]: (~app(X0,sk2)=app(X0,sk2)|~ssList(X0)|~sQ621_spl)),
% 24.35/4.34 inference(component_clause,[status(thm)],[f31651])).
% 24.35/4.34 fof(f31662,plain,(
% 24.35/4.34 ![X0]: (~ssList(X0)|~sQ621_spl)),
% 24.35/4.34 inference(trivial_equality_resolution,[status(thm)],[f31652])).
% 24.35/4.34 fof(f31663,plain,(
% 24.35/4.34 $false|~sQ621_spl),
% 24.35/4.34 inference(backward_subsumption_resolution,[status(thm)],[f21311,f31662])).
% 24.35/4.34 fof(f31738,plain,(
% 24.35/4.34 ~sQ621_spl),
% 24.35/4.34 inference(contradiction_clause,[status(thm)],[f31663])).
% 24.35/4.34 fof(f37631,plain,(
% 24.35/4.34 $false|sQ57_spl),
% 24.35/4.34 inference(forward_subsumption_resolution,[status(thm)],[f1977,f21300])).
% 24.35/4.34 fof(f37632,plain,(
% 24.35/4.34 sQ57_spl),
% 24.35/4.34 inference(contradiction_clause,[status(thm)],[f37631])).
% 24.35/4.34 fof(f37633,plain,(
% 24.35/4.34 $false|sQ61_spl),
% 24.35/4.34 inference(forward_subsumption_resolution,[status(thm)],[f2027,f15310])).
% 24.35/4.34 fof(f37634,plain,(
% 24.35/4.34 sQ61_spl),
% 24.35/4.34 inference(contradiction_clause,[status(thm)],[f37633])).
% 24.35/4.34 fof(f48320,plain,(
% 24.35/4.34 ~cons(hd(sk2),sk2)=sk2|~sQ112_spl),
% 24.35/4.34 inference(resolution,[status(thm)],[f12556,f429])).
% 24.35/4.34 fof(f48321,plain,(
% 24.35/4.34 ~sk2=sk2|~sQ9_spl|~sQ18_spl|~sQ7_spl|~sQ22_spl|~sQ112_spl),
% 24.35/4.34 inference(forward_demodulation,[status(thm)],[f12511,f48320])).
% 24.35/4.34 fof(f48322,plain,(
% 24.35/4.34 $false|~sQ9_spl|~sQ18_spl|~sQ7_spl|~sQ22_spl|~sQ112_spl),
% 24.35/4.34 inference(trivial_equality_resolution,[status(thm)],[f48321])).
% 24.35/4.34 fof(f48323,plain,(
% 24.35/4.34 ~sQ9_spl|~sQ18_spl|~sQ7_spl|~sQ22_spl|~sQ112_spl),
% 24.35/4.34 inference(contradiction_clause,[status(thm)],[f48322])).
% 24.35/4.34 fof(f48324,plain,(
% 24.35/4.34 $false),
% 24.35/4.34 inference(sat_refutation,[status(thm)],[f452,f468,f469,f503,f556,f580,f613,f617,f619,f625,f673,f703,f725,f727,f2466,f2468,f2596,f3269,f31738,f37632,f37634,f48323])).
% 24.35/4.34 % SZS output end CNFRefutation for theBenchmark.p
% 24.35/4.35 % Elapsed time: 4.002840 seconds
% 24.35/4.35 % CPU time: 31.397515 seconds
% 24.35/4.35 % Total memory used: 489.279 MB
% 24.35/4.35 % Net memory used: 465.291 MB
%------------------------------------------------------------------------------