%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC316-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 : n007.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:42:08 PM UTC 2026
% Result : Unsatisfiable 53.35s 7.23s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC316-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.35 % Computer : n007.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 08:12:50 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.38 % Drodi V4.1.1
% 53.35/7.23 % Refutation found
% 53.35/7.23 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 53.35/7.23 % SZS output start CNFRefutation for theBenchmark
% 53.35/7.23 fof(f8,axiom,(
% 53.35/7.23 ssList(nil) ),
% 53.35/7.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.35/7.23 fof(f73,axiom,(
% 53.35/7.23 (![U]: (( ~ ssList(U)| app(U,nil) = U ) ))),
% 53.35/7.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.35/7.23 fof(f75,axiom,(
% 53.35/7.23 (![U]: (( ~ ssList(U)| ssList(tl(U))| nil = U ) ))),
% 53.35/7.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.35/7.23 fof(f76,axiom,(
% 53.35/7.23 (![U]: (( ~ ssList(U)| ssItem(hd(U))| nil = U ) ))),
% 53.35/7.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.35/7.23 fof(f85,axiom,(
% 53.35/7.23 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| ssList(app(V,U)) ) ))),
% 53.35/7.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.35/7.23 fof(f86,axiom,(
% 53.35/7.23 (![U,V]: (( ~ ssItem(U)| ~ ssList(V)| ssList(cons(U,V)) ) ))),
% 53.35/7.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.35/7.23 fof(f96,axiom,(
% 53.35/7.23 (![U,V]: (( ~ ssItem(U)| ~ ssList(V)| tl(cons(U,V)) = V ) ))),
% 53.35/7.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.35/7.23 fof(f97,axiom,(
% 53.35/7.23 (![U,V]: (( ~ ssItem(U)| ~ ssList(V)| hd(cons(U,V)) = U ) ))),
% 53.35/7.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.35/7.23 fof(f98,axiom,(
% 53.35/7.23 (![U,V]: (( cons(U,V) != nil| ~ ssItem(U)| ~ ssList(V) ) ))),
% 53.35/7.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.35/7.23 fof(f100,axiom,(
% 53.35/7.23 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| neq(V,U)| V = U ) ))),
% 53.35/7.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.35/7.23 fof(f118,axiom,(
% 53.35/7.23 (![U,V]: (( app(U,V) != nil| ~ ssList(V)| ~ ssList(U)| nil = U ) ))),
% 53.35/7.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.35/7.23 fof(f120,axiom,(
% 53.35/7.23 (![U,V]: (( ~ ssItem(U)| ~ ssList(V)| app(cons(U,nil),V) = cons(U,V) ) ))),
% 53.35/7.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.35/7.23 fof(f186,negated_conjecture,(
% 53.35/7.23 ssList(sk1) ),
% 53.35/7.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.35/7.23 fof(f187,negated_conjecture,(
% 53.35/7.23 ssList(sk2) ),
% 53.35/7.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.35/7.23 fof(f190,negated_conjecture,(
% 53.35/7.23 sk2 = sk4 ),
% 53.35/7.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.35/7.23 fof(f191,negated_conjecture,(
% 53.35/7.23 sk1 = sk3 ),
% 53.35/7.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.35/7.23 fof(f192,negated_conjecture,(
% 53.35/7.23 ( neq(sk2,nil)| neq(sk2,nil) ) ),
% 53.35/7.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.35/7.23 fof(f199,negated_conjecture,(
% 53.35/7.23 ( ssItem(sk5)| ~ neq(sk4,nil) ) ),
% 53.35/7.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.35/7.23 fof(f200,negated_conjecture,(
% 53.35/7.23 ( ssList(sk6)| ~ neq(sk4,nil) ) ),
% 53.35/7.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.35/7.23 fof(f201,negated_conjecture,(
% 53.35/7.23 ( app(cons(sk5,nil),sk6) = sk3| ~ neq(sk4,nil) ) ),
% 53.35/7.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.35/7.23 fof(f202,negated_conjecture,(
% 53.35/7.23 ( app(sk6,cons(sk5,nil)) = sk4| ~ neq(sk4,nil) ) ),
% 53.35/7.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.35/7.23 fof(f203,negated_conjecture,(
% 53.35/7.23 (![A,B,C,D]: (( ~ ssList(A)| sk2 != A| ~ ssList(B)| ~ ssList(C)| tl(sk1) != B| app(B,C) != A| ~ ssItem(D)| cons(D,nil) != C| hd(sk1) != D| ~ neq(nil,sk1)| ~ neq(nil,sk1)| ~ neq(sk1,nil)| ~ neq(sk4,nil) ) ))),
% 53.35/7.23 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 53.35/7.23 fof(f211,plain,(
% 53.35/7.23 ssList(nil)),
% 53.35/7.23 inference(cnf_transformation,[status(thm)],[f8])).
% 53.35/7.23 fof(f277,plain,(
% 53.35/7.23 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 53.35/7.23 inference(cnf_transformation,[status(thm)],[f73])).
% 53.35/7.23 fof(f279,plain,(
% 53.35/7.23 ![X0]: (~ssList(X0)|ssList(tl(X0))|nil=X0)),
% 53.35/7.23 inference(cnf_transformation,[status(thm)],[f75])).
% 53.35/7.23 fof(f280,plain,(
% 53.35/7.23 ![X0]: (~ssList(X0)|ssItem(hd(X0))|nil=X0)),
% 53.35/7.23 inference(cnf_transformation,[status(thm)],[f76])).
% 53.35/7.23 fof(f289,plain,(
% 53.35/7.23 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X1,X0)))),
% 53.35/7.23 inference(cnf_transformation,[status(thm)],[f85])).
% 53.35/7.23 fof(f290,plain,(
% 53.35/7.23 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|ssList(cons(X0,X1)))),
% 53.35/7.23 inference(cnf_transformation,[status(thm)],[f86])).
% 53.35/7.23 fof(f300,plain,(
% 53.35/7.23 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|tl(cons(X0,X1))=X1)),
% 53.35/7.23 inference(cnf_transformation,[status(thm)],[f96])).
% 53.35/7.23 fof(f301,plain,(
% 53.35/7.23 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|hd(cons(X0,X1))=X0)),
% 53.35/7.23 inference(cnf_transformation,[status(thm)],[f97])).
% 53.35/7.23 fof(f302,plain,(
% 53.35/7.23 ![V]: ((![U]: (~cons(U,V)=nil|~ssItem(U)))|~ssList(V))),
% 53.35/7.23 inference(miniscoping,[status(thm)],[f98])).
% 53.35/7.23 fof(f303,plain,(
% 53.35/7.23 ![X0,X1]: (~cons(X0,X1)=nil|~ssItem(X0)|~ssList(X1))),
% 53.35/7.23 inference(cnf_transformation,[status(thm)],[f302])).
% 53.35/7.23 fof(f306,plain,(
% 53.35/7.23 ![X0,X1]: (~ssList(X0)|~ssList(X1)|neq(X1,X0)|X1=X0)),
% 53.35/7.23 inference(cnf_transformation,[status(thm)],[f100])).
% 53.35/7.23 fof(f330,plain,(
% 53.35/7.23 ![U]: (((![V]: (~app(U,V)=nil|~ssList(V)))|~ssList(U))|nil=U)),
% 53.35/7.23 inference(miniscoping,[status(thm)],[f118])).
% 53.35/7.23 fof(f331,plain,(
% 53.35/7.23 ![X0,X1]: (~app(X0,X1)=nil|~ssList(X1)|~ssList(X0)|nil=X0)),
% 53.35/7.23 inference(cnf_transformation,[status(thm)],[f330])).
% 53.35/7.23 fof(f334,plain,(
% 53.35/7.23 ![X0,X1]: (~ssItem(X0)|~ssList(X1)|app(cons(X0,nil),X1)=cons(X0,X1))),
% 53.35/7.23 inference(cnf_transformation,[status(thm)],[f120])).
% 53.35/7.23 fof(f434,plain,(
% 53.35/7.23 ssList(sk1)),
% 53.35/7.23 inference(cnf_transformation,[status(thm)],[f186])).
% 53.35/7.23 fof(f435,plain,(
% 53.35/7.23 ssList(sk2)),
% 53.35/7.23 inference(cnf_transformation,[status(thm)],[f187])).
% 53.35/7.23 fof(f438,plain,(
% 53.35/7.23 sk2=sk4),
% 53.35/7.23 inference(cnf_transformation,[status(thm)],[f190])).
% 53.35/7.23 fof(f439,plain,(
% 53.35/7.23 sk1=sk3),
% 53.35/7.23 inference(cnf_transformation,[status(thm)],[f191])).
% 53.35/7.23 fof(f440,plain,(
% 53.35/7.23 neq(sk2,nil)|neq(sk2,nil)),
% 53.35/7.23 inference(cnf_transformation,[status(thm)],[f192])).
% 53.35/7.23 fof(f448,plain,(
% 53.35/7.23 ssItem(sk5)|~neq(sk4,nil)),
% 53.35/7.23 inference(cnf_transformation,[status(thm)],[f199])).
% 53.35/7.23 fof(f449,plain,(
% 53.35/7.23 ssList(sk6)|~neq(sk4,nil)),
% 53.35/7.23 inference(cnf_transformation,[status(thm)],[f200])).
% 53.35/7.23 fof(f450,plain,(
% 53.35/7.23 app(cons(sk5,nil),sk6)=sk3|~neq(sk4,nil)),
% 53.35/7.23 inference(cnf_transformation,[status(thm)],[f201])).
% 53.35/7.23 fof(f451,plain,(
% 53.35/7.23 app(sk6,cons(sk5,nil))=sk4|~neq(sk4,nil)),
% 53.35/7.23 inference(cnf_transformation,[status(thm)],[f202])).
% 53.35/7.23 fof(f452,plain,(
% 53.35/7.23 ((((![D]: ((![C]: (((![A,B]: (((((~ssList(A)|~sk2=A)|~ssList(B))|~ssList(C))|~tl(sk1)=B)|~app(B,C)=A))|~ssItem(D))|~cons(D,nil)=C))|~hd(sk1)=D))|~neq(nil,sk1))|~neq(nil,sk1))|~neq(sk1,nil))|~neq(sk4,nil)),
% 53.35/7.23 inference(miniscoping,[status(thm)],[f203])).
% 53.35/7.23 fof(f453,plain,(
% 53.35/7.23 ![X0,X1,X2,X3]: (~ssList(X0)|~sk2=X0|~ssList(X1)|~ssList(X2)|~tl(sk1)=X1|~app(X1,X2)=X0|~ssItem(X3)|~cons(X3,nil)=X2|~hd(sk1)=X3|~neq(nil,sk1)|~neq(nil,sk1)|~neq(sk1,nil)|~neq(sk4,nil))),
% 53.35/7.23 inference(cnf_transformation,[status(thm)],[f452])).
% 53.35/7.23 fof(f487,plain,(
% 53.35/7.23 neq(sk2,nil)),
% 53.35/7.23 inference(duplicate_literals_removal,[status(thm)],[f440])).
% 53.35/7.23 fof(f492,plain,(
% 53.35/7.23 ssItem(sk5)|~neq(sk2,nil)),
% 53.35/7.23 inference(forward_demodulation,[status(thm)],[f438,f448])).
% 53.35/7.23 fof(f493,plain,(
% 53.35/7.23 ssItem(sk5)),
% 53.35/7.23 inference(forward_subsumption_resolution,[status(thm)],[f492,f487])).
% 53.35/7.23 fof(f494,plain,(
% 53.35/7.23 ssList(sk6)|~neq(sk2,nil)),
% 53.35/7.23 inference(forward_demodulation,[status(thm)],[f438,f449])).
% 53.35/7.23 fof(f495,plain,(
% 53.35/7.23 ssList(sk6)),
% 53.35/7.23 inference(forward_subsumption_resolution,[status(thm)],[f494,f487])).
% 53.35/7.23 fof(f496,plain,(
% 53.35/7.23 app(cons(sk5,nil),sk6)=sk1|~neq(sk4,nil)),
% 53.35/7.23 inference(forward_demodulation,[status(thm)],[f439,f450])).
% 53.35/7.23 fof(f497,plain,(
% 53.35/7.23 app(cons(sk5,nil),sk6)=sk1|~neq(sk2,nil)),
% 53.35/7.23 inference(forward_demodulation,[status(thm)],[f438,f496])).
% 53.35/7.23 fof(f498,plain,(
% 53.35/7.23 app(cons(sk5,nil),sk6)=sk1),
% 53.35/7.23 inference(forward_subsumption_resolution,[status(thm)],[f497,f487])).
% 53.35/7.23 fof(f499,plain,(
% 53.35/7.23 app(sk6,cons(sk5,nil))=sk2|~neq(sk4,nil)),
% 53.35/7.23 inference(forward_demodulation,[status(thm)],[f438,f451])).
% 53.35/7.23 fof(f500,plain,(
% 53.35/7.23 app(sk6,cons(sk5,nil))=sk2|~neq(sk2,nil)),
% 53.35/7.23 inference(forward_demodulation,[status(thm)],[f438,f499])).
% 53.35/7.23 fof(f501,plain,(
% 53.35/7.23 app(sk6,cons(sk5,nil))=sk2),
% 53.35/7.23 inference(forward_subsumption_resolution,[status(thm)],[f500,f487])).
% 53.35/7.23 fof(f502,plain,(
% 53.35/7.23 ![X0,X1,X2,X3]: (~ssList(X0)|~sk2=X0|~ssList(X1)|~ssList(X2)|~tl(sk1)=X1|~app(X1,X2)=X0|~ssItem(X3)|~cons(X3,nil)=X2|~hd(sk1)=X3|~neq(nil,sk1)|~neq(nil,sk1)|~neq(sk1,nil)|~neq(sk2,nil))),
% 53.35/7.23 inference(forward_demodulation,[status(thm)],[f438,f453])).
% 53.35/7.23 fof(f503,plain,(
% 53.35/7.23 ![X0,X1,X2,X3]: (~ssList(X0)|~sk2=X0|~ssList(X1)|~ssList(X2)|~tl(sk1)=X1|~app(X1,X2)=X0|~ssItem(X3)|~cons(X3,nil)=X2|~hd(sk1)=X3|~neq(nil,sk1)|~neq(sk1,nil)|~neq(sk2,nil))),
% 53.35/7.23 inference(duplicate_literals_removal,[status(thm)],[f502])).
% 53.35/7.23 fof(f504,plain,(
% 53.35/7.23 ~ssList(sk2)|~ssList(tl(sk1))|~ssList(cons(hd(sk1),nil))|~app(tl(sk1),cons(hd(sk1),nil))=sk2|~ssItem(hd(sk1))|~neq(nil,sk1)|~neq(sk1,nil)|~neq(sk2,nil)),
% 53.35/7.23 inference(destructive_equality_resolution,[status(thm)],[f503])).
% 53.35/7.23 fof(f505,plain,(
% 53.35/7.23 ~ssList(tl(sk1))|~ssList(cons(hd(sk1),nil))|~app(tl(sk1),cons(hd(sk1),nil))=sk2|~ssItem(hd(sk1))|~neq(nil,sk1)|~neq(sk1,nil)|~neq(sk2,nil)),
% 53.35/7.23 inference(forward_subsumption_resolution,[status(thm)],[f504,f435])).
% 53.35/7.23 fof(f513,plain,(
% 53.35/7.23 ![X0]: (~ssList(X0)|nil=X0|app(tl(X0),nil)=tl(X0))),
% 53.35/7.23 inference(resolution,[status(thm)],[f279,f277])).
% 53.35/7.23 fof(f530,plain,(
% 53.35/7.23 ![X0,X1]: (~ssList(X0)|ssList(app(tl(X1),X0))|~ssList(X1)|nil=X1)),
% 53.35/7.23 inference(resolution,[status(thm)],[f289,f279])).
% 53.35/7.23 fof(f534,plain,(
% 53.35/7.23 ![X0]: (~ssList(X0)|ssList(cons(sk5,X0)))),
% 53.35/7.23 inference(resolution,[status(thm)],[f290,f493])).
% 53.35/7.23 fof(f535,plain,(
% 53.35/7.23 ![X0,X1]: (~ssList(X0)|ssList(cons(hd(X1),X0))|~ssList(X1)|nil=X1)),
% 53.35/7.23 inference(resolution,[status(thm)],[f290,f280])).
% 53.35/7.23 fof(f576,plain,(
% 53.35/7.23 ![X0]: (~ssList(X0)|tl(cons(sk5,X0))=X0)),
% 53.35/7.23 inference(resolution,[status(thm)],[f300,f493])).
% 53.35/7.23 fof(f580,plain,(
% 53.35/7.23 ![X0]: (~ssList(X0)|hd(cons(sk5,X0))=sk5)),
% 53.35/7.23 inference(resolution,[status(thm)],[f301,f493])).
% 53.35/7.23 fof(f584,plain,(
% 53.35/7.23 ![X0]: (~cons(sk5,X0)=nil|~ssList(X0))),
% 53.35/7.23 inference(resolution,[status(thm)],[f303,f493])).
% 53.35/7.23 fof(f643,plain,(
% 53.35/7.23 ~ssList(sk1)|~ssList(nil)|nil=sk1|~ssList(tl(sk1))|~ssList(cons(hd(sk1),nil))|~app(tl(sk1),cons(hd(sk1),nil))=sk2|~ssItem(hd(sk1))|~neq(sk1,nil)|~neq(sk2,nil)),
% 53.35/7.23 inference(resolution,[status(thm)],[f306,f505])).
% 53.35/7.23 fof(f649,plain,(
% 53.35/7.23 ~ssList(nil)|nil=sk1|~ssList(tl(sk1))|~ssList(cons(hd(sk1),nil))|~app(tl(sk1),cons(hd(sk1),nil))=sk2|~ssItem(hd(sk1))|~neq(sk1,nil)|~neq(sk2,nil)),
% 53.35/7.23 inference(forward_subsumption_resolution,[status(thm)],[f643,f434])).
% 53.35/7.23 fof(f675,plain,(
% 53.35/7.23 ![X0]: (~app(X0,sk6)=nil|~ssList(X0)|nil=X0)),
% 53.35/7.23 inference(resolution,[status(thm)],[f331,f495])).
% 53.35/7.23 fof(f709,plain,(
% 53.35/7.23 ![X0]: (~app(cons(sk5,X0),sk6)=nil|nil=cons(sk5,X0)|~ssList(X0))),
% 53.35/7.23 inference(resolution,[status(thm)],[f675,f534])).
% 53.35/7.23 fof(f719,plain,(
% 53.35/7.23 ![X0]: (~app(cons(sk5,X0),sk6)=nil|~ssList(X0))),
% 53.35/7.23 inference(forward_subsumption_resolution,[status(thm)],[f709,f584])).
% 53.35/7.23 fof(f818,plain,(
% 53.35/7.23 ~app(cons(sk5,nil),sk6)=nil),
% 53.35/7.23 inference(resolution,[status(thm)],[f719,f211])).
% 53.35/7.23 fof(f825,plain,(
% 53.35/7.23 ~ssList(nil)|~ssList(tl(sk1))|~ssList(cons(hd(sk1),nil))|~app(tl(sk1),cons(hd(sk1),nil))=sk2|~ssItem(hd(sk1))|~neq(sk1,nil)|~neq(sk2,nil)),
% 53.35/7.23 inference(backward_subsumption_resolution,[status(thm)],[f649,f826])).
% 53.35/7.23 fof(f826,plain,(
% 53.35/7.23 ~sk1=nil),
% 53.35/7.23 inference(forward_demodulation,[status(thm)],[f498,f818])).
% 53.35/7.23 fof(f828,plain,(
% 53.35/7.23 ~ssList(tl(sk1))|~ssList(cons(hd(sk1),nil))|~app(tl(sk1),cons(hd(sk1),nil))=sk2|~ssItem(hd(sk1))|~neq(sk1,nil)|~neq(sk2,nil)),
% 53.35/7.23 inference(forward_subsumption_resolution,[status(thm)],[f825,f211])).
% 53.35/7.23 fof(f848,plain,(
% 53.35/7.23 ![X0]: (~ssList(X0)|app(cons(sk5,nil),X0)=cons(sk5,X0))),
% 53.35/7.23 inference(resolution,[status(thm)],[f334,f493])).
% 53.35/7.23 fof(f1199,plain,(
% 53.35/7.23 tl(cons(sk5,sk6))=sk6),
% 53.35/7.23 inference(resolution,[status(thm)],[f576,f495])).
% 53.35/7.23 fof(f1467,plain,(
% 53.35/7.23 hd(cons(sk5,sk6))=sk5),
% 53.35/7.23 inference(resolution,[status(thm)],[f580,f495])).
% 53.35/7.23 fof(f1509,plain,(
% 53.35/7.23 nil=sk1|app(tl(sk1),nil)=tl(sk1)),
% 53.35/7.23 inference(resolution,[status(thm)],[f513,f434])).
% 53.35/7.23 fof(f1511,plain,(
% 53.35/7.23 app(tl(sk1),nil)=tl(sk1)),
% 53.35/7.23 inference(forward_subsumption_resolution,[status(thm)],[f1509,f826])).
% 53.35/7.23 fof(f2754,plain,(
% 53.35/7.23 ![X0]: (~ssList(X0)|ssList(app(tl(sk1),X0))|nil=sk1)),
% 53.35/7.23 inference(resolution,[status(thm)],[f530,f434])).
% 53.35/7.23 fof(f2756,plain,(
% 53.35/7.23 ![X0]: (~ssList(X0)|ssList(app(tl(sk1),X0)))),
% 53.35/7.23 inference(forward_subsumption_resolution,[status(thm)],[f2754,f826])).
% 53.35/7.23 fof(f2780,plain,(
% 53.35/7.23 ssList(app(tl(sk1),nil))),
% 53.35/7.23 inference(resolution,[status(thm)],[f2756,f211])).
% 53.35/7.23 fof(f2800,plain,(
% 53.35/7.23 ~ssList(cons(hd(sk1),nil))|~app(tl(sk1),cons(hd(sk1),nil))=sk2|~ssItem(hd(sk1))|~neq(sk1,nil)|~neq(sk2,nil)),
% 53.35/7.23 inference(backward_subsumption_resolution,[status(thm)],[f828,f2802])).
% 53.35/7.23 fof(f2802,plain,(
% 53.35/7.23 ssList(tl(sk1))),
% 53.35/7.23 inference(forward_demodulation,[status(thm)],[f1511,f2780])).
% 53.35/7.23 fof(f2804,plain,(
% 53.35/7.23 ~ssList(cons(hd(sk1),nil))|~app(tl(sk1),cons(hd(sk1),nil))=sk2|~ssItem(hd(sk1))|~neq(sk1,nil)),
% 53.35/7.28 inference(forward_subsumption_resolution,[status(thm)],[f2800,f487])).
% 53.35/7.28 fof(f3241,plain,(
% 53.35/7.28 ![X0]: (~ssList(X0)|ssList(cons(hd(sk1),X0))|nil=sk1)),
% 53.35/7.28 inference(resolution,[status(thm)],[f535,f434])).
% 53.35/7.28 fof(f3243,plain,(
% 53.35/7.28 ![X0]: (~ssList(X0)|ssList(cons(hd(sk1),X0)))),
% 53.35/7.28 inference(forward_subsumption_resolution,[status(thm)],[f3241,f826])).
% 53.35/7.28 fof(f3294,plain,(
% 53.35/7.28 ssList(cons(hd(sk1),nil))),
% 53.35/7.28 inference(resolution,[status(thm)],[f3243,f211])).
% 53.35/7.28 fof(f3297,plain,(
% 53.35/7.28 ~app(tl(sk1),cons(hd(sk1),nil))=sk2|~ssItem(hd(sk1))|~neq(sk1,nil)),
% 53.35/7.28 inference(backward_subsumption_resolution,[status(thm)],[f2804,f3294])).
% 53.35/7.28 fof(f3663,plain,(
% 53.35/7.28 app(cons(sk5,nil),sk6)=cons(sk5,sk6)),
% 53.35/7.28 inference(resolution,[status(thm)],[f848,f495])).
% 53.35/7.28 fof(f3669,plain,(
% 53.35/7.28 hd(sk1)=sk5),
% 53.35/7.28 inference(backward_demodulation,[status(thm)],[f3676,f1467])).
% 53.35/7.28 fof(f3670,plain,(
% 53.35/7.28 tl(sk1)=sk6),
% 53.35/7.28 inference(backward_demodulation,[status(thm)],[f3676,f1199])).
% 53.35/7.28 fof(f3676,plain,(
% 53.35/7.28 sk1=cons(sk5,sk6)),
% 53.35/7.28 inference(forward_demodulation,[status(thm)],[f498,f3663])).
% 53.35/7.28 fof(f3684,plain,(
% 53.35/7.28 ~app(tl(sk1),cons(hd(sk1),nil))=sk2|~ssItem(sk5)|~neq(sk1,nil)),
% 53.35/7.28 inference(backward_demodulation,[status(thm)],[f3669,f3297])).
% 53.35/7.28 fof(f3760,plain,(
% 53.35/7.28 ~app(sk6,cons(hd(sk1),nil))=sk2|~ssItem(sk5)|~neq(sk1,nil)),
% 53.35/7.28 inference(forward_demodulation,[status(thm)],[f3670,f3684])).
% 53.35/7.28 fof(f3761,plain,(
% 53.35/7.28 ~app(sk6,cons(sk5,nil))=sk2|~ssItem(sk5)|~neq(sk1,nil)),
% 53.35/7.28 inference(forward_demodulation,[status(thm)],[f3669,f3760])).
% 53.35/7.28 fof(f3762,plain,(
% 53.35/7.28 ~sk2=sk2|~ssItem(sk5)|~neq(sk1,nil)),
% 53.35/7.28 inference(forward_demodulation,[status(thm)],[f501,f3761])).
% 53.35/7.28 fof(f3763,plain,(
% 53.35/7.28 ~ssItem(sk5)|~neq(sk1,nil)),
% 53.35/7.28 inference(trivial_equality_resolution,[status(thm)],[f3762])).
% 53.35/7.28 fof(f3764,plain,(
% 53.35/7.28 ~neq(sk1,nil)),
% 53.35/7.28 inference(forward_subsumption_resolution,[status(thm)],[f3763,f493])).
% 53.35/7.28 fof(f3830,plain,(
% 53.35/7.28 ~ssList(nil)|~ssList(sk1)|sk1=nil),
% 53.35/7.28 inference(resolution,[status(thm)],[f3764,f306])).
% 53.35/7.28 fof(f3831,plain,(
% 53.35/7.28 ~ssList(sk1)|sk1=nil),
% 53.35/7.28 inference(forward_subsumption_resolution,[status(thm)],[f3830,f211])).
% 53.35/7.28 fof(f3891,plain,(
% 53.35/7.28 sk1=nil),
% 53.35/7.28 inference(resolution,[status(thm)],[f3831,f434])).
% 53.35/7.28 fof(f3892,plain,(
% 53.35/7.28 $false),
% 53.35/7.28 inference(forward_subsumption_resolution,[status(thm)],[f3891,f826])).
% 53.35/7.28 % SZS output end CNFRefutation for theBenchmark.p
% 9.09/7.33 % Elapsed time: 6.956499 seconds
% 9.09/7.33 % CPU time: 54.283043 seconds
% 9.09/7.33 % Total memory used: 481.448 MB
% 9.09/7.33 % Net memory used: 459.321 MB
%------------------------------------------------------------------------------