%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC014-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 : n011.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:20 PM UTC 2026
% Result : Unsatisfiable 0.12s 0.43s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC014-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n011.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 07:49:11 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 0.12/0.43 % Refutation found
% 0.12/0.43 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.12/0.43 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.43 fof(f8,axiom,(
% 0.12/0.43 ssList(nil) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f75,axiom,(
% 0.12/0.43 (![U]: (( ~ ssList(U)| ssList(tl(U))| nil = U ) ))),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f85,axiom,(
% 0.12/0.43 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| ssList(app(V,U)) ) ))),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f96,axiom,(
% 0.12/0.43 (![U,V]: (( ~ ssItem(U)| ~ ssList(V)| tl(cons(U,V)) = V ) ))),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f98,axiom,(
% 0.12/0.43 (![U,V]: (( cons(U,V) != nil| ~ ssItem(U)| ~ ssList(V) ) ))),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f100,axiom,(
% 0.12/0.43 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| neq(V,U)| V = U ) ))),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f118,axiom,(
% 0.12/0.43 (![U,V]: (( app(U,V) != nil| ~ ssList(V)| ~ ssList(U)| nil = U ) ))),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f120,axiom,(
% 0.12/0.43 (![U,V]: (( ~ ssItem(U)| ~ ssList(V)| app(cons(U,nil),V) = cons(U,V) ) ))),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f186,negated_conjecture,(
% 0.12/0.43 ssList(sk1) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f189,negated_conjecture,(
% 0.12/0.43 ssList(sk4) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f190,negated_conjecture,(
% 0.12/0.43 sk2 = sk4 ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f191,negated_conjecture,(
% 0.12/0.43 sk1 = sk3 ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f192,negated_conjecture,(
% 0.12/0.43 ( neq(sk2,nil)| neq(sk2,nil) ) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f199,negated_conjecture,(
% 0.12/0.43 (![A,B]: (( ~ ssList(A)| sk2 != A| ~ ssList(B)| tl(sk2) != B| app(sk1,B) != A| ~ neq(nil,sk2)| ~ neq(sk4,nil) ) ))),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f200,negated_conjecture,(
% 0.12/0.43 ( ssItem(sk5)| ~ neq(sk4,nil) ) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f201,negated_conjecture,(
% 0.12/0.43 ( ssList(sk6)| ~ neq(sk4,nil) ) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f202,negated_conjecture,(
% 0.12/0.43 ( cons(sk5,nil) = sk3| ~ neq(sk4,nil) ) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f203,negated_conjecture,(
% 0.12/0.43 ( app(cons(sk5,nil),sk6) = sk4| ~ neq(sk4,nil) ) ),
% 0.12/0.43 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.43 fof(f211,plain,(
% 0.12/0.43 ssList(nil)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f8])).
% 0.12/0.43 fof(f279,plain,(
% 0.12/0.43 ![X0]: (~ssList(X0)|ssList(tl(X0))|nil=X0)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f75])).
% 0.12/0.43 fof(f289,plain,(
% 0.12/0.43 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X1,X0)))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f85])).
% 0.12/0.43 fof(f300,plain,(
% 0.12/0.43 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|tl(cons(X0,X1))=X1)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f96])).
% 0.12/0.43 fof(f302,plain,(
% 0.12/0.43 ![V]: ((![U]: (~cons(U,V)=nil|~ssItem(U)))|~ssList(V))),
% 0.12/0.43 inference(miniscoping,[status(thm)],[f98])).
% 0.12/0.43 fof(f303,plain,(
% 0.12/0.43 ![X0,X1]: (~cons(X0,X1)=nil|~ssItem(X0)|~ssList(X1))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f302])).
% 0.12/0.43 fof(f306,plain,(
% 0.12/0.43 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X1,X0)|X1=X0)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f100])).
% 0.12/0.43 fof(f330,plain,(
% 0.12/0.43 ![U]: (((![V]: (~app(U,V)=nil|~ssList(V)))|~ssList(U))|nil=U)),
% 0.12/0.43 inference(miniscoping,[status(thm)],[f118])).
% 0.12/0.43 fof(f331,plain,(
% 0.12/0.43 ![X0,X1]: (~app(X0,X1)=nil|~ssList(X1)|~ssList(X0)|nil=X0)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f330])).
% 0.12/0.43 fof(f334,plain,(
% 0.12/0.43 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|app(cons(X0,nil),X1)=cons(X0,X1))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f120])).
% 0.12/0.43 fof(f434,plain,(
% 0.12/0.43 ssList(sk1)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f186])).
% 0.12/0.43 fof(f437,plain,(
% 0.12/0.43 ssList(sk4)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f189])).
% 0.12/0.43 fof(f438,plain,(
% 0.12/0.43 sk2=sk4),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f190])).
% 0.12/0.43 fof(f439,plain,(
% 0.12/0.43 sk1=sk3),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f191])).
% 0.12/0.43 fof(f440,plain,(
% 0.12/0.43 neq(sk2,nil)|neq(sk2,nil)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f192])).
% 0.12/0.43 fof(f448,plain,(
% 0.12/0.43 ((![A,B]: ((((~ssList(A)|~sk2=A)|~ssList(B))|~tl(sk2)=B)|~app(sk1,B)=A))|~neq(nil,sk2))|~neq(sk4,nil)),
% 0.12/0.43 inference(miniscoping,[status(thm)],[f199])).
% 0.12/0.43 fof(f449,plain,(
% 0.12/0.43 ![X0,X1]: (~ssList(X0)|~sk2=X0|~ssList(X1)|~tl(sk2)=X1|~app(sk1,X1)=X0|~neq(nil,sk2)|~neq(sk4,nil))),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f448])).
% 0.12/0.43 fof(f450,plain,(
% 0.12/0.43 ssItem(sk5)|~neq(sk4,nil)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f200])).
% 0.12/0.43 fof(f451,plain,(
% 0.12/0.43 ssList(sk6)|~neq(sk4,nil)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f201])).
% 0.12/0.43 fof(f452,plain,(
% 0.12/0.43 cons(sk5,nil)=sk3|~neq(sk4,nil)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f202])).
% 0.12/0.43 fof(f453,plain,(
% 0.12/0.43 app(cons(sk5,nil),sk6)=sk4|~neq(sk4,nil)),
% 0.12/0.43 inference(cnf_transformation,[status(thm)],[f203])).
% 0.12/0.43 fof(f461,definition,(
% 0.12/0.43 sQ2_spl <=> (neq(sk2,nil))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f462,plain,(
% 0.12/0.43 neq(sk2,nil)|~sQ2_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f461])).
% 0.12/0.43 fof(f464,plain,(
% 0.12/0.43 sQ2_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f440,f461])).
% 0.12/0.43 fof(f465,definition,(
% 0.12/0.43 sQ3_spl <=> (neq(sk4,nil))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f467,plain,(
% 0.12/0.43 ~neq(sk4,nil)|sQ3_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f465])).
% 0.12/0.43 fof(f469,definition,(
% 0.12/0.43 ![X0,X1]: (sQ4_spl <=> (~ssList(X0)|~sk2=X0|~ssList(X1)|~tl(sk2)=X1|~app(sk1,X1)=X0))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f470,plain,(
% 0.12/0.43 ![X0,X1]: (~ssList(X0)|~sk2=X0|~ssList(X1)|~tl(sk2)=X1|~app(sk1,X1)=X0|~sQ4_spl)),
% 0.12/0.43 inference(component_clause,[status(thm)],[f469])).
% 0.12/0.43 fof(f472,definition,(
% 0.12/0.43 sQ5_spl <=> (neq(nil,sk2))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f474,plain,(
% 0.12/0.43 ~neq(nil,sk2)|sQ5_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f472])).
% 0.12/0.43 fof(f476,definition,(
% 0.12/0.43 sQ6_spl <=> (ssItem(sk5))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f477,plain,(
% 0.12/0.43 ssItem(sk5)|~sQ6_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f476])).
% 0.12/0.43 fof(f480,definition,(
% 0.12/0.43 sQ7_spl <=> (ssList(sk6))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f481,plain,(
% 0.12/0.43 ssList(sk6)|~sQ7_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f480])).
% 0.12/0.43 fof(f484,definition,(
% 0.12/0.43 sQ8_spl <=> (cons(sk5,nil)=sk3)),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f485,plain,(
% 0.12/0.43 cons(sk5,nil)=sk3|~sQ8_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f484])).
% 0.12/0.43 fof(f488,definition,(
% 0.12/0.43 sQ9_spl <=> (app(cons(sk5,nil),sk6)=sk4)),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f489,plain,(
% 0.12/0.43 app(cons(sk5,nil),sk6)=sk4|~sQ9_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f488])).
% 0.12/0.43 fof(f492,plain,(
% 0.12/0.43 sQ4_spl|~sQ5_spl|~sQ3_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f449,f469,f472,f465])).
% 0.12/0.43 fof(f493,plain,(
% 0.12/0.43 sQ6_spl|~sQ3_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f450,f476,f465])).
% 0.12/0.43 fof(f494,plain,(
% 0.12/0.43 sQ7_spl|~sQ3_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f451,f480,f465])).
% 0.12/0.43 fof(f495,plain,(
% 0.12/0.43 sQ8_spl|~sQ3_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f452,f484,f465])).
% 0.12/0.43 fof(f496,plain,(
% 0.12/0.43 sQ9_spl|~sQ3_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f453,f488,f465])).
% 0.12/0.43 fof(f528,plain,(
% 0.12/0.43 neq(sk4,nil)|~sQ2_spl),
% 0.12/0.43 inference(forward_demodulation,[status(thm)],[f438,f462])).
% 0.12/0.43 fof(f529,plain,(
% 0.12/0.43 $false|~sQ2_spl|sQ3_spl),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f467,f528])).
% 0.12/0.43 fof(f530,plain,(
% 0.12/0.43 ~sQ2_spl|sQ3_spl),
% 0.12/0.43 inference(contradiction_clause,[status(thm)],[f529])).
% 0.12/0.43 fof(f531,plain,(
% 0.12/0.43 cons(sk5,nil)=sk1|~sQ8_spl),
% 0.12/0.43 inference(forward_demodulation,[status(thm)],[f439,f485])).
% 0.12/0.43 fof(f532,plain,(
% 0.12/0.43 ![X0,X1]: (~ssList(X0)|~sk4=X0|~ssList(X1)|~tl(sk2)=X1|~app(sk1,X1)=X0|~sQ4_spl)),
% 0.12/0.43 inference(forward_demodulation,[status(thm)],[f438,f470])).
% 0.12/0.43 fof(f533,plain,(
% 0.12/0.43 ![X0,X1]: (~ssList(X0)|~sk4=X0|~ssList(X1)|~tl(sk4)=X1|~app(sk1,X1)=X0|~sQ4_spl)),
% 0.12/0.43 inference(forward_demodulation,[status(thm)],[f438,f532])).
% 0.12/0.43 fof(f534,plain,(
% 0.12/0.43 ~ssList(sk4)|~ssList(tl(sk4))|~app(sk1,tl(sk4))=sk4|~sQ4_spl),
% 0.12/0.43 inference(destructive_equality_resolution,[status(thm)],[f533])).
% 0.12/0.43 fof(f535,plain,(
% 0.12/0.43 ~ssList(tl(sk4))|~app(sk1,tl(sk4))=sk4|~sQ4_spl),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f534,f437])).
% 0.12/0.43 fof(f546,plain,(
% 0.12/0.43 app(sk1,sk6)=sk4|~sQ8_spl|~sQ9_spl),
% 0.12/0.43 inference(forward_demodulation,[status(thm)],[f531,f489])).
% 0.12/0.43 fof(f565,plain,(
% 0.12/0.43 ~app(sk1,tl(sk4))=sk4|~ssList(sk4)|nil=sk4|~sQ4_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f535,f279])).
% 0.12/0.43 fof(f566,definition,(
% 0.12/0.43 sQ10_spl <=> (app(sk1,tl(sk4))=sk4)),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f568,plain,(
% 0.12/0.43 ~app(sk1,tl(sk4))=sk4|sQ10_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f566])).
% 0.12/0.43 fof(f569,definition,(
% 0.12/0.43 sQ11_spl <=> (ssList(sk4))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f572,definition,(
% 0.12/0.43 sQ12_spl <=> (nil=sk4)),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f575,plain,(
% 0.12/0.43 ~sQ10_spl|~sQ11_spl|sQ12_spl|~sQ4_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f565,f566,f569,f572,f469])).
% 0.12/0.43 fof(f576,plain,(
% 0.12/0.43 ~neq(nil,sk4)|sQ5_spl),
% 0.12/0.43 inference(forward_demodulation,[status(thm)],[f438,f474])).
% 0.12/0.43 fof(f600,plain,(
% 0.12/0.43 ~ssList(sk6)|~ssList(sk1)|ssList(sk4)|~sQ8_spl|~sQ9_spl),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f546,f289])).
% 0.12/0.43 fof(f601,definition,(
% 0.12/0.43 sQ13_spl <=> (ssList(sk1))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f603,plain,(
% 0.12/0.43 ~ssList(sk1)|sQ13_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f601])).
% 0.12/0.43 fof(f604,plain,(
% 0.12/0.43 ~sQ7_spl|~sQ13_spl|sQ11_spl|~sQ8_spl|~sQ9_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f600,f480,f601,f569,f484,f488])).
% 0.12/0.43 fof(f605,plain,(
% 0.12/0.43 $false|sQ13_spl),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f603,f434])).
% 0.12/0.43 fof(f606,plain,(
% 0.12/0.43 sQ13_spl),
% 0.12/0.43 inference(contradiction_clause,[status(thm)],[f605])).
% 0.12/0.43 fof(f616,definition,(
% 0.12/0.43 sQ15_spl <=> (ssList(nil))),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f618,plain,(
% 0.12/0.43 ~ssList(nil)|sQ15_spl),
% 0.12/0.43 inference(component_clause,[status(thm)],[f616])).
% 0.12/0.43 fof(f636,plain,(
% 0.12/0.43 ![X0]: (~ssList(X0)|tl(cons(sk5,X0))=X0|~sQ6_spl)),
% 0.12/0.43 inference(resolution,[status(thm)],[f300,f477])).
% 0.12/0.43 fof(f637,plain,(
% 0.12/0.43 ~sk1=nil|~ssItem(sk5)|~ssList(nil)|~sQ8_spl),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f531,f303])).
% 0.12/0.43 fof(f638,definition,(
% 0.12/0.43 sQ16_spl <=> (sk1=nil)),
% 0.12/0.43 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.12/0.43 fof(f641,plain,(
% 0.12/0.43 ~sQ16_spl|~sQ6_spl|~sQ15_spl|~sQ8_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f637,f638,f476,f616,f484])).
% 0.12/0.43 fof(f642,plain,(
% 0.12/0.43 $false|sQ15_spl),
% 0.12/0.43 inference(forward_subsumption_resolution,[status(thm)],[f618,f211])).
% 0.12/0.43 fof(f643,plain,(
% 0.12/0.43 sQ15_spl),
% 0.12/0.43 inference(contradiction_clause,[status(thm)],[f642])).
% 0.12/0.43 fof(f721,plain,(
% 0.12/0.43 ~ssList(sk4)|~ssList(nil)|nil=sk4|sQ5_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f306,f576])).
% 0.12/0.43 fof(f724,plain,(
% 0.12/0.43 ~sQ11_spl|~sQ15_spl|sQ12_spl|sQ5_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f721,f569,f616,f572,f472])).
% 0.12/0.43 fof(f834,plain,(
% 0.12/0.43 ~sk4=nil|~ssList(sk6)|~ssList(sk1)|nil=sk1|~sQ8_spl|~sQ9_spl),
% 0.12/0.43 inference(paramodulation,[status(thm)],[f546,f331])).
% 0.12/0.43 fof(f843,plain,(
% 0.12/0.43 ~sQ12_spl|~sQ7_spl|~sQ13_spl|sQ16_spl|~sQ8_spl|~sQ9_spl),
% 0.12/0.43 inference(split_clause,[status(thm)],[f834,f572,f480,f601,f638,f484,f488])).
% 0.12/0.43 fof(f962,plain,(
% 0.12/0.43 ![X0]: (~ssList(X0)|app(cons(sk5,nil),X0)=cons(sk5,X0)|~sQ6_spl)),
% 0.12/0.43 inference(resolution,[status(thm)],[f334,f477])).
% 0.12/0.43 fof(f963,plain,(
% 0.12/0.43 ![X0]: (~ssList(X0)|app(sk1,X0)=cons(sk5,X0)|~sQ8_spl|~sQ6_spl)),
% 0.12/0.43 inference(forward_demodulation,[status(thm)],[f531,f962])).
% 0.12/0.43 fof(f1075,plain,(
% 0.12/0.43 tl(cons(sk5,sk6))=sk6|~sQ6_spl|~sQ7_spl),
% 0.12/0.43 inference(resolution,[status(thm)],[f636,f481])).
% 0.12/0.45 fof(f1243,plain,(
% 0.12/0.45 app(sk1,sk6)=cons(sk5,sk6)|~sQ8_spl|~sQ6_spl|~sQ7_spl),
% 0.12/0.45 inference(resolution,[status(thm)],[f963,f481])).
% 0.12/0.45 fof(f1248,plain,(
% 0.12/0.45 sk4=cons(sk5,sk6)|~sQ9_spl|~sQ8_spl|~sQ6_spl|~sQ7_spl),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f546,f1243])).
% 0.12/0.45 fof(f1249,plain,(
% 0.12/0.45 tl(sk4)=sk6|~sQ9_spl|~sQ8_spl|~sQ6_spl|~sQ7_spl),
% 0.12/0.45 inference(backward_demodulation,[status(thm)],[f1248,f1075])).
% 0.12/0.45 fof(f1253,plain,(
% 0.12/0.45 ~app(sk1,sk6)=sk4|~sQ9_spl|~sQ8_spl|~sQ6_spl|~sQ7_spl|sQ10_spl),
% 0.12/0.45 inference(backward_demodulation,[status(thm)],[f1249,f568])).
% 0.12/0.45 fof(f1254,plain,(
% 0.12/0.45 ~sk4=sk4|~sQ9_spl|~sQ8_spl|~sQ6_spl|~sQ7_spl|sQ10_spl),
% 0.12/0.45 inference(forward_demodulation,[status(thm)],[f546,f1253])).
% 0.12/0.45 fof(f1255,plain,(
% 0.12/0.45 $false|~sQ9_spl|~sQ8_spl|~sQ6_spl|~sQ7_spl|sQ10_spl),
% 0.12/0.45 inference(trivial_equality_resolution,[status(thm)],[f1254])).
% 0.12/0.45 fof(f1256,plain,(
% 0.12/0.45 ~sQ9_spl|~sQ8_spl|~sQ6_spl|~sQ7_spl|sQ10_spl),
% 0.12/0.45 inference(contradiction_clause,[status(thm)],[f1255])).
% 0.12/0.45 fof(f1257,plain,(
% 0.12/0.45 $false),
% 0.12/0.45 inference(sat_refutation,[status(thm)],[f464,f492,f493,f494,f495,f496,f530,f575,f604,f606,f641,f643,f724,f843,f1256])).
% 0.12/0.45 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.46 % Elapsed time: 0.101910 seconds
% 0.12/0.46 % CPU time: 0.439944 seconds
% 0.12/0.46 % Total memory used: 115.878 MB
% 0.12/0.46 % Net memory used: 115.415 MB
%------------------------------------------------------------------------------