%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC002-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 : n008.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:18 PM UTC 2026
% Result : Unsatisfiable 0.40s 0.70s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWC002-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.40 % Computer : n008.cluster.edu
% 0.15/0.40 % Model : x86_64 x86_64
% 0.15/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.40 % Memory : 8046.5625MB
% 0.15/0.40 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Mon Sep 21 07:49:24 UTC 2026
% 0.15/0.41 % CPUTime :
% 0.19/0.44 % Drodi V4.1.1
% 0.40/0.70 % Refutation found
% 0.40/0.70 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.40/0.70 % SZS output start CNFRefutation for theBenchmark
% 0.40/0.70 fof(f8,axiom,(
% 0.40/0.70 ssList(nil) ),
% 0.40/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.40/0.70 fof(f115,axiom,(
% 0.40/0.70 (![U,V]: (( U != V| ~ neq(U,V)| ~ ssList(V)| ~ ssList(U) ) ))),
% 0.40/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.40/0.70 fof(f186,negated_conjecture,(
% 0.40/0.70 ssList(sk1) ),
% 0.40/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.40/0.70 fof(f187,negated_conjecture,(
% 0.40/0.70 ssList(sk2) ),
% 0.40/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.40/0.70 fof(f188,negated_conjecture,(
% 0.40/0.70 ssList(sk3) ),
% 0.40/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.40/0.70 fof(f189,negated_conjecture,(
% 0.40/0.70 ssList(sk4) ),
% 0.40/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.40/0.70 fof(f190,negated_conjecture,(
% 0.40/0.70 sk2 = sk4 ),
% 0.40/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.40/0.70 fof(f191,negated_conjecture,(
% 0.40/0.70 sk1 = sk3 ),
% 0.40/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.40/0.70 fof(f192,negated_conjecture,(
% 0.40/0.70 ( neq(sk2,nil)| neq(sk2,nil) ) ),
% 0.40/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.40/0.70 fof(f204,negated_conjecture,(
% 0.40/0.70 (![A,B,C]: (( ~ ssItem(A)| ~ ssList(B)| ~ ssList(C)| app(app(B,cons(A,nil)),C) != sk2| app(B,C) != sk1| ssItem(sk5(C,B,A))| ~ neq(sk4,nil) ) ))),
% 0.40/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.40/0.70 fof(f205,negated_conjecture,(
% 0.40/0.70 (![A,B,C]: (( ~ ssItem(A)| ~ ssList(B)| ~ ssList(C)| app(app(B,cons(A,nil)),C) != sk2| app(B,C) != sk1| memberP(sk2,sk5(C,B,A))| ~ neq(sk4,nil) ) ))),
% 0.40/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.40/0.70 fof(f206,negated_conjecture,(
% 0.40/0.70 (![A,B,C]: (( ~ ssItem(A)| ~ ssList(B)| ~ ssList(C)| app(app(B,cons(A,nil)),C) != sk2| app(B,C) != sk1| geq(sk5(C,B,A),A)| ~ neq(sk4,nil) ) ))),
% 0.40/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.40/0.70 fof(f207,negated_conjecture,(
% 0.40/0.70 (![A,B,C]: (( ~ ssItem(A)| ~ ssList(B)| ~ ssList(C)| app(app(B,cons(A,nil)),C) != sk2| app(B,C) != sk1| A != sk5(C,B,A)| ~ neq(sk4,nil) ) ))),
% 0.40/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.40/0.70 fof(f208,negated_conjecture,(
% 0.40/0.70 ( ssItem(sk6)| ~ neq(sk4,nil) ) ),
% 0.40/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.40/0.70 fof(f209,negated_conjecture,(
% 0.40/0.70 ( ssList(sk7)| ~ neq(sk4,nil) ) ),
% 0.40/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.40/0.70 fof(f210,negated_conjecture,(
% 0.40/0.70 ( ssList(sk8)| ~ neq(sk4,nil) ) ),
% 0.40/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.40/0.70 fof(f211,negated_conjecture,(
% 0.40/0.70 ( app(app(sk7,cons(sk6,nil)),sk8) = sk4| ~ neq(sk4,nil) ) ),
% 0.40/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.40/0.70 fof(f212,negated_conjecture,(
% 0.40/0.70 ( app(sk7,sk8) = sk3| ~ neq(sk4,nil) ) ),
% 0.40/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.40/0.70 fof(f213,negated_conjecture,(
% 0.40/0.70 (![A]: (( ~ ssItem(A)| sk6 = A| ~ memberP(sk4,A)| ~ geq(A,sk6)| ~ neq(sk4,nil) ) ))),
% 0.40/0.70 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.40/0.70 fof(f221,plain,(
% 0.40/0.70 ssList(nil)),
% 0.40/0.70 inference(cnf_transformation,[status(thm)],[f8])).
% 0.40/0.70 fof(f334,plain,(
% 0.40/0.70 ![U]: ((![V]: ((~U=V|~neq(U,V))|~ssList(V)))|~ssList(U))),
% 0.40/0.70 inference(miniscoping,[status(thm)],[f115])).
% 0.40/0.70 fof(f335,plain,(
% 0.40/0.70 ![X0,X1]: (~X0=X1|~neq(X0,X1)|~ssList(X1)|~ssList(X0))),
% 0.40/0.70 inference(cnf_transformation,[status(thm)],[f334])).
% 0.40/0.70 fof(f444,plain,(
% 0.40/0.70 ssList(sk1)),
% 0.40/0.70 inference(cnf_transformation,[status(thm)],[f186])).
% 0.40/0.70 fof(f445,plain,(
% 0.40/0.70 ssList(sk2)),
% 0.40/0.70 inference(cnf_transformation,[status(thm)],[f187])).
% 0.40/0.70 fof(f446,plain,(
% 0.40/0.70 ssList(sk3)),
% 0.40/0.70 inference(cnf_transformation,[status(thm)],[f188])).
% 0.40/0.70 fof(f447,plain,(
% 0.40/0.70 ssList(sk4)),
% 0.40/0.70 inference(cnf_transformation,[status(thm)],[f189])).
% 0.40/0.70 fof(f448,plain,(
% 0.40/0.70 sk2=sk4),
% 0.40/0.70 inference(cnf_transformation,[status(thm)],[f190])).
% 0.40/0.70 fof(f449,plain,(
% 0.40/0.70 sk1=sk3),
% 0.40/0.70 inference(cnf_transformation,[status(thm)],[f191])).
% 0.40/0.70 fof(f450,plain,(
% 0.40/0.70 neq(sk2,nil)|neq(sk2,nil)),
% 0.40/0.70 inference(cnf_transformation,[status(thm)],[f192])).
% 0.40/0.70 fof(f467,plain,(
% 0.40/0.70 (![A,B,C]: (((((~ssItem(A)|~ssList(B))|~ssList(C))|~app(app(B,cons(A,nil)),C)=sk2)|~app(B,C)=sk1)|ssItem(sk5(C,B,A))))|~neq(sk4,nil)),
% 0.40/0.70 inference(miniscoping,[status(thm)],[f204])).
% 0.40/0.70 fof(f468,plain,(
% 0.40/0.70 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sk2|~app(X1,X2)=sk1|ssItem(sk5(X2,X1,X0))|~neq(sk4,nil))),
% 0.40/0.70 inference(cnf_transformation,[status(thm)],[f467])).
% 0.40/0.70 fof(f469,plain,(
% 0.40/0.70 (![A,B,C]: (((((~ssItem(A)|~ssList(B))|~ssList(C))|~app(app(B,cons(A,nil)),C)=sk2)|~app(B,C)=sk1)|memberP(sk2,sk5(C,B,A))))|~neq(sk4,nil)),
% 0.40/0.70 inference(miniscoping,[status(thm)],[f205])).
% 0.40/0.70 fof(f470,plain,(
% 0.40/0.70 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sk2|~app(X1,X2)=sk1|memberP(sk2,sk5(X2,X1,X0))|~neq(sk4,nil))),
% 0.40/0.70 inference(cnf_transformation,[status(thm)],[f469])).
% 0.40/0.70 fof(f471,plain,(
% 0.40/0.70 (![A,B,C]: (((((~ssItem(A)|~ssList(B))|~ssList(C))|~app(app(B,cons(A,nil)),C)=sk2)|~app(B,C)=sk1)|geq(sk5(C,B,A),A)))|~neq(sk4,nil)),
% 0.40/0.70 inference(miniscoping,[status(thm)],[f206])).
% 0.40/0.70 fof(f472,plain,(
% 0.40/0.70 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sk2|~app(X1,X2)=sk1|geq(sk5(X2,X1,X0),X0)|~neq(sk4,nil))),
% 0.40/0.70 inference(cnf_transformation,[status(thm)],[f471])).
% 0.40/0.70 fof(f473,plain,(
% 0.40/0.70 (![A,B,C]: (((((~ssItem(A)|~ssList(B))|~ssList(C))|~app(app(B,cons(A,nil)),C)=sk2)|~app(B,C)=sk1)|~A=sk5(C,B,A)))|~neq(sk4,nil)),
% 0.40/0.70 inference(miniscoping,[status(thm)],[f207])).
% 0.40/0.70 fof(f474,plain,(
% 0.40/0.70 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sk2|~app(X1,X2)=sk1|~X0=sk5(X2,X1,X0)|~neq(sk4,nil))),
% 0.40/0.70 inference(cnf_transformation,[status(thm)],[f473])).
% 0.40/0.70 fof(f475,plain,(
% 0.40/0.70 ssItem(sk6)|~neq(sk4,nil)),
% 0.40/0.70 inference(cnf_transformation,[status(thm)],[f208])).
% 0.40/0.70 fof(f476,plain,(
% 0.40/0.70 ssList(sk7)|~neq(sk4,nil)),
% 0.40/0.70 inference(cnf_transformation,[status(thm)],[f209])).
% 0.40/0.70 fof(f477,plain,(
% 0.40/0.70 ssList(sk8)|~neq(sk4,nil)),
% 0.40/0.70 inference(cnf_transformation,[status(thm)],[f210])).
% 0.40/0.70 fof(f478,plain,(
% 0.40/0.70 app(app(sk7,cons(sk6,nil)),sk8)=sk4|~neq(sk4,nil)),
% 0.40/0.70 inference(cnf_transformation,[status(thm)],[f211])).
% 0.40/0.70 fof(f479,plain,(
% 0.40/0.70 app(sk7,sk8)=sk3|~neq(sk4,nil)),
% 0.40/0.70 inference(cnf_transformation,[status(thm)],[f212])).
% 0.40/0.70 fof(f480,plain,(
% 0.40/0.70 (![A]: (((~ssItem(A)|sk6=A)|~memberP(sk4,A))|~geq(A,sk6)))|~neq(sk4,nil)),
% 0.40/0.70 inference(miniscoping,[status(thm)],[f213])).
% 0.40/0.70 fof(f481,plain,(
% 0.40/0.70 ![X0]: (~ssItem(X0)|sk6=X0|~memberP(sk4,X0)|~geq(X0,sk6)|~neq(sk4,nil))),
% 0.40/0.70 inference(cnf_transformation,[status(thm)],[f480])).
% 0.40/0.70 fof(f489,definition,(
% 0.40/0.70 sQ2_spl <=> (neq(sk2,nil))),
% 0.40/0.70 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.40/0.70 fof(f490,plain,(
% 0.40/0.70 neq(sk2,nil)|~sQ2_spl),
% 0.40/0.70 inference(component_clause,[status(thm)],[f489])).
% 0.40/0.70 fof(f492,plain,(
% 0.40/0.70 sQ2_spl),
% 0.40/0.70 inference(split_clause,[status(thm)],[f450,f489])).
% 0.40/0.70 fof(f493,definition,(
% 0.40/0.70 sQ3_spl <=> (neq(sk4,nil))),
% 0.40/0.70 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.40/0.70 fof(f497,definition,(
% 0.40/0.70 ![X0,X1,X2]: (sQ4_spl <=> (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sk2|~app(X1,X2)=sk1|ssItem(sk5(X2,X1,X0))))),
% 0.40/0.70 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.40/0.70 fof(f498,plain,(
% 0.40/0.70 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sk2|~app(X1,X2)=sk1|ssItem(sk5(X2,X1,X0))|~sQ4_spl)),
% 0.40/0.70 inference(component_clause,[status(thm)],[f497])).
% 0.40/0.70 fof(f501,definition,(
% 0.40/0.70 ![X0,X1,X2]: (sQ5_spl <=> (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sk2|~app(X1,X2)=sk1|memberP(sk2,sk5(X2,X1,X0))))),
% 0.40/0.70 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.40/0.70 fof(f502,plain,(
% 0.40/0.70 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sk2|~app(X1,X2)=sk1|memberP(sk2,sk5(X2,X1,X0))|~sQ5_spl)),
% 0.40/0.70 inference(component_clause,[status(thm)],[f501])).
% 0.40/0.70 fof(f505,definition,(
% 0.40/0.70 ![X0,X1,X2]: (sQ6_spl <=> (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sk2|~app(X1,X2)=sk1|geq(sk5(X2,X1,X0),X0)))),
% 0.40/0.70 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.40/0.70 fof(f506,plain,(
% 0.40/0.70 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sk2|~app(X1,X2)=sk1|geq(sk5(X2,X1,X0),X0)|~sQ6_spl)),
% 0.40/0.70 inference(component_clause,[status(thm)],[f505])).
% 0.40/0.70 fof(f509,definition,(
% 0.40/0.70 ![X0,X1,X2]: (sQ7_spl <=> (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sk2|~app(X1,X2)=sk1|~X0=sk5(X2,X1,X0)))),
% 0.40/0.70 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.40/0.70 fof(f510,plain,(
% 0.40/0.70 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sk2|~app(X1,X2)=sk1|~X0=sk5(X2,X1,X0)|~sQ7_spl)),
% 0.40/0.70 inference(component_clause,[status(thm)],[f509])).
% 0.40/0.70 fof(f513,definition,(
% 0.40/0.70 sQ8_spl <=> (ssItem(sk6))),
% 0.40/0.70 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.40/0.70 fof(f517,definition,(
% 0.40/0.70 sQ9_spl <=> (ssList(sk7))),
% 0.40/0.70 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.40/0.70 fof(f521,definition,(
% 0.40/0.70 sQ10_spl <=> (ssList(sk8))),
% 0.40/0.70 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.40/0.70 fof(f525,definition,(
% 0.40/0.70 sQ11_spl <=> (app(app(sk7,cons(sk6,nil)),sk8)=sk4)),
% 0.40/0.70 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.40/0.70 fof(f526,plain,(
% 0.40/0.70 app(app(sk7,cons(sk6,nil)),sk8)=sk4|~sQ11_spl),
% 0.40/0.70 inference(component_clause,[status(thm)],[f525])).
% 0.40/0.70 fof(f529,definition,(
% 0.40/0.70 sQ12_spl <=> (app(sk7,sk8)=sk3)),
% 0.40/0.70 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.40/0.70 fof(f530,plain,(
% 0.40/0.70 app(sk7,sk8)=sk3|~sQ12_spl),
% 0.40/0.70 inference(component_clause,[status(thm)],[f529])).
% 0.40/0.70 fof(f533,definition,(
% 0.40/0.70 ![X0]: (sQ13_spl <=> (~ssItem(X0)|sk6=X0|~memberP(sk4,X0)|~geq(X0,sk6)))),
% 0.40/0.70 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.40/0.70 fof(f534,plain,(
% 0.40/0.70 ![X0]: (~ssItem(X0)|sk6=X0|~memberP(sk4,X0)|~geq(X0,sk6)|~sQ13_spl)),
% 0.40/0.70 inference(component_clause,[status(thm)],[f533])).
% 0.40/0.70 fof(f537,plain,(
% 0.40/0.70 sQ4_spl|~sQ3_spl),
% 0.40/0.70 inference(split_clause,[status(thm)],[f468,f497,f493])).
% 0.40/0.70 fof(f538,plain,(
% 0.40/0.70 sQ5_spl|~sQ3_spl),
% 0.40/0.70 inference(split_clause,[status(thm)],[f470,f501,f493])).
% 0.40/0.70 fof(f539,plain,(
% 0.40/0.70 sQ6_spl|~sQ3_spl),
% 0.40/0.70 inference(split_clause,[status(thm)],[f472,f505,f493])).
% 0.40/0.70 fof(f540,plain,(
% 0.40/0.70 sQ7_spl|~sQ3_spl),
% 0.40/0.70 inference(split_clause,[status(thm)],[f474,f509,f493])).
% 0.40/0.70 fof(f541,plain,(
% 0.40/0.70 sQ8_spl|~sQ3_spl),
% 0.40/0.70 inference(split_clause,[status(thm)],[f475,f513,f493])).
% 0.40/0.70 fof(f542,plain,(
% 0.40/0.70 sQ9_spl|~sQ3_spl),
% 0.40/0.70 inference(split_clause,[status(thm)],[f476,f517,f493])).
% 0.40/0.70 fof(f543,plain,(
% 0.40/0.70 sQ10_spl|~sQ3_spl),
% 0.40/0.70 inference(split_clause,[status(thm)],[f477,f521,f493])).
% 0.40/0.70 fof(f544,plain,(
% 0.40/0.70 sQ11_spl|~sQ3_spl),
% 0.40/0.70 inference(split_clause,[status(thm)],[f478,f525,f493])).
% 0.40/0.70 fof(f545,plain,(
% 0.40/0.70 sQ12_spl|~sQ3_spl),
% 0.40/0.70 inference(split_clause,[status(thm)],[f479,f529,f493])).
% 0.40/0.70 fof(f546,plain,(
% 0.40/0.70 sQ13_spl|~sQ3_spl),
% 0.40/0.70 inference(split_clause,[status(thm)],[f481,f533,f493])).
% 0.40/0.70 fof(f549,plain,(
% 0.40/0.70 ![X1]: (~neq(X1,X1)|~ssList(X1)|~ssList(X1))),
% 0.40/0.70 inference(destructive_equality_resolution,[status(thm)],[f335])).
% 0.40/0.70 fof(f550,plain,(
% 0.40/0.70 ![X0]: (~neq(X0,X0)|~ssList(X0))),
% 0.40/0.70 inference(duplicate_literals_removal,[status(thm)],[f549])).
% 0.40/0.70 fof(f574,definition,(
% 0.40/0.70 sQ16_spl <=> (ssList(nil))),
% 0.40/0.70 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.40/0.70 fof(f576,plain,(
% 0.40/0.70 ~ssList(nil)|sQ16_spl),
% 0.40/0.70 inference(component_clause,[status(thm)],[f574])).
% 0.40/0.70 fof(f591,plain,(
% 0.40/0.70 $false|sQ16_spl),
% 0.40/0.70 inference(forward_subsumption_resolution,[status(thm)],[f576,f221])).
% 0.40/0.70 fof(f592,plain,(
% 0.40/0.70 sQ16_spl),
% 0.40/0.70 inference(contradiction_clause,[status(thm)],[f591])).
% 0.40/0.70 fof(f606,definition,(
% 0.40/0.70 sQ22_spl <=> (neq(sk2,sk2))),
% 0.40/0.70 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.40/0.70 fof(f607,plain,(
% 0.40/0.70 neq(sk2,sk2)|~sQ22_spl),
% 0.40/0.70 inference(component_clause,[status(thm)],[f606])).
% 0.40/0.70 fof(f634,definition,(
% 0.40/0.70 sQ29_spl <=> (neq(sk1,sk1))),
% 0.40/0.70 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.40/0.70 fof(f635,plain,(
% 0.40/0.70 neq(sk1,sk1)|~sQ29_spl),
% 0.40/0.70 inference(component_clause,[status(thm)],[f634])).
% 0.40/0.70 fof(f948,plain,(
% 0.40/0.70 ~ssList(sk2)|~sQ22_spl),
% 0.40/0.70 inference(resolution,[status(thm)],[f607,f550])).
% 0.40/0.70 fof(f949,plain,(
% 0.40/0.70 $false|~sQ22_spl),
% 0.40/0.70 inference(forward_subsumption_resolution,[status(thm)],[f948,f445])).
% 0.40/0.70 fof(f950,plain,(
% 0.40/0.70 ~sQ22_spl),
% 0.40/0.70 inference(contradiction_clause,[status(thm)],[f949])).
% 0.40/0.70 fof(f952,plain,(
% 0.40/0.70 ~ssList(sk1)|~sQ29_spl),
% 0.40/0.70 inference(resolution,[status(thm)],[f635,f550])).
% 0.40/0.70 fof(f953,plain,(
% 0.40/0.70 $false|~sQ29_spl),
% 0.40/0.70 inference(forward_subsumption_resolution,[status(thm)],[f952,f444])).
% 0.40/0.70 fof(f954,plain,(
% 0.40/0.70 ~sQ29_spl),
% 0.40/0.70 inference(contradiction_clause,[status(thm)],[f953])).
% 0.40/0.70 fof(f1082,definition,(
% 0.40/0.70 sQ128_spl <=> (neq(sk3,sk3))),
% 0.40/0.70 introduced(definition,[new_symbols(definition,[sQ128_spl])],[split_symbol_definition])).
% 0.40/0.70 fof(f1083,plain,(
% 0.40/0.70 neq(sk3,sk3)|~sQ128_spl),
% 0.40/0.70 inference(component_clause,[status(thm)],[f1082])).
% 0.40/0.70 fof(f1102,plain,(
% 0.40/0.70 ~ssList(sk3)|~sQ128_spl),
% 0.40/0.70 inference(resolution,[status(thm)],[f1083,f550])).
% 0.40/0.70 fof(f1103,plain,(
% 0.40/0.70 $false|~sQ128_spl),
% 0.40/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1102,f446])).
% 0.40/0.70 fof(f1104,plain,(
% 0.40/0.70 ~sQ128_spl),
% 0.40/0.70 inference(contradiction_clause,[status(thm)],[f1103])).
% 0.40/0.70 fof(f1248,definition,(
% 0.40/0.70 sQ164_spl <=> (neq(sk4,sk4))),
% 0.40/0.70 introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition])).
% 0.40/0.70 fof(f1249,plain,(
% 0.40/0.70 neq(sk4,sk4)|~sQ164_spl),
% 0.40/0.70 inference(component_clause,[status(thm)],[f1248])).
% 0.40/0.70 fof(f1272,plain,(
% 0.40/0.70 ~ssList(sk4)|~sQ164_spl),
% 0.40/0.70 inference(resolution,[status(thm)],[f1249,f550])).
% 0.40/0.70 fof(f1273,plain,(
% 0.40/0.70 $false|~sQ164_spl),
% 0.40/0.70 inference(forward_subsumption_resolution,[status(thm)],[f1272,f447])).
% 0.40/0.70 fof(f1274,plain,(
% 0.40/0.70 ~sQ164_spl),
% 0.40/0.70 inference(contradiction_clause,[status(thm)],[f1273])).
% 0.40/0.70 fof(f1289,plain,(
% 0.40/0.70 neq(sk4,nil)|~sQ2_spl),
% 0.40/0.70 inference(backward_demodulation,[status(thm)],[f448,f490])).
% 0.40/0.70 fof(f1293,plain,(
% 0.40/0.70 sQ3_spl|~sQ2_spl),
% 0.40/0.70 inference(split_clause,[status(thm)],[f1289,f493,f489])).
% 0.40/0.70 fof(f1294,plain,(
% 0.40/0.70 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sk4|~app(X1,X2)=sk1|ssItem(sk5(X2,X1,X0))|~sQ4_spl)),
% 0.40/0.70 inference(forward_demodulation,[status(thm)],[f448,f498])).
% 0.40/0.70 fof(f1295,plain,(
% 0.40/0.70 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sk4|~app(X1,X2)=sk1|memberP(sk2,sk5(X2,X1,X0))|~sQ5_spl)),
% 0.40/0.70 inference(forward_demodulation,[status(thm)],[f448,f502])).
% 0.40/0.70 fof(f1296,plain,(
% 0.40/0.70 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sk4|~app(X1,X2)=sk1|memberP(sk4,sk5(X2,X1,X0))|~sQ5_spl)),
% 0.40/0.70 inference(forward_demodulation,[status(thm)],[f448,f1295])).
% 0.40/0.70 fof(f1297,plain,(
% 0.40/0.70 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sk4|~app(X1,X2)=sk1|geq(sk5(X2,X1,X0),X0)|~sQ6_spl)),
% 0.40/0.70 inference(forward_demodulation,[status(thm)],[f448,f506])).
% 0.40/0.70 fof(f1298,plain,(
% 0.40/0.70 ![X0,X1,X2]: (~ssItem(X0)|~ssList(X1)|~ssList(X2)|~app(app(X1,cons(X0,nil)),X2)=sk4|~app(X1,X2)=sk1|~X0=sk5(X2,X1,X0)|~sQ7_spl)),
% 0.40/0.70 inference(forward_demodulation,[status(thm)],[f448,f510])).
% 0.40/0.70 fof(f1342,plain,(
% 0.40/0.70 ~ssItem(sk6)|~ssList(sk7)|~ssList(sk8)|~app(sk7,sk8)=sk1|ssItem(sk5(sk8,sk7,sk6))|~sQ4_spl|~sQ11_spl),
% 0.40/0.70 inference(resolution,[status(thm)],[f1294,f526])).
% 0.40/0.70 fof(f1344,definition,(
% 0.40/0.70 sQ176_spl <=> (app(sk7,sk8)=sk1)),
% 0.40/0.70 introduced(definition,[new_symbols(definition,[sQ176_spl])],[split_symbol_definition])).
% 0.40/0.70 fof(f1346,plain,(
% 0.40/0.70 ~app(sk7,sk8)=sk1|sQ176_spl),
% 0.40/0.70 inference(component_clause,[status(thm)],[f1344])).
% 0.40/0.70 fof(f1347,definition,(
% 0.40/0.70 sQ177_spl <=> (ssItem(sk5(sk8,sk7,sk6)))),
% 0.40/0.70 introduced(definition,[new_symbols(definition,[sQ177_spl])],[split_symbol_definition])).
% 0.40/0.70 fof(f1350,plain,(
% 0.40/0.70 ~sQ8_spl|~sQ9_spl|~sQ10_spl|~sQ176_spl|sQ177_spl|~sQ4_spl|~sQ11_spl),
% 0.40/0.70 inference(split_clause,[status(thm)],[f1342,f513,f517,f521,f1344,f1347,f497,f525])).
% 0.40/0.70 fof(f1352,plain,(
% 0.40/0.70 ~ssItem(sk6)|~ssList(sk7)|~ssList(sk8)|~app(sk7,sk8)=sk1|memberP(sk4,sk5(sk8,sk7,sk6))|~sQ5_spl|~sQ11_spl),
% 0.40/0.70 inference(resolution,[status(thm)],[f1296,f526])).
% 0.40/0.70 fof(f1354,definition,(
% 0.40/0.70 sQ178_spl <=> (memberP(sk4,sk5(sk8,sk7,sk6)))),
% 0.40/0.70 introduced(definition,[new_symbols(definition,[sQ178_spl])],[split_symbol_definition])).
% 0.40/0.70 fof(f1357,plain,(
% 0.40/0.70 ~sQ8_spl|~sQ9_spl|~sQ10_spl|~sQ176_spl|sQ178_spl|~sQ5_spl|~sQ11_spl),
% 0.40/0.70 inference(split_clause,[status(thm)],[f1352,f513,f517,f521,f1344,f1354,f501,f525])).
% 0.40/0.72 fof(f1359,plain,(
% 0.40/0.72 ~ssItem(sk6)|~ssList(sk7)|~ssList(sk8)|~app(sk7,sk8)=sk1|geq(sk5(sk8,sk7,sk6),sk6)|~sQ6_spl|~sQ11_spl),
% 0.40/0.72 inference(resolution,[status(thm)],[f1297,f526])).
% 0.40/0.72 fof(f1361,definition,(
% 0.40/0.72 sQ179_spl <=> (geq(sk5(sk8,sk7,sk6),sk6))),
% 0.40/0.72 introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition])).
% 0.40/0.72 fof(f1362,plain,(
% 0.40/0.72 geq(sk5(sk8,sk7,sk6),sk6)|~sQ179_spl),
% 0.40/0.72 inference(component_clause,[status(thm)],[f1361])).
% 0.40/0.72 fof(f1364,plain,(
% 0.40/0.72 ~sQ8_spl|~sQ9_spl|~sQ10_spl|~sQ176_spl|sQ179_spl|~sQ6_spl|~sQ11_spl),
% 0.40/0.72 inference(split_clause,[status(thm)],[f1359,f513,f517,f521,f1344,f1361,f505,f525])).
% 0.40/0.72 fof(f1366,plain,(
% 0.40/0.72 ~ssItem(sk6)|~ssList(sk7)|~ssList(sk8)|~app(sk7,sk8)=sk1|~sk6=sk5(sk8,sk7,sk6)|~sQ7_spl|~sQ11_spl),
% 0.40/0.72 inference(resolution,[status(thm)],[f1298,f526])).
% 0.40/0.72 fof(f1368,definition,(
% 0.40/0.72 sQ180_spl <=> (sk6=sk5(sk8,sk7,sk6))),
% 0.40/0.72 introduced(definition,[new_symbols(definition,[sQ180_spl])],[split_symbol_definition])).
% 0.40/0.72 fof(f1371,plain,(
% 0.40/0.72 ~sQ8_spl|~sQ9_spl|~sQ10_spl|~sQ176_spl|~sQ180_spl|~sQ7_spl|~sQ11_spl),
% 0.40/0.72 inference(split_clause,[status(thm)],[f1366,f513,f517,f521,f1344,f1368,f509,f525])).
% 0.40/0.72 fof(f1702,plain,(
% 0.40/0.72 ~sk3=sk1|~sQ12_spl|sQ176_spl),
% 0.40/0.72 inference(forward_demodulation,[status(thm)],[f530,f1346])).
% 0.40/0.72 fof(f1851,plain,(
% 0.40/0.72 $false|~sQ12_spl|sQ176_spl),
% 0.40/0.72 inference(forward_subsumption_resolution,[status(thm)],[f449,f1702])).
% 0.40/0.72 fof(f1852,plain,(
% 0.40/0.72 ~sQ12_spl|sQ176_spl),
% 0.40/0.72 inference(contradiction_clause,[status(thm)],[f1851])).
% 0.40/0.72 fof(f1957,plain,(
% 0.40/0.72 ~ssItem(sk5(sk8,sk7,sk6))|sk6=sk5(sk8,sk7,sk6)|~memberP(sk4,sk5(sk8,sk7,sk6))|~sQ179_spl|~sQ13_spl),
% 0.40/0.72 inference(resolution,[status(thm)],[f1362,f534])).
% 0.40/0.72 fof(f1958,plain,(
% 0.40/0.72 ~sQ177_spl|sQ180_spl|~sQ178_spl|~sQ179_spl|~sQ13_spl),
% 0.40/0.72 inference(split_clause,[status(thm)],[f1957,f1347,f1368,f1354,f1361,f533])).
% 0.40/0.72 fof(f1959,plain,(
% 0.40/0.72 $false),
% 0.40/0.72 inference(sat_refutation,[status(thm)],[f492,f537,f538,f539,f540,f541,f542,f543,f544,f545,f546,f592,f950,f954,f1104,f1274,f1293,f1350,f1357,f1364,f1371,f1852,f1958])).
% 0.40/0.72 % SZS output end CNFRefutation for theBenchmark.p
% 0.40/0.75 % Elapsed time: 0.318410 seconds
% 0.40/0.75 % CPU time: 1.806344 seconds
% 0.40/0.75 % Total memory used: 135.629 MB
% 0.40/0.75 % Net memory used: 134.326 MB
%------------------------------------------------------------------------------