%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC030-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 : n017.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:23 PM UTC 2026
% Result : Unsatisfiable 0.09s 0.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC030-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.09/0.37 % Computer : n017.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 07:45:42 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.39 % Drodi V4.1.1
% 0.09/0.42 % Refutation found
% 0.09/0.42 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.09/0.42 % SZS output start CNFRefutation for theBenchmark
% 0.09/0.42 fof(f73,axiom,(
% 0.09/0.42 (![U]: (( ~ ssList(U)| app(U,nil) = U ) ))),
% 0.09/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.42 fof(f74,axiom,(
% 0.09/0.42 (![U]: (( ~ ssList(U)| app(nil,U) = U ) ))),
% 0.09/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.42 fof(f118,axiom,(
% 0.09/0.42 (![U,V]: (( app(U,V) != nil| ~ ssList(V)| ~ ssList(U)| nil = U ) ))),
% 0.09/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.42 fof(f119,axiom,(
% 0.09/0.42 (![U,V]: (( app(U,V) != nil| ~ ssList(V)| ~ ssList(U)| nil = V ) ))),
% 0.09/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.42 fof(f145,axiom,(
% 0.09/0.42 (![U,V]: (( nil != U| nil != V| ~ ssList(V)| ~ ssList(U)| app(U,V) = nil ) ))),
% 0.09/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.42 fof(f188,negated_conjecture,(
% 0.09/0.42 ssList(sk3) ),
% 0.09/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.42 fof(f189,negated_conjecture,(
% 0.09/0.42 ssList(sk4) ),
% 0.09/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.42 fof(f190,negated_conjecture,(
% 0.09/0.42 sk2 = sk4 ),
% 0.09/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.42 fof(f191,negated_conjecture,(
% 0.09/0.42 sk1 = sk3 ),
% 0.09/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.42 fof(f192,negated_conjecture,(
% 0.09/0.42 ssList(sk5) ),
% 0.09/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.42 fof(f193,negated_conjecture,(
% 0.09/0.42 ssList(sk6) ),
% 0.09/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.42 fof(f194,negated_conjecture,(
% 0.09/0.42 app(sk5,sk6) = sk4 ),
% 0.09/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.42 fof(f195,negated_conjecture,(
% 0.09/0.42 app(sk6,sk5) = sk3 ),
% 0.09/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.42 fof(f196,negated_conjecture,(
% 0.09/0.42 ( nil = sk2| nil = sk1 ) ),
% 0.09/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.42 fof(f199,negated_conjecture,(
% 0.09/0.42 ( nil != sk1| nil != sk2 ) ),
% 0.09/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.09/0.42 fof(f273,plain,(
% 0.09/0.42 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f73])).
% 0.09/0.42 fof(f274,plain,(
% 0.09/0.42 ![X0]: (~ssList(X0)|app(nil,X0)=X0)),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f74])).
% 0.09/0.42 fof(f326,plain,(
% 0.09/0.42 ![U]: (((![V]: (~app(U,V)=nil|~ssList(V)))|~ssList(U))|nil=U)),
% 0.09/0.42 inference(miniscoping,[status(thm)],[f118])).
% 0.09/0.42 fof(f327,plain,(
% 0.09/0.42 ![X0,X1]: (~app(X0,X1)=nil|~ssList(X1)|~ssList(X0)|nil=X0)),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f326])).
% 0.09/0.42 fof(f328,plain,(
% 0.09/0.42 ![V]: ((![U]: ((~app(U,V)=nil|~ssList(V))|~ssList(U)))|nil=V)),
% 0.09/0.42 inference(miniscoping,[status(thm)],[f119])).
% 0.09/0.42 fof(f329,plain,(
% 0.09/0.42 ![X0,X1]: (~app(X0,X1)=nil|~ssList(X1)|~ssList(X0)|nil=X1)),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f328])).
% 0.09/0.42 fof(f361,plain,(
% 0.09/0.42 ![X0,X1]: (~nil=X0|~nil=X1|~ssList(X1)|~ssList(X0)|app(X0,X1)=nil)),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f145])).
% 0.09/0.42 fof(f432,plain,(
% 0.09/0.42 ssList(sk3)),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f188])).
% 0.09/0.42 fof(f433,plain,(
% 0.09/0.42 ssList(sk4)),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f189])).
% 0.09/0.42 fof(f434,plain,(
% 0.09/0.42 sk2=sk4),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f190])).
% 0.09/0.42 fof(f435,plain,(
% 0.09/0.42 sk1=sk3),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f191])).
% 0.09/0.42 fof(f436,plain,(
% 0.09/0.42 ssList(sk5)),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f192])).
% 0.09/0.42 fof(f437,plain,(
% 0.09/0.42 ssList(sk6)),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f193])).
% 0.09/0.42 fof(f438,plain,(
% 0.09/0.42 app(sk5,sk6)=sk4),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f194])).
% 0.09/0.42 fof(f439,plain,(
% 0.09/0.42 app(sk6,sk5)=sk3),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f195])).
% 0.09/0.42 fof(f440,plain,(
% 0.09/0.42 nil=sk2|nil=sk1),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f196])).
% 0.09/0.42 fof(f443,plain,(
% 0.09/0.42 ~nil=sk1|~nil=sk2),
% 0.09/0.42 inference(cnf_transformation,[status(thm)],[f199])).
% 0.09/0.42 fof(f451,definition,(
% 0.09/0.42 sQ2_spl <=> (nil=sk2)),
% 0.09/0.42 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.09/0.42 fof(f452,plain,(
% 0.09/0.42 nil=sk2|~sQ2_spl),
% 0.09/0.42 inference(component_clause,[status(thm)],[f451])).
% 0.09/0.42 fof(f453,plain,(
% 0.09/0.42 ~nil=sk2|sQ2_spl),
% 0.09/0.42 inference(component_clause,[status(thm)],[f451])).
% 0.09/0.42 fof(f454,definition,(
% 0.09/0.42 sQ3_spl <=> (nil=sk1)),
% 0.09/0.42 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.09/0.42 fof(f455,plain,(
% 0.09/0.42 nil=sk1|~sQ3_spl),
% 0.09/0.42 inference(component_clause,[status(thm)],[f454])).
% 0.09/0.42 fof(f456,plain,(
% 0.09/0.42 ~nil=sk1|sQ3_spl),
% 0.09/0.42 inference(component_clause,[status(thm)],[f454])).
% 0.09/0.42 fof(f457,plain,(
% 0.09/0.42 sQ2_spl|sQ3_spl),
% 0.09/0.42 inference(split_clause,[status(thm)],[f440,f451,f454])).
% 0.09/0.42 fof(f460,plain,(
% 0.09/0.42 ~sQ3_spl|~sQ2_spl),
% 0.09/0.42 inference(split_clause,[status(thm)],[f443,f454,f451])).
% 0.09/0.42 fof(f477,plain,(
% 0.09/0.42 ~ssList(nil)|~ssList(nil)|app(nil,nil)=nil),
% 0.09/0.42 inference(destructive_equality_resolution,[status(thm)],[f361])).
% 0.09/0.42 fof(f478,plain,(
% 0.09/0.42 ~ssList(nil)|app(nil,nil)=nil),
% 0.09/0.42 inference(duplicate_literals_removal,[status(thm)],[f477])).
% 0.09/0.42 fof(f492,plain,(
% 0.09/0.42 ~nil=sk3|sQ3_spl),
% 0.09/0.42 inference(forward_demodulation,[status(thm)],[f435,f456])).
% 0.09/0.42 fof(f495,plain,(
% 0.09/0.42 nil=sk4|~sQ2_spl),
% 0.09/0.42 inference(forward_demodulation,[status(thm)],[f434,f452])).
% 0.09/0.42 fof(f496,plain,(
% 0.09/0.42 ![X0]: (~ssList(X0)|app(X0,sk4)=X0|~sQ2_spl)),
% 0.09/0.42 inference(forward_demodulation,[status(thm)],[f495,f273])).
% 0.09/0.42 fof(f499,plain,(
% 0.09/0.42 app(sk4,sk4)=sk4|~sQ2_spl),
% 0.09/0.42 inference(resolution,[status(thm)],[f496,f433])).
% 0.09/0.42 fof(f501,plain,(
% 0.09/0.42 ![X0]: (~ssList(X0)|app(sk4,X0)=X0|~sQ2_spl)),
% 0.09/0.42 inference(forward_demodulation,[status(thm)],[f495,f274])).
% 0.09/0.42 fof(f502,plain,(
% 0.09/0.42 app(sk4,sk6)=sk6|~sQ2_spl),
% 0.09/0.42 inference(resolution,[status(thm)],[f501,f437])).
% 0.09/0.42 fof(f586,plain,(
% 0.09/0.42 ![X0,X1]: (~app(X0,X1)=sk4|~ssList(X1)|~ssList(X0)|nil=X0|~sQ2_spl)),
% 0.09/0.42 inference(forward_demodulation,[status(thm)],[f495,f327])).
% 0.09/0.42 fof(f587,plain,(
% 0.09/0.42 ![X0,X1]: (~app(X0,X1)=sk4|~ssList(X1)|~ssList(X0)|sk4=X0|~sQ2_spl)),
% 0.09/0.42 inference(forward_demodulation,[status(thm)],[f495,f586])).
% 0.09/0.42 fof(f588,plain,(
% 0.09/0.42 ~ssList(sk4)|~ssList(sk4)|sk4=sk4|~sQ2_spl),
% 0.09/0.42 inference(resolution,[status(thm)],[f587,f499])).
% 0.09/0.42 fof(f598,plain,(
% 0.09/0.42 ~sk4=sk4|~ssList(sk6)|~ssList(sk5)|sk4=sk5|~sQ2_spl),
% 0.09/0.42 inference(paramodulation,[status(thm)],[f438,f587])).
% 0.09/0.42 fof(f599,definition,(
% 0.09/0.42 sQ4_spl <=> (ssList(sk4))),
% 0.09/0.42 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.09/0.42 fof(f601,plain,(
% 0.09/0.42 ~ssList(sk4)|sQ4_spl),
% 0.09/0.42 inference(component_clause,[status(thm)],[f599])).
% 0.09/0.42 fof(f602,definition,(
% 0.09/0.42 sQ5_spl <=> (sk4=sk4)),
% 0.09/0.42 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.09/0.42 fof(f605,plain,(
% 0.09/0.42 ~sQ4_spl|sQ5_spl|~sQ2_spl),
% 0.09/0.42 inference(split_clause,[status(thm)],[f588,f599,f602,f451])).
% 0.09/0.42 fof(f606,definition,(
% 0.09/0.42 sQ6_spl <=> (ssList(sk6))),
% 0.09/0.42 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.09/0.42 fof(f608,plain,(
% 0.09/0.42 ~ssList(sk6)|sQ6_spl),
% 0.09/0.42 inference(component_clause,[status(thm)],[f606])).
% 0.09/0.42 fof(f609,definition,(
% 0.09/0.42 sQ7_spl <=> (ssList(sk5))),
% 0.09/0.42 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.09/0.42 fof(f611,plain,(
% 0.09/0.42 ~ssList(sk5)|sQ7_spl),
% 0.09/0.42 inference(component_clause,[status(thm)],[f609])).
% 0.09/0.42 fof(f612,definition,(
% 0.09/0.42 sQ8_spl <=> (sk4=sk5)),
% 0.09/0.42 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.09/0.42 fof(f613,plain,(
% 0.09/0.42 sk4=sk5|~sQ8_spl),
% 0.09/0.42 inference(component_clause,[status(thm)],[f612])).
% 0.09/0.42 fof(f616,definition,(
% 0.09/0.42 sQ9_spl <=> (sk3=sk4)),
% 0.09/0.42 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.09/0.42 fof(f618,plain,(
% 0.09/0.42 ~sk3=sk4|sQ9_spl),
% 0.09/0.42 inference(component_clause,[status(thm)],[f616])).
% 0.09/0.42 fof(f619,definition,(
% 0.09/0.42 sQ10_spl <=> (ssList(sk3))),
% 0.09/0.42 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.09/0.42 fof(f621,plain,(
% 0.09/0.42 ~ssList(sk3)|sQ10_spl),
% 0.09/0.42 inference(component_clause,[status(thm)],[f619])).
% 0.09/0.42 fof(f633,plain,(
% 0.09/0.42 ~sQ5_spl|~sQ6_spl|~sQ7_spl|sQ8_spl|~sQ2_spl),
% 0.09/0.42 inference(split_clause,[status(thm)],[f598,f602,f606,f609,f612,f451])).
% 0.09/0.42 fof(f634,plain,(
% 0.09/0.42 $false|sQ4_spl),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f601,f433])).
% 0.09/0.42 fof(f635,plain,(
% 0.09/0.42 sQ4_spl),
% 0.09/0.42 inference(contradiction_clause,[status(thm)],[f634])).
% 0.09/0.42 fof(f636,plain,(
% 0.09/0.42 ~nil=sk4|sQ2_spl),
% 0.09/0.42 inference(forward_demodulation,[status(thm)],[f434,f453])).
% 0.09/0.42 fof(f637,plain,(
% 0.09/0.42 nil=sk3|~sQ3_spl),
% 0.09/0.42 inference(forward_demodulation,[status(thm)],[f435,f455])).
% 0.09/0.42 fof(f641,plain,(
% 0.09/0.42 ~sk3=sk4|~sQ3_spl|sQ2_spl),
% 0.09/0.42 inference(backward_demodulation,[status(thm)],[f637,f636])).
% 0.09/0.42 fof(f708,plain,(
% 0.09/0.42 ![X0,X1]: (~app(X0,X1)=sk3|~ssList(X1)|~ssList(X0)|nil=X1|~sQ3_spl)),
% 0.09/0.42 inference(forward_demodulation,[status(thm)],[f637,f329])).
% 0.09/0.42 fof(f709,plain,(
% 0.09/0.42 ![X0,X1]: (~app(X0,X1)=sk3|~ssList(X1)|~ssList(X0)|sk3=X1|~sQ3_spl)),
% 0.09/0.42 inference(forward_demodulation,[status(thm)],[f637,f708])).
% 0.09/0.42 fof(f710,plain,(
% 0.09/0.42 ~ssList(sk5)|~ssList(sk6)|sk3=sk5|~sQ3_spl),
% 0.09/0.42 inference(resolution,[status(thm)],[f709,f439])).
% 0.09/0.42 fof(f713,definition,(
% 0.09/0.42 sQ12_spl <=> (sk3=sk5)),
% 0.09/0.42 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.09/0.42 fof(f714,plain,(
% 0.09/0.42 sk3=sk5|~sQ12_spl),
% 0.09/0.42 inference(component_clause,[status(thm)],[f713])).
% 0.09/0.42 fof(f716,plain,(
% 0.09/0.42 ~sQ7_spl|~sQ6_spl|sQ12_spl|~sQ3_spl),
% 0.09/0.42 inference(split_clause,[status(thm)],[f710,f609,f606,f713,f454])).
% 0.09/0.42 fof(f725,plain,(
% 0.09/0.42 $false|sQ7_spl),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f611,f436])).
% 0.09/0.42 fof(f726,plain,(
% 0.09/0.42 sQ7_spl),
% 0.09/0.42 inference(contradiction_clause,[status(thm)],[f725])).
% 0.09/0.42 fof(f727,plain,(
% 0.09/0.42 $false|sQ6_spl),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f608,f437])).
% 0.09/0.42 fof(f728,plain,(
% 0.09/0.42 sQ6_spl),
% 0.09/0.42 inference(contradiction_clause,[status(thm)],[f727])).
% 0.09/0.42 fof(f767,plain,(
% 0.09/0.42 ~sk5=sk4|~sQ12_spl|~sQ3_spl|sQ2_spl),
% 0.09/0.42 inference(backward_demodulation,[status(thm)],[f714,f641])).
% 0.09/0.42 fof(f768,plain,(
% 0.09/0.42 nil=sk5|~sQ12_spl|~sQ3_spl),
% 0.09/0.42 inference(backward_demodulation,[status(thm)],[f714,f637])).
% 0.09/0.42 fof(f770,plain,(
% 0.09/0.42 app(sk6,sk5)=sk5|~sQ12_spl),
% 0.09/0.42 inference(backward_demodulation,[status(thm)],[f714,f439])).
% 0.09/0.42 fof(f836,plain,(
% 0.09/0.42 ![X0]: (~ssList(X0)|app(sk5,X0)=X0|~sQ12_spl|~sQ3_spl)),
% 0.09/0.42 inference(forward_demodulation,[status(thm)],[f768,f274])).
% 0.09/0.42 fof(f863,plain,(
% 0.09/0.42 app(sk5,sk6)=sk6|~sQ12_spl|~sQ3_spl),
% 0.09/0.42 inference(resolution,[status(thm)],[f836,f437])).
% 0.09/0.42 fof(f866,plain,(
% 0.09/0.42 sk6=sk4|~sQ12_spl|~sQ3_spl),
% 0.09/0.42 inference(backward_demodulation,[status(thm)],[f863,f438])).
% 0.09/0.42 fof(f867,plain,(
% 0.09/0.42 ~sk5=sk6|~sQ12_spl|~sQ3_spl|sQ2_spl),
% 0.09/0.42 inference(backward_demodulation,[status(thm)],[f866,f767])).
% 0.09/0.42 fof(f882,plain,(
% 0.09/0.42 ![X0]: (~ssList(X0)|app(X0,sk5)=X0|~sQ12_spl|~sQ3_spl)),
% 0.09/0.42 inference(forward_demodulation,[status(thm)],[f768,f273])).
% 0.09/0.42 fof(f903,plain,(
% 0.09/0.42 app(sk6,sk5)=sk6|~sQ12_spl|~sQ3_spl),
% 0.09/0.42 inference(resolution,[status(thm)],[f882,f437])).
% 0.09/0.42 fof(f905,plain,(
% 0.09/0.42 sk6=sk5|~sQ3_spl|~sQ12_spl),
% 0.09/0.42 inference(backward_demodulation,[status(thm)],[f903,f770])).
% 0.09/0.42 fof(f906,plain,(
% 0.09/0.42 $false|sQ2_spl|~sQ3_spl|~sQ12_spl),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f905,f867])).
% 0.09/0.42 fof(f907,plain,(
% 0.09/0.42 sQ2_spl|~sQ3_spl|~sQ12_spl),
% 0.09/0.42 inference(contradiction_clause,[status(thm)],[f906])).
% 0.09/0.42 fof(f974,plain,(
% 0.09/0.42 ~ssList(nil)|app(nil,nil)=sk4|~sQ2_spl),
% 0.09/0.42 inference(backward_demodulation,[status(thm)],[f495,f478])).
% 0.09/0.42 fof(f975,definition,(
% 0.09/0.42 sQ15_spl <=> (ssList(nil))),
% 0.09/0.42 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.09/0.42 fof(f977,plain,(
% 0.09/0.42 ~ssList(nil)|sQ15_spl),
% 0.09/0.42 inference(component_clause,[status(thm)],[f975])).
% 0.09/0.42 fof(f978,definition,(
% 0.09/0.42 sQ16_spl <=> (app(nil,nil)=sk4)),
% 0.09/0.42 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.09/0.42 fof(f979,plain,(
% 0.09/0.42 app(nil,nil)=sk4|~sQ16_spl),
% 0.09/0.42 inference(component_clause,[status(thm)],[f978])).
% 0.09/0.42 fof(f981,plain,(
% 0.09/0.42 ~sQ15_spl|sQ16_spl|~sQ2_spl),
% 0.09/0.42 inference(split_clause,[status(thm)],[f974,f975,f978,f451])).
% 0.09/0.42 fof(f982,plain,(
% 0.09/0.42 ~ssList(sk4)|~sQ2_spl|sQ15_spl),
% 0.09/0.42 inference(forward_demodulation,[status(thm)],[f495,f977])).
% 0.09/0.42 fof(f1007,plain,(
% 0.09/0.42 ~sk4=sk3|~sQ2_spl|sQ3_spl),
% 0.09/0.42 inference(forward_demodulation,[status(thm)],[f495,f492])).
% 0.09/0.42 fof(f1018,plain,(
% 0.09/0.42 nil=sk5|~sQ8_spl|~sQ2_spl),
% 0.09/0.42 inference(backward_demodulation,[status(thm)],[f613,f495])).
% 0.09/0.42 fof(f1019,plain,(
% 0.09/0.42 ~sk3=sk5|~sQ8_spl|sQ9_spl),
% 0.09/0.42 inference(backward_demodulation,[status(thm)],[f613,f618])).
% 0.09/0.42 fof(f1027,plain,(
% 0.09/0.42 ~ssList(sk5)|~sQ8_spl|~sQ2_spl|sQ15_spl),
% 0.09/0.42 inference(forward_demodulation,[status(thm)],[f613,f982])).
% 0.09/0.42 fof(f1028,plain,(
% 0.09/0.42 $false|~sQ8_spl|~sQ2_spl|sQ15_spl),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1027,f436])).
% 0.09/0.42 fof(f1029,plain,(
% 0.09/0.42 ~sQ8_spl|~sQ2_spl|sQ15_spl),
% 0.09/0.42 inference(contradiction_clause,[status(thm)],[f1028])).
% 0.09/0.42 fof(f1030,plain,(
% 0.09/0.42 app(nil,nil)=sk5|~sQ8_spl|~sQ16_spl),
% 0.09/0.42 inference(forward_demodulation,[status(thm)],[f613,f979])).
% 0.09/0.42 fof(f1170,plain,(
% 0.09/0.42 $false|sQ10_spl),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f621,f432])).
% 0.09/0.42 fof(f1171,plain,(
% 0.09/0.42 sQ10_spl),
% 0.09/0.42 inference(contradiction_clause,[status(thm)],[f1170])).
% 0.09/0.42 fof(f1172,plain,(
% 0.09/0.42 app(sk5,sk6)=sk6|~sQ8_spl|~sQ2_spl),
% 0.09/0.42 inference(forward_demodulation,[status(thm)],[f613,f502])).
% 0.09/0.42 fof(f1247,plain,(
% 0.09/0.42 sk6=sk5|~sQ2_spl|~sQ8_spl),
% 0.09/0.42 inference(backward_demodulation,[status(thm)],[f1248,f613])).
% 0.09/0.42 fof(f1248,plain,(
% 0.09/0.42 sk6=sk4|~sQ8_spl|~sQ2_spl),
% 0.09/0.42 inference(forward_demodulation,[status(thm)],[f1172,f438])).
% 0.09/0.42 fof(f1255,plain,(
% 0.09/0.42 ~sk3=sk6|~sQ2_spl|~sQ8_spl|sQ9_spl),
% 0.09/0.42 inference(backward_demodulation,[status(thm)],[f1247,f1019])).
% 0.09/0.42 fof(f1256,plain,(
% 0.09/0.42 nil=sk6|~sQ8_spl|~sQ2_spl),
% 0.09/0.42 inference(backward_demodulation,[status(thm)],[f1247,f1018])).
% 0.09/0.42 fof(f1400,plain,(
% 0.09/0.42 app(sk6,sk6)=sk3|~sQ2_spl|~sQ8_spl),
% 0.09/0.42 inference(forward_demodulation,[status(thm)],[f1247,f439])).
% 0.09/0.42 fof(f1421,plain,(
% 0.09/0.42 app(sk6,nil)=sk5|~sQ2_spl|~sQ8_spl|~sQ16_spl),
% 0.09/0.42 inference(forward_demodulation,[status(thm)],[f1256,f1030])).
% 0.09/0.42 fof(f1422,plain,(
% 0.09/0.42 app(sk6,sk6)=sk5|~sQ2_spl|~sQ8_spl|~sQ16_spl),
% 0.09/0.42 inference(forward_demodulation,[status(thm)],[f1256,f1421])).
% 0.09/0.42 fof(f1423,plain,(
% 0.09/0.42 sk6=sk3|~sQ16_spl|~sQ2_spl|~sQ8_spl),
% 0.09/0.42 inference(backward_demodulation,[status(thm)],[f1424,f1400])).
% 0.09/0.42 fof(f1424,plain,(
% 0.09/0.42 app(sk6,sk6)=sk6|~sQ2_spl|~sQ8_spl|~sQ16_spl),
% 0.09/0.42 inference(forward_demodulation,[status(thm)],[f1247,f1422])).
% 0.09/0.42 fof(f1429,plain,(
% 0.09/0.42 $false|sQ9_spl|~sQ16_spl|~sQ2_spl|~sQ8_spl),
% 0.09/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1423,f1255])).
% 0.09/0.42 fof(f1430,plain,(
% 0.09/0.42 sQ9_spl|~sQ16_spl|~sQ2_spl|~sQ8_spl),
% 0.09/0.42 inference(contradiction_clause,[status(thm)],[f1429])).
% 0.09/0.42 fof(f1441,plain,(
% 0.09/0.42 ~sQ9_spl|~sQ2_spl|sQ3_spl),
% 0.09/0.42 inference(split_clause,[status(thm)],[f1007,f616,f451,f454])).
% 0.09/0.42 fof(f1444,plain,(
% 0.09/0.42 $false),
% 0.09/0.42 inference(sat_refutation,[status(thm)],[f457,f460,f605,f633,f635,f716,f726,f728,f907,f981,f1029,f1171,f1430,f1441])).
% 0.09/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.09/0.45 % Elapsed time: 0.070326 seconds
% 0.09/0.45 % CPU time: 0.209702 seconds
% 0.09/0.45 % Total memory used: 109.663 MB
% 0.09/0.45 % Net memory used: 109.470 MB
%------------------------------------------------------------------------------