%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC013-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 : n018.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.14s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC013-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.10/0.36 % Computer : n018.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 07:51:15 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.14/0.41 % Refutation found
% 0.14/0.41 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.41 fof(f8,axiom,(
% 0.14/0.41 ssList(nil) ),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f9,axiom,(
% 0.14/0.41 ssItem(skac3) ),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f10,axiom,(
% 0.14/0.41 ssItem(skac2) ),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f76,axiom,(
% 0.14/0.41 (![U]: (( ~ ssList(U)| ssItem(hd(U))| nil = U ) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f86,axiom,(
% 0.14/0.41 (![U,V]: (( ~ ssItem(U)| ~ ssList(V)| ssList(cons(U,V)) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f100,axiom,(
% 0.14/0.41 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| neq(V,U)| V = U ) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f115,axiom,(
% 0.14/0.41 (![U,V]: (( U != V| ~ neq(U,V)| ~ ssList(V)| ~ ssList(U) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f188,negated_conjecture,(
% 0.14/0.41 ssList(sk3) ),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f189,negated_conjecture,(
% 0.14/0.41 ssList(sk4) ),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f190,negated_conjecture,(
% 0.14/0.41 sk2 = sk4 ),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f191,negated_conjecture,(
% 0.14/0.41 sk1 = sk3 ),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f192,negated_conjecture,(
% 0.14/0.41 ( neq(sk2,nil)| neq(sk2,nil) ) ),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f196,negated_conjecture,(
% 0.14/0.41 (![A,B]: (( ~ ssList(A)| sk3 = A| ~ ssItem(B)| cons(B,nil) != A| hd(sk4) != B| ~ neq(nil,sk4)| ~ neq(sk4,nil) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f197,negated_conjecture,(
% 0.14/0.41 (![A,B]: (( ~ ssList(A)| sk1 != A| ~ ssItem(B)| cons(B,nil) != A| hd(sk2) != B| ~ neq(nil,sk2)| ~ neq(sk4,nil) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f205,plain,(
% 0.14/0.41 ssList(nil)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f8])).
% 0.14/0.41 fof(f206,plain,(
% 0.14/0.41 ssItem(skac3)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f9])).
% 0.14/0.41 fof(f207,plain,(
% 0.14/0.41 ssItem(skac2)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f10])).
% 0.14/0.41 fof(f274,plain,(
% 0.14/0.41 ![X0]: (~ssList(X0)|ssItem(hd(X0))|nil=X0)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f76])).
% 0.14/0.41 fof(f284,plain,(
% 0.14/0.41 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|ssList(cons(X0,X1)))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f86])).
% 0.14/0.41 fof(f300,plain,(
% 0.14/0.41 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X1,X0)|X1=X0)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f100])).
% 0.14/0.41 fof(f318,plain,(
% 0.14/0.41 ![U]: ((![V]: ((~U=V|~neq(U,V))|~ssList(V)))|~ssList(U))),
% 0.14/0.41 inference(miniscoping,[status(thm)],[f115])).
% 0.14/0.41 fof(f319,plain,(
% 0.14/0.41 ![X0,X1]: (~X0=X1|~neq(X0,X1)|~ssList(X1)|~ssList(X0))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f318])).
% 0.14/0.41 fof(f430,plain,(
% 0.14/0.41 ssList(sk3)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f188])).
% 0.14/0.41 fof(f431,plain,(
% 0.14/0.41 ssList(sk4)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f189])).
% 0.14/0.41 fof(f432,plain,(
% 0.14/0.41 sk2=sk4),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f190])).
% 0.14/0.41 fof(f433,plain,(
% 0.14/0.41 sk1=sk3),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f191])).
% 0.14/0.41 fof(f434,plain,(
% 0.14/0.41 neq(sk2,nil)|neq(sk2,nil)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f192])).
% 0.14/0.41 fof(f440,plain,(
% 0.14/0.41 ((![B]: ((![A]: (((~ssList(A)|sk3=A)|~ssItem(B))|~cons(B,nil)=A))|~hd(sk4)=B))|~neq(nil,sk4))|~neq(sk4,nil)),
% 0.14/0.41 inference(miniscoping,[status(thm)],[f196])).
% 0.14/0.41 fof(f441,plain,(
% 0.14/0.41 ![X0,X1]: (~ssList(X0)|sk3=X0|~ssItem(X1)|~cons(X1,nil)=X0|~hd(sk4)=X1|~neq(nil,sk4)|~neq(sk4,nil))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f440])).
% 0.14/0.41 fof(f442,plain,(
% 0.14/0.41 ((![B]: ((![A]: (((~ssList(A)|~sk1=A)|~ssItem(B))|~cons(B,nil)=A))|~hd(sk2)=B))|~neq(nil,sk2))|~neq(sk4,nil)),
% 0.14/0.41 inference(miniscoping,[status(thm)],[f197])).
% 0.14/0.41 fof(f443,plain,(
% 0.14/0.41 ![X0,X1]: (~ssList(X0)|~sk1=X0|~ssItem(X1)|~cons(X1,nil)=X0|~hd(sk2)=X1|~neq(nil,sk2)|~neq(sk4,nil))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f442])).
% 0.14/0.41 fof(f451,definition,(
% 0.14/0.41 sQ2_spl <=> (neq(sk2,nil))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f452,plain,(
% 0.14/0.41 neq(sk2,nil)|~sQ2_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f451])).
% 0.14/0.41 fof(f454,plain,(
% 0.14/0.41 sQ2_spl),
% 0.14/0.41 inference(split_clause,[status(thm)],[f434,f451])).
% 0.14/0.41 fof(f455,definition,(
% 0.14/0.41 sQ3_spl <=> (neq(sk4,nil))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f457,plain,(
% 0.14/0.41 ~neq(sk4,nil)|sQ3_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f455])).
% 0.14/0.41 fof(f459,definition,(
% 0.14/0.41 ![X0,X1]: (sQ4_spl <=> (~ssList(X0)|sk3=X0|~ssItem(X1)|~cons(X1,nil)=X0|~hd(sk4)=X1))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f460,plain,(
% 0.14/0.41 ![X0,X1]: (~ssList(X0)|sk3=X0|~ssItem(X1)|~cons(X1,nil)=X0|~hd(sk4)=X1|~sQ4_spl)),
% 0.14/0.41 inference(component_clause,[status(thm)],[f459])).
% 0.14/0.41 fof(f462,definition,(
% 0.14/0.41 sQ5_spl <=> (neq(nil,sk4))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f463,plain,(
% 0.14/0.41 neq(nil,sk4)|~sQ5_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f462])).
% 0.14/0.41 fof(f466,definition,(
% 0.14/0.41 ![X0,X1]: (sQ6_spl <=> (~ssList(X0)|~sk1=X0|~ssItem(X1)|~cons(X1,nil)=X0|~hd(sk2)=X1))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f467,plain,(
% 0.14/0.41 ![X0,X1]: (~ssList(X0)|~sk1=X0|~ssItem(X1)|~cons(X1,nil)=X0|~hd(sk2)=X1|~sQ6_spl)),
% 0.14/0.41 inference(component_clause,[status(thm)],[f466])).
% 0.14/0.41 fof(f469,definition,(
% 0.14/0.41 sQ7_spl <=> (neq(nil,sk2))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f471,plain,(
% 0.14/0.41 ~neq(nil,sk2)|sQ7_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f469])).
% 0.14/0.41 fof(f473,plain,(
% 0.14/0.41 sQ4_spl|~sQ5_spl|~sQ3_spl),
% 0.14/0.41 inference(split_clause,[status(thm)],[f441,f459,f462,f455])).
% 0.14/0.41 fof(f474,plain,(
% 0.14/0.41 sQ6_spl|~sQ7_spl|~sQ3_spl),
% 0.14/0.41 inference(split_clause,[status(thm)],[f443,f466,f469,f455])).
% 0.14/0.41 fof(f482,plain,(
% 0.14/0.41 ![X1]: (~neq(X1,X1)|~ssList(X1)|~ssList(X1))),
% 0.14/0.41 inference(destructive_equality_resolution,[status(thm)],[f319])).
% 0.14/0.41 fof(f483,plain,(
% 0.14/0.41 ![X0]: (~neq(X0,X0)|~ssList(X0))),
% 0.14/0.41 inference(duplicate_literals_removal,[status(thm)],[f482])).
% 0.14/0.41 fof(f506,plain,(
% 0.14/0.41 neq(sk4,nil)|~sQ2_spl),
% 0.14/0.41 inference(forward_demodulation,[status(thm)],[f432,f452])).
% 0.14/0.41 fof(f507,plain,(
% 0.14/0.41 $false|~sQ2_spl|sQ3_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f457,f506])).
% 0.14/0.41 fof(f508,plain,(
% 0.14/0.41 ~sQ2_spl|sQ3_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f507])).
% 0.14/0.41 fof(f509,plain,(
% 0.14/0.41 ~ssList(cons(hd(sk4),nil))|sk3=cons(hd(sk4),nil)|~ssItem(hd(sk4))|~sQ4_spl),
% 0.14/0.41 inference(destructive_equality_resolution,[status(thm)],[f460])).
% 0.14/0.41 fof(f510,plain,(
% 0.14/0.41 ![X0,X1]: (~ssList(X0)|~sk3=X0|~ssItem(X1)|~cons(X1,nil)=X0|~hd(sk2)=X1|~sQ6_spl)),
% 0.14/0.41 inference(forward_demodulation,[status(thm)],[f433,f467])).
% 0.14/0.41 fof(f511,plain,(
% 0.14/0.41 ![X0,X1]: (~ssList(X0)|~sk3=X0|~ssItem(X1)|~cons(X1,nil)=X0|~hd(sk4)=X1|~sQ6_spl)),
% 0.14/0.41 inference(forward_demodulation,[status(thm)],[f432,f510])).
% 0.14/0.41 fof(f512,plain,(
% 0.14/0.41 ~ssList(sk3)|~ssItem(hd(sk4))|~cons(hd(sk4),nil)=sk3|~sQ6_spl),
% 0.14/0.41 inference(destructive_equality_resolution,[status(thm)],[f511])).
% 0.14/0.41 fof(f513,plain,(
% 0.14/0.41 ~ssItem(hd(sk4))|~cons(hd(sk4),nil)=sk3|~sQ6_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f512,f430])).
% 0.14/0.41 fof(f515,plain,(
% 0.14/0.41 ssItem(hd(sk4))|nil=sk4),
% 0.14/0.41 inference(resolution,[status(thm)],[f274,f431])).
% 0.14/0.41 fof(f524,definition,(
% 0.14/0.41 sQ10_spl <=> (ssItem(hd(sk4)))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f525,plain,(
% 0.14/0.41 ssItem(hd(sk4))|~sQ10_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f524])).
% 0.14/0.41 fof(f527,definition,(
% 0.14/0.41 sQ11_spl <=> (nil=sk4)),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f528,plain,(
% 0.14/0.41 nil=sk4|~sQ11_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f527])).
% 0.14/0.41 fof(f530,plain,(
% 0.14/0.41 sQ10_spl|sQ11_spl),
% 0.14/0.41 inference(split_clause,[status(thm)],[f515,f524,f527])).
% 0.14/0.41 fof(f539,plain,(
% 0.14/0.41 ![X0]: (~ssList(X0)|ssList(cons(hd(sk4),X0))|~sQ10_spl)),
% 0.14/0.41 inference(resolution,[status(thm)],[f284,f525])).
% 0.14/0.41 fof(f764,plain,(
% 0.14/0.41 ssList(cons(hd(sk4),nil))|~sQ10_spl),
% 0.14/0.41 inference(resolution,[status(thm)],[f539,f205])).
% 0.14/0.41 fof(f855,plain,(
% 0.14/0.41 ![X0]: (~ssList(X0)|neq(X0,sk4)|X0=sk4)),
% 0.14/0.41 inference(resolution,[status(thm)],[f300,f431])).
% 0.14/0.41 fof(f997,plain,(
% 0.14/0.41 ~neq(nil,sk4)|sQ7_spl),
% 0.14/0.41 inference(forward_demodulation,[status(thm)],[f432,f471])).
% 0.14/0.41 fof(f998,definition,(
% 0.14/0.41 sQ28_spl <=> (cons(hd(sk4),nil)=sk3)),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f1001,plain,(
% 0.14/0.41 ~sQ10_spl|~sQ28_spl|~sQ6_spl),
% 0.14/0.41 inference(split_clause,[status(thm)],[f513,f524,f998,f466])).
% 0.14/0.41 fof(f1002,definition,(
% 0.14/0.41 sQ29_spl <=> (ssList(cons(hd(sk4),nil)))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f1004,plain,(
% 0.14/0.41 ~ssList(cons(hd(sk4),nil))|sQ29_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f1002])).
% 0.14/0.41 fof(f1005,plain,(
% 0.14/0.41 ~sQ29_spl|sQ28_spl|~sQ10_spl|~sQ4_spl),
% 0.14/0.41 inference(split_clause,[status(thm)],[f509,f1002,f998,f524,f459])).
% 0.14/0.41 fof(f1170,plain,(
% 0.14/0.41 $false|sQ29_spl|~sQ10_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f764,f1004])).
% 0.14/0.41 fof(f1171,plain,(
% 0.14/0.41 sQ29_spl|~sQ10_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f1170])).
% 0.14/0.41 fof(f1553,plain,(
% 0.14/0.41 neq(sk4,sk4)|~sQ11_spl|~sQ2_spl),
% 0.14/0.41 inference(backward_demodulation,[status(thm)],[f528,f506])).
% 0.14/0.41 fof(f1778,plain,(
% 0.14/0.41 ~ssList(sk4)|~sQ11_spl|~sQ2_spl),
% 0.14/0.41 inference(resolution,[status(thm)],[f1553,f483])).
% 0.14/0.41 fof(f1779,plain,(
% 0.14/0.41 $false|~sQ11_spl|~sQ2_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1778,f431])).
% 0.14/0.41 fof(f1780,plain,(
% 0.14/0.41 ~sQ11_spl|~sQ2_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f1779])).
% 0.14/0.41 fof(f1874,definition,(
% 0.14/0.41 sQ46_spl <=> (ssItem(skac3))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f1876,plain,(
% 0.14/0.41 ~ssItem(skac3)|sQ46_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f1874])).
% 0.14/0.41 fof(f1877,definition,(
% 0.14/0.41 sQ47_spl <=> (ssList(sk4))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f1879,plain,(
% 0.14/0.41 ~ssList(sk4)|sQ47_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f1877])).
% 0.14/0.41 fof(f1882,plain,(
% 0.14/0.41 $false|sQ47_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1879,f431])).
% 0.14/0.41 fof(f1883,plain,(
% 0.14/0.41 sQ47_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f1882])).
% 0.14/0.41 fof(f1884,plain,(
% 0.14/0.41 $false|sQ46_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1876,f206])).
% 0.14/0.41 fof(f1885,plain,(
% 0.14/0.41 sQ46_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f1884])).
% 0.14/0.41 fof(f1888,definition,(
% 0.14/0.41 sQ48_spl <=> (ssList(sk3))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f1890,plain,(
% 0.14/0.41 ~ssList(sk3)|sQ48_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f1888])).
% 0.14/0.41 fof(f1893,plain,(
% 0.14/0.41 $false|sQ48_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1890,f430])).
% 0.14/0.41 fof(f1894,plain,(
% 0.14/0.41 sQ48_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f1893])).
% 0.14/0.41 fof(f1907,definition,(
% 0.14/0.41 sQ49_spl <=> (ssList(nil))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f1909,plain,(
% 0.14/0.41 ~ssList(nil)|sQ49_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f1907])).
% 0.14/0.41 fof(f1912,plain,(
% 0.14/0.41 $false|sQ49_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1909,f205])).
% 0.14/0.41 fof(f1913,plain,(
% 0.14/0.41 sQ49_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f1912])).
% 0.14/0.41 fof(f1916,definition,(
% 0.14/0.41 sQ50_spl <=> (ssItem(skac2))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f1918,plain,(
% 0.14/0.41 ~ssItem(skac2)|sQ50_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f1916])).
% 0.14/0.41 fof(f1921,plain,(
% 0.14/0.41 $false|sQ50_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1918,f207])).
% 0.14/0.41 fof(f1922,plain,(
% 0.14/0.41 sQ50_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f1921])).
% 0.14/0.41 fof(f2092,plain,(
% 0.14/0.41 neq(nil,sk4)|nil=sk4),
% 0.14/0.41 inference(resolution,[status(thm)],[f855,f205])).
% 0.14/0.41 fof(f2150,plain,(
% 0.14/0.41 sQ5_spl|sQ11_spl),
% 0.14/0.41 inference(split_clause,[status(thm)],[f2092,f462,f527])).
% 0.14/0.41 fof(f2187,plain,(
% 0.14/0.41 $false|sQ7_spl|~sQ5_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f463,f997])).
% 0.14/0.41 fof(f2188,plain,(
% 0.14/0.41 sQ7_spl|~sQ5_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f2187])).
% 0.14/0.41 fof(f2189,plain,(
% 0.14/0.41 $false),
% 0.14/0.41 inference(sat_refutation,[status(thm)],[f454,f473,f474,f508,f530,f1001,f1005,f1171,f1780,f1883,f1885,f1894,f1913,f1922,f2150,f2188])).
% 0.14/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.44 % Elapsed time: 0.068683 seconds
% 0.14/0.44 % CPU time: 0.261432 seconds
% 0.14/0.44 % Total memory used: 107.743 MB
% 0.14/0.44 % Net memory used: 107.498 MB
%------------------------------------------------------------------------------