%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWC412-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 : n012.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:24 PM UTC 2026
% Result : Unsatisfiable 0.03s 0.34s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SWC412-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/0.29 % Computer : n012.cluster.edu
% 0.03/0.29 % Model : x86_64 x86_64
% 0.03/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.29 % Memory : 8046.5625MB
% 0.03/0.29 % OS : Linux 6.8.0-71-generic
% 0.03/0.29 % CPULimit : 300
% 0.03/0.29 % WCLimit : 300
% 0.03/0.29 % DateTime : Mon Sep 21 08:22:22 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.31 % Drodi V4.1.1
% 0.03/0.34 % Refutation found
% 0.03/0.34 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.03/0.34 % SZS output start CNFRefutation for theBenchmark
% 0.03/0.34 fof(f8,axiom,(
% 0.03/0.34 ssList(nil) ),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f73,axiom,(
% 0.03/0.34 (![U]: (( ~ ssList(U)| app(U,nil) = U ) ))),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f85,axiom,(
% 0.03/0.34 (![U,V]: (( ~ ssList(U)| ~ ssList(V)| ssList(app(V,U)) ) ))),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f119,axiom,(
% 0.03/0.34 (![U,V]: (( app(U,V) != nil| ~ ssList(V)| ~ ssList(U)| nil = V ) ))),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f186,negated_conjecture,(
% 0.03/0.34 ssList(sk1) ),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f189,negated_conjecture,(
% 0.03/0.34 ssList(sk4) ),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f190,negated_conjecture,(
% 0.03/0.34 sk2 = sk4 ),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f191,negated_conjecture,(
% 0.03/0.34 sk1 = sk3 ),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f192,negated_conjecture,(
% 0.03/0.34 (![A,B,C,D,E,F]: (( ~ ssItem(A)| ~ ssItem(B)| ~ ssList(C)| app(app(cons(A,nil),cons(B,nil)),C) != sk4| ~ ssItem(D)| ~ ssItem(E)| ~ ssList(F)| app(app(cons(E,nil),F),cons(D,nil)) = sk3| app(app(cons(D,nil),F),cons(E,nil)) != sk4 ) ))),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f197,negated_conjecture,(
% 0.03/0.34 (![A,B,C]: (( ~ ssItem(A)| ~ ssItem(B)| ~ ssList(C)| app(app(cons(A,nil),cons(B,nil)),C) != sk4| ssItem(sk11) ) ))),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f198,negated_conjecture,(
% 0.03/0.34 (![A,B,C]: (( ~ ssItem(A)| ~ ssItem(B)| ~ ssList(C)| app(app(cons(A,nil),cons(B,nil)),C) != sk4| ssItem(sk12) ) ))),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f199,negated_conjecture,(
% 0.03/0.34 (![A,B,C]: (( ~ ssItem(A)| ~ ssItem(B)| ~ ssList(C)| app(app(cons(A,nil),cons(B,nil)),C) != sk4| ssList(sk13) ) ))),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f200,negated_conjecture,(
% 0.03/0.34 (![A,B,C]: (( ~ ssItem(A)| ~ ssItem(B)| ~ ssList(C)| app(app(cons(A,nil),cons(B,nil)),C) != sk4| app(app(cons(sk11,nil),sk13),cons(sk12,nil)) = sk2 ) ))),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f201,negated_conjecture,(
% 0.03/0.34 (![A,B,C]: (( ~ ssItem(A)| ~ ssItem(B)| ~ ssList(C)| app(app(cons(A,nil),cons(B,nil)),C) != sk4| app(app(cons(sk12,nil),sk13),cons(sk11,nil)) != sk1 ) ))),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f202,negated_conjecture,(
% 0.03/0.34 (![A,B,C]: (( ssItem(sk5)| ~ ssItem(A)| ~ ssItem(B)| ~ ssList(C)| app(app(cons(B,nil),C),cons(A,nil)) = sk3| app(app(cons(A,nil),C),cons(B,nil)) != sk4 ) ))),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f203,negated_conjecture,(
% 0.03/0.34 (![A,B,C]: (( ssItem(sk6)| ~ ssItem(A)| ~ ssItem(B)| ~ ssList(C)| app(app(cons(B,nil),C),cons(A,nil)) = sk3| app(app(cons(A,nil),C),cons(B,nil)) != sk4 ) ))),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f204,negated_conjecture,(
% 0.03/0.34 (![A,B,C]: (( ssList(sk7)| ~ ssItem(A)| ~ ssItem(B)| ~ ssList(C)| app(app(cons(B,nil),C),cons(A,nil)) = sk3| app(app(cons(A,nil),C),cons(B,nil)) != sk4 ) ))),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f205,negated_conjecture,(
% 0.03/0.34 (![A,B,C]: (( app(app(cons(sk5,nil),cons(sk6,nil)),sk7) = sk2| ~ ssItem(A)| ~ ssItem(B)| ~ ssList(C)| app(app(cons(B,nil),C),cons(A,nil)) = sk3| app(app(cons(A,nil),C),cons(B,nil)) != sk4 ) ))),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f210,negated_conjecture,(
% 0.03/0.34 ( ssItem(sk5)| ssItem(sk11) ) ),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f211,negated_conjecture,(
% 0.03/0.34 ( ssItem(sk5)| ssItem(sk12) ) ),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f212,negated_conjecture,(
% 0.03/0.34 ( ssItem(sk5)| ssList(sk13) ) ),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f213,negated_conjecture,(
% 0.03/0.34 ( ssItem(sk5)| app(app(cons(sk11,nil),sk13),cons(sk12,nil)) = sk2 ) ),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f214,negated_conjecture,(
% 0.03/0.34 ( ssItem(sk5)| app(app(cons(sk12,nil),sk13),cons(sk11,nil)) != sk1 ) ),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f227,negated_conjecture,(
% 0.03/0.34 ( ssItem(sk6)| ssItem(sk11) ) ),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f228,negated_conjecture,(
% 0.03/0.34 ( ssItem(sk6)| ssItem(sk12) ) ),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f229,negated_conjecture,(
% 0.03/0.34 ( ssItem(sk6)| ssList(sk13) ) ),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f230,negated_conjecture,(
% 0.03/0.34 ( ssItem(sk6)| app(app(cons(sk11,nil),sk13),cons(sk12,nil)) = sk2 ) ),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f231,negated_conjecture,(
% 0.03/0.34 ( ssItem(sk6)| app(app(cons(sk12,nil),sk13),cons(sk11,nil)) != sk1 ) ),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f232,negated_conjecture,(
% 0.03/0.34 ( ssList(sk7)| ssItem(sk11) ) ),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f233,negated_conjecture,(
% 0.03/0.34 ( app(app(cons(sk5,nil),cons(sk6,nil)),sk7) = sk2| ssItem(sk11) ) ),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f234,negated_conjecture,(
% 0.03/0.34 ( ssList(sk7)| ssItem(sk12) ) ),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f235,negated_conjecture,(
% 0.03/0.34 ( ssList(sk7)| ssList(sk13) ) ),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f236,negated_conjecture,(
% 0.03/0.34 ( ssList(sk7)| app(app(cons(sk11,nil),sk13),cons(sk12,nil)) = sk2 ) ),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f237,negated_conjecture,(
% 0.03/0.34 ( ssList(sk7)| app(app(cons(sk12,nil),sk13),cons(sk11,nil)) != sk1 ) ),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f238,negated_conjecture,(
% 0.03/0.34 ( app(app(cons(sk5,nil),cons(sk6,nil)),sk7) = sk2| ssItem(sk12) ) ),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f239,negated_conjecture,(
% 0.03/0.34 ( app(app(cons(sk5,nil),cons(sk6,nil)),sk7) = sk2| ssList(sk13) ) ),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f240,negated_conjecture,(
% 0.03/0.34 ( app(app(cons(sk5,nil),cons(sk6,nil)),sk7) = sk2| app(app(cons(sk11,nil),sk13),cons(sk12,nil)) = sk2 ) ),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f241,negated_conjecture,(
% 0.03/0.34 ( app(app(cons(sk5,nil),cons(sk6,nil)),sk7) = sk2| app(app(cons(sk12,nil),sk13),cons(sk11,nil)) != sk1 ) ),
% 0.03/0.34 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.34 fof(f249,plain,(
% 0.03/0.34 ssList(nil)),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f8])).
% 0.03/0.34 fof(f315,plain,(
% 0.03/0.34 ![X0]: (~ssList(X0)|app(X0,nil)=X0)),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f73])).
% 0.03/0.34 fof(f327,plain,(
% 0.03/0.34 ![X0,X1]: (~ssList(X0)|~ssList(X1)|ssList(app(X1,X0)))),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f85])).
% 0.03/0.34 fof(f370,plain,(
% 0.03/0.34 ![V]: ((![U]: ((~app(U,V)=nil|~ssList(V))|~ssList(U)))|nil=V)),
% 0.03/0.34 inference(miniscoping,[status(thm)],[f119])).
% 0.03/0.34 fof(f371,plain,(
% 0.03/0.34 ![X0,X1]: (~app(X0,X1)=nil|~ssList(X1)|~ssList(X0)|nil=X1)),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f370])).
% 0.03/0.34 fof(f472,plain,(
% 0.03/0.34 ssList(sk1)),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f186])).
% 0.03/0.34 fof(f475,plain,(
% 0.03/0.34 ssList(sk4)),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f189])).
% 0.03/0.34 fof(f476,plain,(
% 0.03/0.34 sk2=sk4),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f190])).
% 0.03/0.34 fof(f477,plain,(
% 0.03/0.34 sk1=sk3),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f191])).
% 0.03/0.34 fof(f478,plain,(
% 0.03/0.34 ![D,E,F]: ((((((![A,B,C]: (((~ssItem(A)|~ssItem(B))|~ssList(C))|~app(app(cons(A,nil),cons(B,nil)),C)=sk4))|~ssItem(D))|~ssItem(E))|~ssList(F))|app(app(cons(E,nil),F),cons(D,nil))=sk3)|~app(app(cons(D,nil),F),cons(E,nil))=sk4)),
% 0.03/0.34 inference(miniscoping,[status(thm)],[f192])).
% 0.03/0.34 fof(f479,plain,(
% 0.03/0.34 ![X0,X1,X2,X3,X4,X5]: (~ssItem(X0)|~ssItem(X1)|~ssList(X2)|~app(app(cons(X0,nil),cons(X1,nil)),X2)=sk4|~ssItem(X3)|~ssItem(X4)|~ssList(X5)|app(app(cons(X4,nil),X5),cons(X3,nil))=sk3|~app(app(cons(X3,nil),X5),cons(X4,nil))=sk4)),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f478])).
% 0.03/0.34 fof(f488,plain,(
% 0.03/0.34 (![A,B,C]: (((~ssItem(A)|~ssItem(B))|~ssList(C))|~app(app(cons(A,nil),cons(B,nil)),C)=sk4))|ssItem(sk11)),
% 0.03/0.34 inference(miniscoping,[status(thm)],[f197])).
% 0.03/0.34 fof(f489,plain,(
% 0.03/0.34 ![X0,X1,X2]: (~ssItem(X0)|~ssItem(X1)|~ssList(X2)|~app(app(cons(X0,nil),cons(X1,nil)),X2)=sk4|ssItem(sk11))),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f488])).
% 0.03/0.34 fof(f490,plain,(
% 0.03/0.34 (![A,B,C]: (((~ssItem(A)|~ssItem(B))|~ssList(C))|~app(app(cons(A,nil),cons(B,nil)),C)=sk4))|ssItem(sk12)),
% 0.03/0.34 inference(miniscoping,[status(thm)],[f198])).
% 0.03/0.34 fof(f491,plain,(
% 0.03/0.34 ![X0,X1,X2]: (~ssItem(X0)|~ssItem(X1)|~ssList(X2)|~app(app(cons(X0,nil),cons(X1,nil)),X2)=sk4|ssItem(sk12))),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f490])).
% 0.03/0.34 fof(f492,plain,(
% 0.03/0.34 (![A,B,C]: (((~ssItem(A)|~ssItem(B))|~ssList(C))|~app(app(cons(A,nil),cons(B,nil)),C)=sk4))|ssList(sk13)),
% 0.03/0.34 inference(miniscoping,[status(thm)],[f199])).
% 0.03/0.34 fof(f493,plain,(
% 0.03/0.34 ![X0,X1,X2]: (~ssItem(X0)|~ssItem(X1)|~ssList(X2)|~app(app(cons(X0,nil),cons(X1,nil)),X2)=sk4|ssList(sk13))),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f492])).
% 0.03/0.34 fof(f494,plain,(
% 0.03/0.34 (![A,B,C]: (((~ssItem(A)|~ssItem(B))|~ssList(C))|~app(app(cons(A,nil),cons(B,nil)),C)=sk4))|app(app(cons(sk11,nil),sk13),cons(sk12,nil))=sk2),
% 0.03/0.34 inference(miniscoping,[status(thm)],[f200])).
% 0.03/0.34 fof(f495,plain,(
% 0.03/0.34 ![X0,X1,X2]: (~ssItem(X0)|~ssItem(X1)|~ssList(X2)|~app(app(cons(X0,nil),cons(X1,nil)),X2)=sk4|app(app(cons(sk11,nil),sk13),cons(sk12,nil))=sk2)),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f494])).
% 0.03/0.34 fof(f496,plain,(
% 0.03/0.34 (![A,B,C]: (((~ssItem(A)|~ssItem(B))|~ssList(C))|~app(app(cons(A,nil),cons(B,nil)),C)=sk4))|~app(app(cons(sk12,nil),sk13),cons(sk11,nil))=sk1),
% 0.03/0.34 inference(miniscoping,[status(thm)],[f201])).
% 0.03/0.34 fof(f497,plain,(
% 0.03/0.34 ![X0,X1,X2]: (~ssItem(X0)|~ssItem(X1)|~ssList(X2)|~app(app(cons(X0,nil),cons(X1,nil)),X2)=sk4|~app(app(cons(sk12,nil),sk13),cons(sk11,nil))=sk1)),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f496])).
% 0.03/0.34 fof(f498,plain,(
% 0.03/0.34 ![X0,X1,X2]: (ssItem(sk5)|~ssItem(X0)|~ssItem(X1)|~ssList(X2)|app(app(cons(X1,nil),X2),cons(X0,nil))=sk3|~app(app(cons(X0,nil),X2),cons(X1,nil))=sk4)),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f202])).
% 0.03/0.34 fof(f499,plain,(
% 0.03/0.34 ![X0,X1,X2]: (ssItem(sk6)|~ssItem(X0)|~ssItem(X1)|~ssList(X2)|app(app(cons(X1,nil),X2),cons(X0,nil))=sk3|~app(app(cons(X0,nil),X2),cons(X1,nil))=sk4)),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f203])).
% 0.03/0.34 fof(f500,plain,(
% 0.03/0.34 ![X0,X1,X2]: (ssList(sk7)|~ssItem(X0)|~ssItem(X1)|~ssList(X2)|app(app(cons(X1,nil),X2),cons(X0,nil))=sk3|~app(app(cons(X0,nil),X2),cons(X1,nil))=sk4)),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f204])).
% 0.03/0.34 fof(f501,plain,(
% 0.03/0.34 ![X0,X1,X2]: (app(app(cons(sk5,nil),cons(sk6,nil)),sk7)=sk2|~ssItem(X0)|~ssItem(X1)|~ssList(X2)|app(app(cons(X1,nil),X2),cons(X0,nil))=sk3|~app(app(cons(X0,nil),X2),cons(X1,nil))=sk4)),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f205])).
% 0.03/0.34 fof(f506,plain,(
% 0.03/0.34 ssItem(sk5)|ssItem(sk11)),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f210])).
% 0.03/0.34 fof(f507,plain,(
% 0.03/0.34 ssItem(sk5)|ssItem(sk12)),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f211])).
% 0.03/0.34 fof(f508,plain,(
% 0.03/0.34 ssItem(sk5)|ssList(sk13)),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f212])).
% 0.03/0.34 fof(f509,plain,(
% 0.03/0.34 ssItem(sk5)|app(app(cons(sk11,nil),sk13),cons(sk12,nil))=sk2),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f213])).
% 0.03/0.34 fof(f510,plain,(
% 0.03/0.34 ssItem(sk5)|~app(app(cons(sk12,nil),sk13),cons(sk11,nil))=sk1),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f214])).
% 0.03/0.34 fof(f523,plain,(
% 0.03/0.34 ssItem(sk6)|ssItem(sk11)),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f227])).
% 0.03/0.34 fof(f524,plain,(
% 0.03/0.34 ssItem(sk6)|ssItem(sk12)),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f228])).
% 0.03/0.34 fof(f525,plain,(
% 0.03/0.34 ssItem(sk6)|ssList(sk13)),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f229])).
% 0.03/0.34 fof(f526,plain,(
% 0.03/0.34 ssItem(sk6)|app(app(cons(sk11,nil),sk13),cons(sk12,nil))=sk2),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f230])).
% 0.03/0.34 fof(f527,plain,(
% 0.03/0.34 ssItem(sk6)|~app(app(cons(sk12,nil),sk13),cons(sk11,nil))=sk1),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f231])).
% 0.03/0.34 fof(f528,plain,(
% 0.03/0.34 ssList(sk7)|ssItem(sk11)),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f232])).
% 0.03/0.34 fof(f529,plain,(
% 0.03/0.34 app(app(cons(sk5,nil),cons(sk6,nil)),sk7)=sk2|ssItem(sk11)),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f233])).
% 0.03/0.34 fof(f530,plain,(
% 0.03/0.34 ssList(sk7)|ssItem(sk12)),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f234])).
% 0.03/0.34 fof(f531,plain,(
% 0.03/0.34 ssList(sk7)|ssList(sk13)),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f235])).
% 0.03/0.34 fof(f532,plain,(
% 0.03/0.34 ssList(sk7)|app(app(cons(sk11,nil),sk13),cons(sk12,nil))=sk2),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f236])).
% 0.03/0.34 fof(f533,plain,(
% 0.03/0.34 ssList(sk7)|~app(app(cons(sk12,nil),sk13),cons(sk11,nil))=sk1),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f237])).
% 0.03/0.34 fof(f534,plain,(
% 0.03/0.34 app(app(cons(sk5,nil),cons(sk6,nil)),sk7)=sk2|ssItem(sk12)),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f238])).
% 0.03/0.34 fof(f535,plain,(
% 0.03/0.34 app(app(cons(sk5,nil),cons(sk6,nil)),sk7)=sk2|ssList(sk13)),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f239])).
% 0.03/0.34 fof(f536,plain,(
% 0.03/0.34 app(app(cons(sk5,nil),cons(sk6,nil)),sk7)=sk2|app(app(cons(sk11,nil),sk13),cons(sk12,nil))=sk2),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f240])).
% 0.03/0.34 fof(f537,plain,(
% 0.03/0.34 app(app(cons(sk5,nil),cons(sk6,nil)),sk7)=sk2|~app(app(cons(sk12,nil),sk13),cons(sk11,nil))=sk1),
% 0.03/0.34 inference(cnf_transformation,[status(thm)],[f241])).
% 0.03/0.34 fof(f545,definition,(
% 0.03/0.34 ![X0,X1,X2]: (sQ2_spl <=> (~ssItem(X0)|~ssItem(X1)|~ssList(X2)|~app(app(cons(X0,nil),cons(X1,nil)),X2)=sk4))),
% 0.03/0.34 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.03/0.34 fof(f546,plain,(
% 0.03/0.34 ![X0,X1,X2]: (~ssItem(X0)|~ssItem(X1)|~ssList(X2)|~app(app(cons(X0,nil),cons(X1,nil)),X2)=sk4|~sQ2_spl)),
% 0.03/0.34 inference(component_clause,[status(thm)],[f545])).
% 0.03/0.34 fof(f548,definition,(
% 0.03/0.34 ![X3,X4,X5]: (sQ3_spl <=> (~ssItem(X3)|~ssItem(X4)|~ssList(X5)|app(app(cons(X4,nil),X5),cons(X3,nil))=sk3|~app(app(cons(X3,nil),X5),cons(X4,nil))=sk4))),
% 0.03/0.34 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.03/0.34 fof(f549,plain,(
% 0.03/0.34 ![X0,X1,X2]: (~ssItem(X0)|~ssItem(X1)|~ssList(X2)|app(app(cons(X1,nil),X2),cons(X0,nil))=sk3|~app(app(cons(X0,nil),X2),cons(X1,nil))=sk4|~sQ3_spl)),
% 0.03/0.34 inference(component_clause,[status(thm)],[f548])).
% 0.03/0.34 fof(f551,plain,(
% 0.03/0.34 sQ2_spl|sQ3_spl),
% 0.03/0.34 inference(split_clause,[status(thm)],[f479,f545,f548])).
% 0.03/0.34 fof(f568,definition,(
% 0.03/0.34 sQ8_spl <=> (ssItem(sk11))),
% 0.03/0.34 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.03/0.34 fof(f571,plain,(
% 0.03/0.34 sQ2_spl|sQ8_spl),
% 0.03/0.34 inference(split_clause,[status(thm)],[f489,f545,f568])).
% 0.03/0.34 fof(f572,definition,(
% 0.03/0.34 sQ9_spl <=> (ssItem(sk12))),
% 0.03/0.34 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.03/0.34 fof(f575,plain,(
% 0.03/0.34 sQ2_spl|sQ9_spl),
% 0.03/0.34 inference(split_clause,[status(thm)],[f491,f545,f572])).
% 0.03/0.34 fof(f576,definition,(
% 0.03/0.34 sQ10_spl <=> (ssList(sk13))),
% 0.03/0.34 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.03/0.34 fof(f579,plain,(
% 0.03/0.34 sQ2_spl|sQ10_spl),
% 0.03/0.34 inference(split_clause,[status(thm)],[f493,f545,f576])).
% 0.03/0.34 fof(f580,definition,(
% 0.03/0.34 sQ11_spl <=> (app(app(cons(sk11,nil),sk13),cons(sk12,nil))=sk2)),
% 0.03/0.34 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.03/0.34 fof(f581,plain,(
% 0.03/0.34 app(app(cons(sk11,nil),sk13),cons(sk12,nil))=sk2|~sQ11_spl),
% 0.03/0.34 inference(component_clause,[status(thm)],[f580])).
% 0.03/0.34 fof(f583,plain,(
% 0.03/0.34 sQ2_spl|sQ11_spl),
% 0.03/0.34 inference(split_clause,[status(thm)],[f495,f545,f580])).
% 0.03/0.34 fof(f584,definition,(
% 0.03/0.34 sQ12_spl <=> (app(app(cons(sk12,nil),sk13),cons(sk11,nil))=sk1)),
% 0.03/0.34 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.03/0.34 fof(f587,plain,(
% 0.03/0.34 sQ2_spl|~sQ12_spl),
% 0.03/0.34 inference(split_clause,[status(thm)],[f497,f545,f584])).
% 0.03/0.34 fof(f588,definition,(
% 0.03/0.34 sQ13_spl <=> (ssItem(sk5))),
% 0.03/0.34 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.03/0.34 fof(f591,plain,(
% 0.03/0.34 sQ13_spl|sQ3_spl),
% 0.03/0.34 inference(split_clause,[status(thm)],[f498,f588,f548])).
% 0.03/0.34 fof(f592,definition,(
% 0.03/0.34 sQ14_spl <=> (ssItem(sk6))),
% 0.03/0.34 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.03/0.34 fof(f595,plain,(
% 0.03/0.34 sQ14_spl|sQ3_spl),
% 0.03/0.34 inference(split_clause,[status(thm)],[f499,f592,f548])).
% 0.03/0.34 fof(f596,definition,(
% 0.03/0.34 sQ15_spl <=> (ssList(sk7))),
% 0.03/0.34 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.03/0.34 fof(f597,plain,(
% 0.03/0.34 ssList(sk7)|~sQ15_spl),
% 0.03/0.34 inference(component_clause,[status(thm)],[f596])).
% 0.03/0.34 fof(f599,plain,(
% 0.03/0.34 sQ15_spl|sQ3_spl),
% 0.03/0.34 inference(split_clause,[status(thm)],[f500,f596,f548])).
% 0.03/0.34 fof(f600,definition,(
% 0.03/0.34 sQ16_spl <=> (app(app(cons(sk5,nil),cons(sk6,nil)),sk7)=sk2)),
% 0.03/0.34 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.03/0.34 fof(f601,plain,(
% 0.03/0.34 app(app(cons(sk5,nil),cons(sk6,nil)),sk7)=sk2|~sQ16_spl),
% 0.03/0.34 inference(component_clause,[status(thm)],[f600])).
% 0.03/0.34 fof(f603,plain,(
% 0.03/0.34 sQ16_spl|sQ3_spl),
% 0.03/0.34 inference(split_clause,[status(thm)],[f501,f600,f548])).
% 0.03/0.34 fof(f608,plain,(
% 0.03/0.34 sQ13_spl|sQ8_spl),
% 0.03/0.34 inference(split_clause,[status(thm)],[f506,f588,f568])).
% 0.03/0.34 fof(f609,plain,(
% 0.03/0.34 sQ13_spl|sQ9_spl),
% 0.03/0.34 inference(split_clause,[status(thm)],[f507,f588,f572])).
% 0.03/0.34 fof(f610,plain,(
% 0.03/0.34 sQ13_spl|sQ10_spl),
% 0.03/0.34 inference(split_clause,[status(thm)],[f508,f588,f576])).
% 0.03/0.34 fof(f611,plain,(
% 0.03/0.34 sQ13_spl|sQ11_spl),
% 0.03/0.34 inference(split_clause,[status(thm)],[f509,f588,f580])).
% 0.03/0.34 fof(f612,plain,(
% 0.03/0.34 sQ13_spl|~sQ12_spl),
% 0.03/0.34 inference(split_clause,[status(thm)],[f510,f588,f584])).
% 0.03/0.34 fof(f625,plain,(
% 0.03/0.34 sQ14_spl|sQ8_spl),
% 0.03/0.34 inference(split_clause,[status(thm)],[f523,f592,f568])).
% 0.03/0.34 fof(f626,plain,(
% 0.03/0.34 sQ14_spl|sQ9_spl),
% 0.03/0.34 inference(split_clause,[status(thm)],[f524,f592,f572])).
% 0.03/0.34 fof(f627,plain,(
% 0.03/0.34 sQ14_spl|sQ10_spl),
% 0.03/0.34 inference(split_clause,[status(thm)],[f525,f592,f576])).
% 0.03/0.34 fof(f628,plain,(
% 0.03/0.34 sQ14_spl|sQ11_spl),
% 0.03/0.34 inference(split_clause,[status(thm)],[f526,f592,f580])).
% 0.03/0.34 fof(f629,plain,(
% 0.03/0.34 sQ14_spl|~sQ12_spl),
% 0.03/0.34 inference(split_clause,[status(thm)],[f527,f592,f584])).
% 0.03/0.34 fof(f630,plain,(
% 0.03/0.34 sQ15_spl|sQ8_spl),
% 0.03/0.34 inference(split_clause,[status(thm)],[f528,f596,f568])).
% 0.03/0.34 fof(f631,plain,(
% 0.03/0.34 sQ16_spl|sQ8_spl),
% 0.03/0.34 inference(split_clause,[status(thm)],[f529,f600,f568])).
% 0.03/0.34 fof(f632,plain,(
% 0.03/0.34 sQ15_spl|sQ9_spl),
% 0.03/0.34 inference(split_clause,[status(thm)],[f530,f596,f572])).
% 0.03/0.34 fof(f633,plain,(
% 0.03/0.35 sQ15_spl|sQ10_spl),
% 0.03/0.35 inference(split_clause,[status(thm)],[f531,f596,f576])).
% 0.03/0.35 fof(f634,plain,(
% 0.03/0.35 sQ15_spl|sQ11_spl),
% 0.03/0.35 inference(split_clause,[status(thm)],[f532,f596,f580])).
% 0.03/0.35 fof(f635,plain,(
% 0.03/0.35 sQ15_spl|~sQ12_spl),
% 0.03/0.35 inference(split_clause,[status(thm)],[f533,f596,f584])).
% 0.03/0.35 fof(f636,plain,(
% 0.03/0.35 sQ16_spl|sQ9_spl),
% 0.03/0.35 inference(split_clause,[status(thm)],[f534,f600,f572])).
% 0.03/0.35 fof(f637,plain,(
% 0.03/0.35 sQ16_spl|sQ10_spl),
% 0.03/0.35 inference(split_clause,[status(thm)],[f535,f600,f576])).
% 0.03/0.35 fof(f638,plain,(
% 0.03/0.35 sQ16_spl|sQ11_spl),
% 0.03/0.35 inference(split_clause,[status(thm)],[f536,f600,f580])).
% 0.03/0.35 fof(f639,plain,(
% 0.03/0.35 sQ16_spl|~sQ12_spl),
% 0.03/0.35 inference(split_clause,[status(thm)],[f537,f600,f584])).
% 0.03/0.35 fof(f673,plain,(
% 0.03/0.35 app(sk4,nil)=sk4),
% 0.03/0.35 inference(resolution,[status(thm)],[f315,f475])).
% 0.03/0.35 fof(f674,plain,(
% 0.03/0.35 app(sk1,nil)=sk1),
% 0.03/0.35 inference(resolution,[status(thm)],[f315,f472])).
% 0.03/0.35 fof(f681,plain,(
% 0.03/0.35 app(app(cons(sk5,nil),cons(sk6,nil)),sk7)=sk4|~sQ16_spl),
% 0.03/0.35 inference(forward_demodulation,[status(thm)],[f476,f601])).
% 0.03/0.35 fof(f685,plain,(
% 0.03/0.35 ![X0]: (~ssList(X0)|ssList(app(sk4,X0)))),
% 0.03/0.35 inference(resolution,[status(thm)],[f327,f475])).
% 0.03/0.35 fof(f686,plain,(
% 0.03/0.35 ![X0]: (~ssList(X0)|ssList(app(sk1,X0)))),
% 0.03/0.35 inference(resolution,[status(thm)],[f327,f472])).
% 0.03/0.35 fof(f718,definition,(
% 0.03/0.35 sQ17_spl <=> (ssList(nil))),
% 0.03/0.35 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.03/0.35 fof(f720,plain,(
% 0.03/0.35 ~ssList(nil)|sQ17_spl),
% 0.03/0.35 inference(component_clause,[status(thm)],[f718])).
% 0.03/0.35 fof(f725,plain,(
% 0.03/0.35 ~ssList(nil)|ssList(sk4)),
% 0.03/0.35 inference(paramodulation,[status(thm)],[f673,f685])).
% 0.03/0.35 fof(f726,definition,(
% 0.03/0.35 sQ18_spl <=> (ssList(sk4))),
% 0.03/0.35 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.03/0.35 fof(f729,plain,(
% 0.03/0.35 ~sQ17_spl|sQ18_spl),
% 0.03/0.35 inference(split_clause,[status(thm)],[f725,f718,f726])).
% 0.03/0.35 fof(f730,plain,(
% 0.03/0.35 $false|sQ17_spl),
% 0.03/0.35 inference(forward_subsumption_resolution,[status(thm)],[f720,f249])).
% 0.03/0.35 fof(f731,plain,(
% 0.03/0.35 sQ17_spl),
% 0.03/0.35 inference(contradiction_clause,[status(thm)],[f730])).
% 0.03/0.35 fof(f735,plain,(
% 0.03/0.35 ~ssList(nil)|ssList(sk1)),
% 0.03/0.35 inference(paramodulation,[status(thm)],[f674,f686])).
% 0.03/0.35 fof(f736,definition,(
% 0.03/0.35 sQ19_spl <=> (ssList(sk1))),
% 0.03/0.35 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.03/0.35 fof(f739,plain,(
% 0.03/0.35 ~sQ17_spl|sQ19_spl),
% 0.03/0.35 inference(split_clause,[status(thm)],[f735,f718,f736])).
% 0.03/0.35 fof(f740,plain,(
% 0.03/0.35 ~ssItem(sk5)|~ssItem(sk6)|~ssList(sk7)|~sQ2_spl|~sQ16_spl),
% 0.03/0.35 inference(resolution,[status(thm)],[f546,f681])).
% 0.03/0.35 fof(f742,plain,(
% 0.03/0.35 ~sQ13_spl|~sQ14_spl|~sQ15_spl|~sQ2_spl|~sQ16_spl),
% 0.03/0.35 inference(split_clause,[status(thm)],[f740,f588,f592,f596,f545,f600])).
% 0.03/0.35 fof(f747,plain,(
% 0.03/0.35 ![X0,X1,X2]: (~ssItem(X0)|~ssItem(X1)|~ssList(X2)|app(app(cons(X1,nil),X2),cons(X0,nil))=sk1|~app(app(cons(X0,nil),X2),cons(X1,nil))=sk4|~sQ3_spl)),
% 0.03/0.35 inference(forward_demodulation,[status(thm)],[f477,f549])).
% 0.03/0.35 fof(f749,plain,(
% 0.03/0.35 app(app(cons(sk11,nil),sk13),cons(sk12,nil))=sk4|~sQ11_spl),
% 0.03/0.35 inference(forward_demodulation,[status(thm)],[f476,f581])).
% 0.03/0.35 fof(f877,plain,(
% 0.03/0.35 ![X0]: (~app(X0,sk7)=nil|~ssList(X0)|nil=sk7|~sQ15_spl)),
% 0.03/0.35 inference(resolution,[status(thm)],[f371,f597])).
% 0.03/0.35 fof(f878,plain,(
% 0.03/0.35 ![X0]: (~app(X0,nil)=nil|~ssList(X0)|nil=nil)),
% 0.03/0.35 inference(resolution,[status(thm)],[f371,f249])).
% 0.03/0.35 fof(f879,plain,(
% 0.03/0.35 ![X0]: (~app(X0,sk4)=nil|~ssList(X0)|nil=sk4)),
% 0.03/0.35 inference(resolution,[status(thm)],[f371,f475])).
% 0.03/0.35 fof(f880,plain,(
% 0.03/0.35 ![X0]: (~app(X0,sk1)=nil|~ssList(X0)|nil=sk1)),
% 0.03/0.35 inference(resolution,[status(thm)],[f371,f472])).
% 0.03/0.35 fof(f896,definition,(
% 0.03/0.35 ![X0]: (sQ25_spl <=> (~app(X0,sk7)=nil|~ssList(X0)))),
% 0.03/0.35 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.03/0.35 fof(f899,definition,(
% 0.03/0.35 sQ26_spl <=> (nil=sk7)),
% 0.03/0.35 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.03/0.35 fof(f902,plain,(
% 0.03/0.35 sQ25_spl|sQ26_spl|~sQ15_spl),
% 0.03/0.35 inference(split_clause,[status(thm)],[f877,f896,f899,f596])).
% 0.03/0.35 fof(f903,definition,(
% 0.03/0.35 ![X0]: (sQ27_spl <=> (~app(X0,nil)=nil|~ssList(X0)))),
% 0.03/0.35 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.03/0.35 fof(f906,definition,(
% 0.03/0.35 sQ28_spl <=> (nil=nil)),
% 0.03/0.35 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.03/0.35 fof(f909,plain,(
% 0.03/0.35 sQ27_spl|sQ28_spl),
% 0.03/0.35 inference(split_clause,[status(thm)],[f878,f903,f906])).
% 0.03/0.35 fof(f910,definition,(
% 0.03/0.35 ![X0]: (sQ29_spl <=> (~app(X0,sk4)=nil|~ssList(X0)))),
% 0.03/0.35 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.03/0.35 fof(f913,definition,(
% 0.03/0.35 sQ30_spl <=> (nil=sk4)),
% 0.03/0.35 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.03/0.35 fof(f916,plain,(
% 0.03/0.35 sQ29_spl|sQ30_spl),
% 0.03/0.35 inference(split_clause,[status(thm)],[f879,f910,f913])).
% 0.03/0.35 fof(f917,definition,(
% 0.03/0.35 ![X0]: (sQ31_spl <=> (~app(X0,sk1)=nil|~ssList(X0)))),
% 0.03/0.35 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.03/0.35 fof(f920,definition,(
% 0.03/0.35 sQ32_spl <=> (nil=sk1)),
% 0.03/0.35 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.03/0.35 fof(f923,plain,(
% 0.03/0.35 sQ31_spl|sQ32_spl),
% 0.03/0.35 inference(split_clause,[status(thm)],[f880,f917,f920])).
% 0.03/0.35 fof(f1104,plain,(
% 0.03/0.35 ~ssItem(sk11)|~ssItem(sk12)|~ssList(sk13)|app(app(cons(sk12,nil),sk13),cons(sk11,nil))=sk1|~sQ11_spl|~sQ3_spl),
% 0.03/0.35 inference(resolution,[status(thm)],[f749,f747])).
% 0.03/0.35 fof(f1106,plain,(
% 0.03/0.35 ~sQ8_spl|~sQ9_spl|~sQ10_spl|sQ12_spl|~sQ11_spl|~sQ3_spl),
% 0.03/0.35 inference(split_clause,[status(thm)],[f1104,f568,f572,f576,f584,f580,f548])).
% 0.03/0.35 fof(f1108,plain,(
% 0.03/0.35 $false),
% 0.03/0.35 inference(sat_refutation,[status(thm)],[f551,f571,f575,f579,f583,f587,f591,f595,f599,f603,f608,f609,f610,f611,f612,f625,f626,f627,f628,f629,f630,f631,f632,f633,f634,f635,f636,f637,f638,f639,f729,f731,f739,f742,f902,f909,f916,f923,f1106])).
% 0.03/0.35 % SZS output end CNFRefutation for theBenchmark.p
% 0.09/0.36 % Elapsed time: 0.062172 seconds
% 0.09/0.36 % CPU time: 0.226926 seconds
% 0.09/0.36 % Total memory used: 113.698 MB
% 0.09/0.36 % Net memory used: 113.320 MB
%------------------------------------------------------------------------------