%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWC022+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.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:39:37 PM UTC 2026
% Result : Theorem 3.53s 1.08s
% Output : CNFRefutation 1.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 62
% Syntax : Number of formulae : 258 ( 19 unt; 41 def)
% Number of atoms : 991 ( 160 equ)
% Maximal formula atoms : 19 ( 3 avg)
% Number of connectives : 1277 ( 544 ~; 539 |; 100 &)
% ( 50 <=>; 44 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 50 ( 48 usr; 40 prp; 0-4 aty)
% Number of functors : 15 ( 15 usr; 7 con; 0-4 aty)
% Number of variables : 308 ( 281 !; 27 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
? [U] :
( ? [V] :
( U != V
& ssItem(V) )
& ssItem(U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [U] :
( ssList(U)
=> ( singletonP(U)
<=> ? [V] :
( cons(V,nil) = U
& ssItem(V) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( neq(U,V)
<=> U != V ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> ssList(cons(V,U)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
ssList(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> cons(V,U) != U ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssItem(W)
=> ! [X] :
( ssItem(X)
=> ( cons(W,U) = cons(X,V)
=> ( V = U
& W = X ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [U] :
( ssList(U)
=> ( nil != U
=> ssItem(hd(U)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssItem(V)
=> hd(cons(V,U)) = V ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
! [U] :
( ssList(U)
=> ( nil != U
=> ssList(tl(U)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ( ( frontsegP(V,W)
& frontsegP(U,V) )
=> frontsegP(U,W) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ( ( frontsegP(V,U)
& frontsegP(U,V) )
=> U = V ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,axiom,
! [U] :
( ssList(U)
=> frontsegP(U,U) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [U] :
( ssItem(U)
=> ! [V] :
( ssItem(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( frontsegP(cons(U,W),cons(V,X))
<=> ( frontsegP(W,X)
& U = V ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,axiom,
! [U] :
( ssList(U)
=> frontsegP(U,nil) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,axiom,
! [U] :
( ssList(U)
=> ( frontsegP(nil,U)
<=> nil = U ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f66,axiom,
totalorderedP(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f69,axiom,
strictorderedP(nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f75,axiom,
! [U] :
( ssList(U)
=> ( nil != U
=> ? [V] :
( hd(U) = V
& ssItem(V) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f78,axiom,
! [U] :
( ssList(U)
=> ( nil != U
=> cons(hd(U),tl(U)) = U ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f96,conjecture,
! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ( ( neq(X,nil)
| ~ neq(V,nil) )
& ( ? [Z] :
( ? [X1] :
( neq(nil,X)
& hd(X) = X1
& cons(X1,nil) = Z
& ssItem(X1) )
& W != Z
& ssList(Z) )
| ? [Y] :
( frontsegP(U,Y)
& frontsegP(V,Y)
& neq(Y,nil)
& ssList(Y) )
| ~ neq(V,nil) ) )
| U != W
| V != X ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f97,negated_conjecture,
~ ! [U] :
( ssList(U)
=> ! [V] :
( ssList(V)
=> ! [W] :
( ssList(W)
=> ! [X] :
( ssList(X)
=> ( ( ( neq(X,nil)
| ~ neq(V,nil) )
& ( ? [Z] :
( ? [X1] :
( neq(nil,X)
& hd(X) = X1
& cons(X1,nil) = Z
& ssItem(X1) )
& W != Z
& ssList(Z) )
| ? [Y] :
( frontsegP(U,Y)
& frontsegP(V,Y)
& neq(Y,nil)
& ssList(Y) )
| ~ neq(V,nil) ) )
| U != W
| V != X ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f96]) ).
fof(f102,plain,
( sK0_skl != sK1_skl
& ssItem(sK1_skl)
& ssItem(sK0_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(U,sK0_skl),skolemize(V,sK1_skl)],[f2]) ).
fof(f104,plain,
ssItem(sK1_skl),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f113,plain,
! [U] :
( ( singletonP(U)
<=> ? [V] :
( cons(V,nil) = U
& ssItem(V) ) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f114,plain,
! [U] :
( ( ( ! [V] :
( cons(V,nil) != U
| ~ ssItem(V) )
| singletonP(U) )
& ( ? [V] :
( cons(V,nil) = U
& ssItem(V) )
| ~ singletonP(U) ) )
| ~ ssList(U) ),
inference(NNF_transformation,[status(thm)],[f113]) ).
fof(f115,plain,
! [U] :
( ( ( ! [V] :
( cons(V,nil) != U
| ~ ssItem(V) )
| singletonP(U) )
& ( ( cons(sK4_skl(U),nil) = U
& ssItem(sK4_skl(U)) )
| ~ singletonP(U) ) )
| ~ ssList(U) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(V,sK4_skl(U))],[f114]) ).
fof(f117,plain,
! [X0] :
( cons(sK4_skl(X0),nil) = X0
| ~ singletonP(X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f118,plain,
! [X0,X1] :
( cons(X1,nil) != X0
| ~ ssItem(X1)
| singletonP(X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f115]) ).
fof(f217,plain,
! [U] :
( ! [V] :
( ( neq(U,V)
<=> U != V )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f15]) ).
fof(f218,plain,
! [U] :
( ! [V] :
( ( ( U = V
| neq(U,V) )
& ( U != V
| ~ neq(U,V) ) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(NNF_transformation,[status(thm)],[f217]) ).
fof(f219,plain,
! [X0,X1] :
( X0 != X1
| ~ neq(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f220,plain,
! [X0,X1] :
( X0 = X1
| neq(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f218]) ).
fof(f221,plain,
! [U] :
( ! [V] :
( ssList(cons(V,U))
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f222,plain,
! [X0,X1] :
( ssList(cons(X1,X0))
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f221]) ).
fof(f223,plain,
ssList(nil),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f224,plain,
! [U] :
( ! [V] :
( cons(V,U) != U
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f18]) ).
fof(f225,plain,
! [X0,X1] :
( cons(X1,X0) != X0
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f224]) ).
fof(f226,plain,
! [U] :
( ! [V] :
( ! [W] :
( ! [X] :
( ( V = U
& W = X )
| cons(W,U) != cons(X,V)
| ~ ssItem(X) )
| ~ ssItem(W) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f19]) ).
fof(f227,plain,
! [X0,X1,X2,X3] :
( X2 = X3
| cons(X2,X0) != cons(X3,X1)
| ~ ssItem(X3)
| ~ ssItem(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f226]) ).
fof(f228,plain,
! [X0,X1,X2,X3] :
( X1 = X0
| cons(X2,X0) != cons(X3,X1)
| ~ ssItem(X3)
| ~ ssItem(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f226]) ).
fof(f236,plain,
! [U] :
( ssItem(hd(U))
| nil = U
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f22]) ).
fof(f237,plain,
! [X0] :
( ssItem(hd(X0))
| nil = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f236]) ).
fof(f238,plain,
! [U] :
( ! [V] :
( hd(cons(V,U)) = V
| ~ ssItem(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f23]) ).
fof(f239,plain,
! [X0,X1] :
( hd(cons(X1,X0)) = X1
| ~ ssItem(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f238]) ).
fof(f240,plain,
! [U] :
( ssList(tl(U))
| nil = U
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f24]) ).
fof(f241,plain,
! [X0] :
( ssList(tl(X0))
| nil = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f240]) ).
fof(f281,plain,
! [U] :
( ! [V] :
( ! [W] :
( frontsegP(U,W)
| ~ frontsegP(V,W)
| ~ frontsegP(U,V)
| ~ ssList(W) )
| ~ ssList(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f282,plain,
! [X0,X1,X2] :
( frontsegP(X0,X2)
| ~ frontsegP(X1,X2)
| ~ frontsegP(X0,X1)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f281]) ).
fof(f283,plain,
! [U] :
( ! [V] :
( U = V
| ~ frontsegP(V,U)
| ~ frontsegP(U,V)
| ~ ssList(V) )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f284,plain,
! [X0,X1] :
( X0 = X1
| ~ frontsegP(X1,X0)
| ~ frontsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f283]) ).
fof(f285,plain,
! [U] :
( frontsegP(U,U)
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f42]) ).
fof(f286,plain,
! [X0] :
( frontsegP(X0,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f285]) ).
fof(f289,plain,
! [U] :
( ! [V] :
( ! [W] :
( ! [X] :
( ( frontsegP(cons(U,W),cons(V,X))
<=> ( frontsegP(W,X)
& U = V ) )
| ~ ssList(X) )
| ~ ssList(W) )
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(pre_NNF_transformation,[status(thm)],[f44]) ).
fof(f290,plain,
! [U] :
( ! [V] :
( ! [W] :
( ! [X] :
( ( ( ~ frontsegP(W,X)
| U != V
| frontsegP(cons(U,W),cons(V,X)) )
& ( ( frontsegP(W,X)
& U = V )
| ~ frontsegP(cons(U,W),cons(V,X)) ) )
| ~ ssList(X) )
| ~ ssList(W) )
| ~ ssItem(V) )
| ~ ssItem(U) ),
inference(NNF_transformation,[status(thm)],[f289]) ).
fof(f291,plain,
! [X0,X1,X2,X3] :
( X0 = X1
| ~ frontsegP(cons(X0,X2),cons(X1,X3))
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f290]) ).
fof(f292,plain,
! [X0,X1,X2,X3] :
( frontsegP(X2,X3)
| ~ frontsegP(cons(X0,X2),cons(X1,X3))
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f290]) ).
fof(f293,plain,
! [X0,X1,X2,X3] :
( ~ frontsegP(X2,X3)
| X0 != X1
| frontsegP(cons(X0,X2),cons(X1,X3))
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X0) ),
inference(cnf_transformation,[status(thm)],[f290]) ).
fof(f294,plain,
! [U] :
( frontsegP(U,nil)
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f45]) ).
fof(f295,plain,
! [X0] :
( frontsegP(X0,nil)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f294]) ).
fof(f296,plain,
! [U] :
( ( frontsegP(nil,U)
<=> nil = U )
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f297,plain,
! [U] :
( ( ( nil != U
| frontsegP(nil,U) )
& ( nil = U
| ~ frontsegP(nil,U) ) )
| ~ ssList(U) ),
inference(NNF_transformation,[status(thm)],[f296]) ).
fof(f298,plain,
! [X0] :
( nil = X0
| ~ frontsegP(nil,X0)
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f297]) ).
fof(f339,plain,
totalorderedP(nil),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f349,plain,
strictorderedP(nil),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f363,plain,
! [U] :
( ? [V] :
( hd(U) = V
& ssItem(V) )
| nil = U
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f75]) ).
fof(f364,plain,
! [U] :
( ( hd(U) = sK45_skl(U)
& ssItem(sK45_skl(U)) )
| nil = U
| ~ ssList(U) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK45_skl]),skolemize(V,sK45_skl(U))],[f363]) ).
fof(f366,plain,
! [X0] :
( hd(X0) = sK45_skl(X0)
| nil = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f364]) ).
fof(f373,plain,
! [U] :
( cons(hd(U),tl(U)) = U
| nil = U
| ~ ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f78]) ).
fof(f374,plain,
! [X0] :
( cons(hd(X0),tl(X0)) = X0
| nil = X0
| ~ ssList(X0) ),
inference(cnf_transformation,[status(thm)],[f373]) ).
fof(f415,plain,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ( ( ~ neq(X,nil)
& neq(V,nil) )
| ( ! [Z] :
( ! [X1] :
( ~ neq(nil,X)
| hd(X) != X1
| cons(X1,nil) != Z
| ~ ssItem(X1) )
| W = Z
| ~ ssList(Z) )
& ! [Y] :
( ~ frontsegP(U,Y)
| ~ frontsegP(V,Y)
| ~ neq(Y,nil)
| ~ ssList(Y) )
& neq(V,nil) ) )
& U = W
& V = X
& ssList(X) )
& ssList(W) )
& ssList(V) )
& ssList(U) ),
inference(pre_NNF_transformation,[status(thm)],[f97]) ).
fof(f416,definition,
! [U,V,W,X] :
( sP0_prd(X,W,V,U)
<=> ( ! [Z] :
( ! [X1] :
( ~ neq(nil,X)
| hd(X) != X1
| cons(X1,nil) != Z
| ~ ssItem(X1) )
| W = Z
| ~ ssList(Z) )
& ! [Y] :
( ~ frontsegP(U,Y)
| ~ frontsegP(V,Y)
| ~ neq(Y,nil)
| ~ ssList(Y) )
& neq(V,nil) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f417,plain,
? [U] :
( ? [V] :
( ? [W] :
( ? [X] :
( ( ( ~ neq(X,nil)
& neq(V,nil) )
| sP0_prd(X,W,V,U) )
& U = W
& V = X
& ssList(X) )
& ssList(W) )
& ssList(V) )
& ssList(U) ),
inference(formula_renaming,[status(thm)],[f415,f416]) ).
fof(f418,plain,
( ( ( ~ neq(sK50_skl,nil)
& neq(sK48_skl,nil) )
| sP0_prd(sK50_skl,sK49_skl,sK48_skl,sK47_skl) )
& sK47_skl = sK49_skl
& sK48_skl = sK50_skl
& ssList(sK50_skl)
& ssList(sK49_skl)
& ssList(sK48_skl)
& ssList(sK47_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl,sK48_skl,sK49_skl,sK50_skl]),skolemize(U,sK47_skl),skolemize(V,sK48_skl),skolemize(W,sK49_skl),skolemize(X,sK50_skl)],[f417]) ).
fof(f421,plain,
ssList(sK49_skl),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f422,plain,
ssList(sK50_skl),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f423,plain,
sK48_skl = sK50_skl,
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f424,plain,
sK47_skl = sK49_skl,
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f425,plain,
( neq(sK48_skl,nil)
| sP0_prd(sK50_skl,sK49_skl,sK48_skl,sK47_skl) ),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f426,plain,
( ~ neq(sK50_skl,nil)
| sP0_prd(sK50_skl,sK49_skl,sK48_skl,sK47_skl) ),
inference(cnf_transformation,[status(thm)],[f418]) ).
fof(f427,definition,
! [U,V,Y] :
( sP1_prd(Y,V,U)
<=> ( ~ frontsegP(U,Y)
| ~ frontsegP(V,Y)
| ~ neq(Y,nil)
| ~ ssList(Y) ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f428,plain,
! [U,V,W,X] :
( sP0_prd(X,W,V,U)
<=> ( ! [Z] :
( ! [X1] :
( ~ neq(nil,X)
| hd(X) != X1
| cons(X1,nil) != Z
| ~ ssItem(X1) )
| W = Z
| ~ ssList(Z) )
& ! [Y] : sP1_prd(Y,V,U)
& neq(V,nil) ) ),
inference(formula_renaming,[status(thm)],[f416,f427]) ).
fof(f429,plain,
! [U,V,W,X] :
( ( ? [Z] :
( ? [X1] :
( neq(nil,X)
& hd(X) = X1
& cons(X1,nil) = Z
& ssItem(X1) )
& W != Z
& ssList(Z) )
| ? [Y] : ~ sP1_prd(Y,V,U)
| ~ neq(V,nil)
| sP0_prd(X,W,V,U) )
& ( ( ! [Z] :
( ! [X1] :
( ~ neq(nil,X)
| hd(X) != X1
| cons(X1,nil) != Z
| ~ ssItem(X1) )
| W = Z
| ~ ssList(Z) )
& ! [Y] : sP1_prd(Y,V,U)
& neq(V,nil) )
| ~ sP0_prd(X,W,V,U) ) ),
inference(NNF_transformation,[status(thm)],[f428]) ).
fof(f430,plain,
( ! [U,V,W,X] :
( ? [Z] :
( neq(nil,X)
& ? [X1] :
( hd(X) = X1
& cons(X1,nil) = Z
& ssItem(X1) )
& W != Z
& ssList(Z) )
| ? [Y] : ~ sP1_prd(Y,V,U)
| ~ neq(V,nil)
| sP0_prd(X,W,V,U) )
& ! [U,V,W,X] :
( ( ! [Z] :
( ~ neq(nil,X)
| ! [X1] :
( hd(X) != X1
| cons(X1,nil) != Z
| ~ ssItem(X1) )
| W = Z
| ~ ssList(Z) )
& ! [Y] : sP1_prd(Y,V,U)
& neq(V,nil) )
| ~ sP0_prd(X,W,V,U) ) ),
inference(miniscoping,[status(thm)],[f429]) ).
fof(f431,plain,
( ! [U,V,W,X] :
( ( neq(nil,X)
& hd(X) = sK53_skl(X,W,V,U)
& cons(sK53_skl(X,W,V,U),nil) = sK52_skl(X,W,V,U)
& ssItem(sK53_skl(X,W,V,U))
& W != sK52_skl(X,W,V,U)
& ssList(sK52_skl(X,W,V,U)) )
| ~ sP1_prd(sK51_skl(X,W,V,U),V,U)
| ~ neq(V,nil)
| sP0_prd(X,W,V,U) )
& ! [U,V,W,X] :
( ( ! [Z] :
( ~ neq(nil,X)
| ! [X1] :
( hd(X) != X1
| cons(X1,nil) != Z
| ~ ssItem(X1) )
| W = Z
| ~ ssList(Z) )
& ! [Y] : sP1_prd(Y,V,U)
& neq(V,nil) )
| ~ sP0_prd(X,W,V,U) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK51_skl,sK52_skl,sK53_skl]),skolemize(Y,sK51_skl(X,W,V,U)),skolemize(Z,sK52_skl(X,W,V,U)),skolemize(X1,sK53_skl(X,W,V,U))],[f430]) ).
fof(f432,plain,
! [X0,X1,X2,X3] :
( neq(X2,nil)
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f431]) ).
fof(f433,plain,
! [X0,X1,X2,X3,X4] :
( sP1_prd(X4,X2,X3)
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f431]) ).
fof(f434,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ neq(nil,X0)
| hd(X0) != X5
| cons(X5,nil) != X4
| ~ ssItem(X5)
| X1 = X4
| ~ ssList(X4)
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f431]) ).
fof(f441,plain,
! [U,V,Y] :
( ( ( frontsegP(U,Y)
& frontsegP(V,Y)
& neq(Y,nil)
& ssList(Y) )
| sP1_prd(Y,V,U) )
& ( ~ frontsegP(U,Y)
| ~ frontsegP(V,Y)
| ~ neq(Y,nil)
| ~ ssList(Y)
| ~ sP1_prd(Y,V,U) ) ),
inference(NNF_transformation,[status(thm)],[f427]) ).
fof(f442,plain,
( ! [U,V,Y] :
( ( frontsegP(U,Y)
& frontsegP(V,Y)
& neq(Y,nil)
& ssList(Y) )
| sP1_prd(Y,V,U) )
& ! [U,V,Y] :
( ~ frontsegP(U,Y)
| ~ frontsegP(V,Y)
| ~ neq(Y,nil)
| ~ ssList(Y)
| ~ sP1_prd(Y,V,U) ) ),
inference(miniscoping,[status(thm)],[f441]) ).
fof(f443,plain,
! [X0,X1,X2] :
( ~ frontsegP(X2,X0)
| ~ frontsegP(X1,X0)
| ~ neq(X0,nil)
| ~ ssList(X0)
| ~ sP1_prd(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f442]) ).
fof(f448,definition,
( sQ0_spl
<=> sP0_prd(sK50_skl,sK49_skl,sK48_skl,sK47_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f449,plain,
( ~ sQ0_spl
| sP0_prd(sK50_skl,sK49_skl,sK48_skl,sK47_skl) ),
inference(component_clause,[status(thm)],[f448]) ).
fof(f451,definition,
( sQ1_spl
<=> neq(sK48_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f452,plain,
( ~ sQ1_spl
| neq(sK48_skl,nil) ),
inference(component_clause,[status(thm)],[f451]) ).
fof(f454,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f425,f448,f451]) ).
fof(f455,definition,
( sQ2_spl
<=> neq(sK50_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f457,plain,
( sQ2_spl
| ~ neq(sK50_skl,nil) ),
inference(component_clause,[status(thm)],[f455]) ).
fof(f458,plain,
( ~ sQ2_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f426,f448,f455]) ).
fof(f462,plain,
! [X0] :
( ~ ssItem(X0)
| singletonP(cons(X0,nil))
| ~ ssList(cons(X0,nil)) ),
inference(destructive_equality_resolution,[status(thm)],[f118]) ).
fof(f474,plain,
! [X1] :
( ~ neq(X1,X1)
| ~ ssList(X1)
| ~ ssList(X1) ),
inference(destructive_equality_resolution,[status(thm)],[f219]) ).
fof(f475,plain,
! [X0] :
( ~ neq(X0,X0)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f474]) ).
fof(f478,plain,
! [X1,X2,X3] :
( ~ frontsegP(X2,X3)
| frontsegP(cons(X1,X2),cons(X1,X3))
| ~ ssList(X3)
| ~ ssList(X2)
| ~ ssItem(X1)
| ~ ssItem(X1) ),
inference(destructive_equality_resolution,[status(thm)],[f293]) ).
fof(f479,plain,
! [X0,X1,X2] :
( ~ frontsegP(X1,X2)
| frontsegP(cons(X0,X1),cons(X0,X2))
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f478]) ).
fof(f489,plain,
! [X0,X1,X2,X3] :
( ~ neq(nil,X0)
| ~ ssItem(hd(X0))
| X1 = cons(hd(X0),nil)
| ~ ssList(cons(hd(X0),nil))
| ~ sP0_prd(X0,X1,X2,X3) ),
inference(destructive_equality_resolution,[status(thm)],[f434]) ).
fof(f494,plain,
( ~ sQ0_spl
| sP0_prd(sK50_skl,sK49_skl,sK50_skl,sK47_skl) ),
inference(forward_demodulation,[status(thm)],[f423,f449]) ).
fof(f495,plain,
( ~ sQ0_spl
| sP0_prd(sK50_skl,sK49_skl,sK50_skl,sK49_skl) ),
inference(forward_demodulation,[status(thm)],[f424,f494]) ).
fof(f496,plain,
( ~ sQ0_spl
| neq(sK50_skl,nil) ),
inference(resolution,[status(thm)],[f432,f495]) ).
fof(f497,plain,
! [X0] :
( ~ sQ0_spl
| sP1_prd(X0,sK50_skl,sK49_skl) ),
inference(resolution,[status(thm)],[f433,f495]) ).
fof(f498,plain,
( ~ ssList(nil)
| nil = nil
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f298,f295]) ).
fof(f500,definition,
( sQ3_spl
<=> ssList(nil) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f502,plain,
( sQ3_spl
| ~ ssList(nil) ),
inference(component_clause,[status(thm)],[f500]) ).
fof(f503,definition,
( sQ4_spl
<=> nil = nil ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f506,plain,
( sQ4_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f498,f500,f503]) ).
fof(f508,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f502,f223]) ).
fof(f509,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f508]) ).
fof(f512,plain,
! [X0,X1,X2,X3] :
( ~ neq(nil,X0)
| ~ ssItem(hd(X0))
| X1 = cons(hd(X0),nil)
| ~ sP0_prd(X0,X1,X2,X3)
| ~ ssItem(hd(X0))
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f222,f489]) ).
fof(f513,definition,
! [X0,X1,X2,X3] :
( sQ5_spl
<=> ( ~ neq(nil,X0)
| ~ ssItem(hd(X0))
| X1 = cons(hd(X0),nil)
| ~ sP0_prd(X0,X1,X2,X3)
| ~ ssItem(hd(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f514,plain,
! [X0,X1,X2,X3] :
( ~ sQ5_spl
| ~ neq(nil,X0)
| ~ ssItem(hd(X0))
| X1 = cons(hd(X0),nil)
| ~ sP0_prd(X0,X1,X2,X3)
| ~ ssItem(hd(X0)) ),
inference(component_clause,[status(thm)],[f513]) ).
fof(f516,plain,
( sQ5_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f512,f500,f513]) ).
fof(f517,plain,
! [X0,X1,X2,X3] :
( ~ sQ5_spl
| ~ neq(nil,X0)
| X1 = cons(hd(X0),nil)
| ~ sP0_prd(X0,X1,X2,X3)
| ~ ssItem(hd(X0)) ),
inference(duplicate_literals_removal,[status(thm)],[f514]) ).
fof(f519,plain,
! [X0] :
( ~ ssList(X0)
| nil = X0
| ~ frontsegP(nil,X0)
| ~ ssList(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f284,f295]) ).
fof(f522,definition,
! [X0] :
( sQ6_spl
<=> ( ~ ssList(X0)
| nil = X0
| ~ frontsegP(nil,X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f525,plain,
( sQ6_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f519,f500,f522]) ).
fof(f529,plain,
! [X0,X1] :
( X1 = X1
| ~ ssItem(X1)
| ~ ssItem(X1)
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(equality_resolution,[status(thm)],[f227]) ).
fof(f530,definition,
! [X0] :
( sQ7_spl
<=> ( ~ ssList(X0)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f531,plain,
! [X0] :
( ~ sQ7_spl
| ~ ssList(X0)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f530]) ).
fof(f533,definition,
! [X1] :
( sQ8_spl
<=> ( X1 = X1
| ~ ssItem(X1)
| ~ ssItem(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f536,plain,
( sQ8_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f529,f530,f533]) ).
fof(f537,plain,
! [X0] :
( ~ sQ7_spl
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f531]) ).
fof(f547,plain,
( ~ sQ7_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f223,f537]) ).
fof(f550,plain,
~ sQ7_spl,
inference(contradiction_clause,[status(thm)],[f547]) ).
fof(f552,plain,
! [X0] :
( ~ sQ0_spl
| ~ frontsegP(sK49_skl,X0)
| ~ frontsegP(sK50_skl,X0)
| ~ neq(X0,nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f443,f497]) ).
fof(f559,definition,
( sQ11_spl
<=> ssList(sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f561,plain,
( sQ11_spl
| ~ ssList(sK50_skl) ),
inference(component_clause,[status(thm)],[f559]) ).
fof(f562,definition,
( sQ12_spl
<=> frontsegP(sK50_skl,sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f563,plain,
( ~ sQ12_spl
| frontsegP(sK50_skl,sK50_skl) ),
inference(component_clause,[status(thm)],[f562]) ).
fof(f564,plain,
( sQ12_spl
| ~ frontsegP(sK50_skl,sK50_skl) ),
inference(component_clause,[status(thm)],[f562]) ).
fof(f576,plain,
( ~ sQ1_spl
| neq(sK50_skl,nil) ),
inference(forward_demodulation,[status(thm)],[f423,f452]) ).
fof(f577,plain,
( sQ2_spl
| ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f457,f576]) ).
fof(f578,plain,
( sQ2_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f577]) ).
fof(f588,definition,
( sQ17_spl
<=> sK50_skl = nil ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f589,plain,
( ~ sQ17_spl
| sK50_skl = nil ),
inference(component_clause,[status(thm)],[f588]) ).
fof(f613,plain,
( ~ sQ0_spl
| ~ sQ17_spl
| neq(sK50_skl,sK50_skl) ),
inference(forward_demodulation,[status(thm)],[f589,f496]) ).
fof(f614,plain,
( ~ sQ0_spl
| ~ sQ17_spl
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f613,f475]) ).
fof(f616,plain,
( ~ sQ0_spl
| ~ sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f614,f422]) ).
fof(f617,plain,
( ~ sQ0_spl
| ~ sQ17_spl ),
inference(contradiction_clause,[status(thm)],[f616]) ).
fof(f622,plain,
! [X0,X1] :
( frontsegP(X1,nil)
| ~ frontsegP(X1,X0)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f295,f282]) ).
fof(f623,definition,
! [X0,X1] :
( sQ18_spl
<=> ( frontsegP(X1,nil)
| ~ frontsegP(X1,X0)
| ~ ssList(X0)
| ~ ssList(X1)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f626,plain,
( ~ sQ3_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f622,f623,f500]) ).
fof(f634,plain,
! [X0] :
( ~ ssItem(X0)
| singletonP(cons(X0,nil))
| ~ ssItem(X0)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f222,f462]) ).
fof(f635,definition,
! [X0] :
( sQ19_spl
<=> ( ~ ssItem(X0)
| singletonP(cons(X0,nil))
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f638,plain,
( sQ19_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f634,f500,f635]) ).
fof(f642,plain,
! [X0,X1,X2] :
( frontsegP(X1,X2)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssItem(X0)
| ~ frontsegP(X1,X2)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f479,f292]) ).
fof(f643,plain,
! [X0,X1,X2] :
( X0 = X0
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssItem(X0)
| ~ ssItem(X0)
| ~ frontsegP(X1,X2)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ ssItem(X0) ),
inference(resolution,[status(thm)],[f479,f291]) ).
fof(f645,definition,
! [X0] :
( sQ20_spl
<=> ( ~ ssItem(X0)
| ~ ssItem(X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f646,plain,
! [X0] :
( ~ sQ20_spl
| ~ ssItem(X0)
| ~ ssItem(X0)
| ~ ssItem(X0) ),
inference(component_clause,[status(thm)],[f645]) ).
fof(f648,definition,
! [X1,X2] :
( sQ21_spl
<=> ( frontsegP(X1,X2)
| ~ ssList(X2)
| ~ ssList(X1)
| ~ frontsegP(X1,X2)
| ~ ssList(X2)
| ~ ssList(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f651,plain,
( sQ21_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f642,f645,f648]) ).
fof(f652,definition,
! [X0] :
( sQ22_spl
<=> ( X0 = X0
| ~ ssItem(X0)
| ~ ssItem(X0)
| ~ ssItem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f655,definition,
! [X1,X2] :
( sQ23_spl
<=> ( ~ ssList(X2)
| ~ ssList(X1)
| ~ frontsegP(X1,X2)
| ~ ssList(X2)
| ~ ssList(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f656,plain,
! [X0,X1] :
( ~ sQ23_spl
| ~ ssList(X1)
| ~ ssList(X0)
| ~ frontsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f655]) ).
fof(f658,plain,
( sQ23_spl
| sQ22_spl ),
inference(split_clause,[status(thm)],[f643,f652,f655]) ).
fof(f660,plain,
! [X0] :
( ~ sQ20_spl
| ~ ssItem(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f646]) ).
fof(f661,plain,
! [X0,X1] :
( ~ sQ23_spl
| ~ frontsegP(X0,X1)
| ~ ssList(X1)
| ~ ssList(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f656]) ).
fof(f664,plain,
( ~ sQ20_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f104,f660]) ).
fof(f666,plain,
~ sQ20_spl,
inference(contradiction_clause,[status(thm)],[f664]) ).
fof(f674,definition,
( sQ25_spl
<=> ssList(sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f676,plain,
( sQ25_spl
| ~ ssList(sK49_skl) ),
inference(component_clause,[status(thm)],[f674]) ).
fof(f678,definition,
( sQ26_spl
<=> frontsegP(sK50_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f684,definition,
( sQ28_spl
<=> sK49_skl = nil ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f688,plain,
( sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f676,f421]) ).
fof(f689,plain,
sQ25_spl,
inference(contradiction_clause,[status(thm)],[f688]) ).
fof(f728,plain,
! [X0] :
( ~ sQ23_spl
| ~ ssList(X0)
| ~ ssList(nil)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f661,f295]) ).
fof(f730,plain,
( ~ sQ23_spl
| ~ sQ3_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f728,f530,f500,f655]) ).
fof(f742,plain,
( ~ sQ0_spl
| ~ sQ5_spl
| ~ neq(nil,sK50_skl)
| sK49_skl = cons(hd(sK50_skl),nil)
| ~ ssItem(hd(sK50_skl)) ),
inference(resolution,[status(thm)],[f517,f495]) ).
fof(f743,definition,
( sQ31_spl
<=> ssItem(hd(sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f745,plain,
( sQ31_spl
| ~ ssItem(hd(sK50_skl)) ),
inference(component_clause,[status(thm)],[f743]) ).
fof(f746,definition,
( sQ32_spl
<=> sK49_skl = cons(hd(sK50_skl),nil) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f747,plain,
( ~ sQ32_spl
| sK49_skl = cons(hd(sK50_skl),nil) ),
inference(component_clause,[status(thm)],[f746]) ).
fof(f749,definition,
( sQ33_spl
<=> neq(nil,sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f751,plain,
( sQ33_spl
| ~ neq(nil,sK50_skl) ),
inference(component_clause,[status(thm)],[f749]) ).
fof(f752,plain,
( ~ sQ0_spl
| ~ sQ5_spl
| ~ sQ33_spl
| sQ32_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f742,f743,f746,f749,f513,f448]) ).
fof(f775,definition,
( sQ39_spl
<=> totalorderedP(nil) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f777,plain,
( sQ39_spl
| ~ totalorderedP(nil) ),
inference(component_clause,[status(thm)],[f775]) ).
fof(f779,plain,
( sQ39_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f777,f339]) ).
fof(f780,plain,
sQ39_spl,
inference(contradiction_clause,[status(thm)],[f779]) ).
fof(f783,plain,
( sQ31_spl
| nil = sK50_skl
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f237,f745]) ).
fof(f784,plain,
( sQ31_spl
| sQ17_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f783,f559,f588,f743]) ).
fof(f785,plain,
( sQ11_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f561,f422]) ).
fof(f786,plain,
sQ11_spl,
inference(contradiction_clause,[status(thm)],[f785]) ).
fof(f787,plain,
( sQ12_spl
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f564,f286]) ).
fof(f788,plain,
( sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f787,f559,f562]) ).
fof(f810,plain,
( ~ sQ32_spl
| sK49_skl != nil
| ~ ssItem(hd(sK50_skl))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f747,f225]) ).
fof(f839,plain,
( ~ sQ32_spl
| ~ sQ28_spl
| ~ sQ31_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f810,f500,f743,f684,f746]) ).
fof(f857,definition,
( sQ51_spl
<=> strictorderedP(nil) ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f859,plain,
( sQ51_spl
| ~ strictorderedP(nil) ),
inference(component_clause,[status(thm)],[f857]) ).
fof(f861,plain,
( sQ51_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f859,f349]) ).
fof(f862,plain,
sQ51_spl,
inference(contradiction_clause,[status(thm)],[f861]) ).
fof(f905,plain,
( sQ33_spl
| nil = sK50_skl
| ~ ssList(sK50_skl)
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f220,f751]) ).
fof(f910,plain,
( sQ33_spl
| sQ17_spl
| ~ sQ11_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f905,f500,f559,f588,f749]) ).
fof(f989,definition,
! [X0] :
( sQ60_spl
<=> neq(nil,X0) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f990,plain,
! [X0] :
( ~ sQ60_spl
| neq(nil,X0) ),
inference(component_clause,[status(thm)],[f989]) ).
fof(f999,plain,
( ~ sQ60_spl
| ~ ssList(nil) ),
inference(resolution,[status(thm)],[f990,f475]) ).
fof(f1000,plain,
( ~ sQ60_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f999,f500,f989]) ).
fof(f1139,plain,
( ~ sQ32_spl
| hd(sK49_skl) = hd(sK50_skl)
| ~ ssItem(hd(sK50_skl))
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f747,f239]) ).
fof(f1140,definition,
( sQ70_spl
<=> hd(sK49_skl) = hd(sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f1141,plain,
( ~ sQ70_spl
| hd(sK49_skl) = hd(sK50_skl) ),
inference(component_clause,[status(thm)],[f1140]) ).
fof(f1143,plain,
( ~ sQ32_spl
| sQ70_spl
| ~ sQ31_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f1139,f500,f743,f1140,f746]) ).
fof(f1148,plain,
( ~ sQ12_spl
| sK50_skl = sK50_skl
| ~ frontsegP(sK50_skl,sK50_skl)
| ~ ssList(sK50_skl)
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f284,f563]) ).
fof(f1153,definition,
( sQ71_spl
<=> sK50_skl = sK50_skl ),
introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition]) ).
fof(f1156,plain,
( sQ71_spl
| ~ sQ12_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f1148,f559,f562,f1153]) ).
fof(f1160,plain,
! [X0] :
( ~ sQ32_spl
| ~ frontsegP(X0,nil)
| frontsegP(cons(hd(sK50_skl),X0),sK49_skl)
| ~ ssList(nil)
| ~ ssList(X0)
| ~ ssItem(hd(sK50_skl)) ),
inference(paramodulation,[status(thm)],[f747,f479]) ).
fof(f1166,definition,
! [X0] :
( sQ73_spl
<=> ( ~ frontsegP(X0,nil)
| frontsegP(cons(hd(sK50_skl),X0),sK49_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f1167,plain,
! [X0] :
( ~ sQ73_spl
| ~ frontsegP(X0,nil)
| frontsegP(cons(hd(sK50_skl),X0),sK49_skl)
| ~ ssList(X0) ),
inference(component_clause,[status(thm)],[f1166]) ).
fof(f1169,plain,
( ~ sQ32_spl
| ~ sQ3_spl
| sQ73_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f1160,f743,f1166,f500,f746]) ).
fof(f1170,plain,
! [X0] :
( ~ sQ73_spl
| frontsegP(cons(hd(sK50_skl),X0),sK49_skl)
| ~ ssList(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1167,f295]) ).
fof(f1188,plain,
( ~ sQ32_spl
| ~ sQ73_spl
| frontsegP(sK49_skl,sK49_skl)
| ~ ssList(nil) ),
inference(paramodulation,[status(thm)],[f747,f1170]) ).
fof(f1193,definition,
( sQ77_spl
<=> frontsegP(sK49_skl,sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f1196,plain,
( ~ sQ32_spl
| ~ sQ73_spl
| sQ77_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f1188,f500,f1193,f1166,f746]) ).
fof(f1243,plain,
! [X0] :
( ~ sQ12_spl
| frontsegP(X0,sK50_skl)
| ~ frontsegP(X0,sK50_skl)
| ~ ssList(sK50_skl)
| ~ ssList(sK50_skl)
| ~ ssList(X0) ),
inference(resolution,[status(thm)],[f282,f563]) ).
fof(f1261,definition,
! [X0] :
( sQ85_spl
<=> ( frontsegP(X0,sK50_skl)
| ~ frontsegP(X0,sK50_skl)
| ~ ssList(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f1264,plain,
( ~ sQ12_spl
| ~ sQ11_spl
| sQ85_spl ),
inference(split_clause,[status(thm)],[f1243,f1261,f559,f562]) ).
fof(f1509,definition,
( sQ110_spl
<=> neq(sK49_skl,nil) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f1510,plain,
( ~ sQ110_spl
| neq(sK49_skl,nil) ),
inference(component_clause,[status(thm)],[f1509]) ).
fof(f1511,plain,
( sQ110_spl
| ~ neq(sK49_skl,nil) ),
inference(component_clause,[status(thm)],[f1509]) ).
fof(f1563,plain,
( ~ sQ70_spl
| hd(sK50_skl) = sK45_skl(sK49_skl)
| nil = sK49_skl
| ~ ssList(sK49_skl) ),
inference(paramodulation,[status(thm)],[f1141,f366]) ).
fof(f1564,definition,
( sQ116_spl
<=> hd(sK50_skl) = sK45_skl(sK49_skl) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f1565,plain,
( ~ sQ116_spl
| hd(sK50_skl) = sK45_skl(sK49_skl) ),
inference(component_clause,[status(thm)],[f1564]) ).
fof(f1567,plain,
( ~ sQ70_spl
| sQ116_spl
| sQ28_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f1563,f674,f684,f1564,f1140]) ).
fof(f1576,plain,
! [X0] :
( ~ sQ73_spl
| ~ sQ116_spl
| frontsegP(cons(sK45_skl(sK49_skl),X0),sK49_skl)
| ~ ssList(X0) ),
inference(backward_demodulation,[status(thm)],[f1565,f1170]) ).
fof(f1580,plain,
( ~ sQ116_spl
| sK45_skl(sK49_skl) = sK45_skl(sK50_skl)
| nil = sK50_skl
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f1565,f366]) ).
fof(f1588,definition,
( sQ117_spl
<=> sK45_skl(sK49_skl) = sK45_skl(sK50_skl) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f1589,plain,
( ~ sQ117_spl
| sK45_skl(sK49_skl) = sK45_skl(sK50_skl) ),
inference(component_clause,[status(thm)],[f1588]) ).
fof(f1591,plain,
( ~ sQ116_spl
| sQ117_spl
| sQ17_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f1580,f559,f588,f1588,f1564]) ).
fof(f1642,plain,
( ~ sQ116_spl
| ~ sQ117_spl
| hd(sK50_skl) = sK45_skl(sK50_skl) ),
inference(backward_demodulation,[status(thm)],[f1589,f1565]) ).
fof(f1843,plain,
! [X0] :
( ~ sQ73_spl
| ~ sQ116_spl
| ~ sQ117_spl
| frontsegP(cons(sK45_skl(sK50_skl),X0),sK49_skl)
| ~ ssList(X0) ),
inference(forward_demodulation,[status(thm)],[f1589,f1576]) ).
fof(f1897,plain,
( sQ110_spl
| sK49_skl = nil
| ~ ssList(nil)
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f1511,f220]) ).
fof(f1899,plain,
( sQ110_spl
| sQ28_spl
| ~ sQ3_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f1897,f674,f500,f684,f1509]) ).
fof(f1904,plain,
( ~ sQ0_spl
| ~ sQ110_spl
| ~ frontsegP(sK49_skl,sK49_skl)
| ~ frontsegP(sK50_skl,sK49_skl)
| ~ ssList(sK49_skl) ),
inference(resolution,[status(thm)],[f1510,f552]) ).
fof(f1905,plain,
( ~ sQ0_spl
| ~ sQ110_spl
| ~ sQ77_spl
| ~ sQ26_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f1904,f674,f678,f1193,f1509,f448]) ).
fof(f2031,plain,
! [X0,X1] :
( X1 = nil
| ~ ssItem(X0)
| ~ ssItem(sK4_skl(cons(X0,X1)))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ singletonP(cons(X0,X1))
| ~ ssList(cons(X0,X1)) ),
inference(resolution,[status(thm)],[f117,f228]) ).
fof(f2032,plain,
! [X0,X1] :
( sK4_skl(cons(X0,X1)) = X0
| ~ ssItem(X0)
| ~ ssItem(sK4_skl(cons(X0,X1)))
| ~ ssList(X1)
| ~ ssList(nil)
| ~ singletonP(cons(X0,X1))
| ~ ssList(cons(X0,X1)) ),
inference(resolution,[status(thm)],[f117,f227]) ).
fof(f2045,definition,
! [X0,X1] :
( sQ174_spl
<=> ( X1 = nil
| ~ ssItem(X0)
| ~ ssItem(sK4_skl(cons(X0,X1)))
| ~ ssList(X1)
| ~ singletonP(cons(X0,X1))
| ~ ssList(cons(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition]) ).
fof(f2048,plain,
( ~ sQ3_spl
| sQ174_spl ),
inference(split_clause,[status(thm)],[f2031,f2045,f500]) ).
fof(f2049,definition,
! [X0,X1] :
( sQ175_spl
<=> ( sK4_skl(cons(X0,X1)) = X0
| ~ ssItem(X0)
| ~ ssItem(sK4_skl(cons(X0,X1)))
| ~ ssList(X1)
| ~ singletonP(cons(X0,X1))
| ~ ssList(cons(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ175_spl])],[split_symbol_definition]) ).
fof(f2052,plain,
( ~ sQ3_spl
| sQ175_spl ),
inference(split_clause,[status(thm)],[f2032,f2049,f500]) ).
fof(f2204,plain,
( ~ sQ116_spl
| ~ sQ117_spl
| cons(sK45_skl(sK50_skl),tl(sK50_skl)) = sK50_skl
| nil = sK50_skl
| ~ ssList(sK50_skl) ),
inference(paramodulation,[status(thm)],[f1642,f374]) ).
fof(f2216,definition,
( sQ194_spl
<=> cons(sK45_skl(sK50_skl),tl(sK50_skl)) = sK50_skl ),
introduced(definition,[new_symbols(definition,[sQ194_spl])],[split_symbol_definition]) ).
fof(f2217,plain,
( ~ sQ194_spl
| cons(sK45_skl(sK50_skl),tl(sK50_skl)) = sK50_skl ),
inference(component_clause,[status(thm)],[f2216]) ).
fof(f2219,plain,
( ~ sQ116_spl
| ~ sQ117_spl
| sQ194_spl
| sQ17_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f2204,f559,f588,f2216,f1588,f1564]) ).
fof(f2228,plain,
( ~ sQ194_spl
| ~ sQ73_spl
| ~ sQ116_spl
| ~ sQ117_spl
| frontsegP(sK50_skl,sK49_skl)
| ~ ssList(tl(sK50_skl)) ),
inference(paramodulation,[status(thm)],[f2217,f1843]) ).
fof(f2265,definition,
( sQ196_spl
<=> ssList(tl(sK50_skl)) ),
introduced(definition,[new_symbols(definition,[sQ196_spl])],[split_symbol_definition]) ).
fof(f2267,plain,
( sQ196_spl
| ~ ssList(tl(sK50_skl)) ),
inference(component_clause,[status(thm)],[f2265]) ).
fof(f2273,plain,
( ~ sQ194_spl
| ~ sQ73_spl
| ~ sQ116_spl
| ~ sQ117_spl
| sQ26_spl
| ~ sQ196_spl ),
inference(split_clause,[status(thm)],[f2228,f2265,f678,f1588,f1564,f1166,f2216]) ).
fof(f2394,plain,
( sQ196_spl
| nil = sK50_skl
| ~ ssList(sK50_skl) ),
inference(resolution,[status(thm)],[f2267,f241]) ).
fof(f2395,plain,
( sQ196_spl
| sQ17_spl
| ~ sQ11_spl ),
inference(split_clause,[status(thm)],[f2394,f559,f588,f2265]) ).
fof(f2396,plain,
$false,
inference(sat_refutation,[status(thm)],[f454,f458,f506,f509,f516,f525,f536,f550,f578,f617,f626,f638,f651,f658,f666,f689,f730,f752,f780,f784,f786,f788,f839,f862,f910,f1000,f1143,f1156,f1169,f1196,f1264,f1567,f1591,f1899,f1905,f2048,f2052,f2219,f2273,f2395]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWC022+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.46 % Computer : n008.cluster.edu
% 0.19/0.46 % Model : x86_64 x86_64
% 0.19/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.46 % Memory : 8046.5625MB
% 0.19/0.46 % OS : Linux 6.8.0-71-generic
% 0.19/0.46 % CPULimit : 300
% 0.19/0.46 % WCLimit : 300
% 0.19/0.46 % DateTime : Mon Sep 21 07:50:40 UTC 2026
% 0.19/0.47 % CPUTime :
% 0.19/0.49 % Drodi V4.1.1
% 3.53/1.08 % Refutation found
% 3.53/1.08 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.53/1.08 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.64/1.11 % Elapsed time: 0.626386 seconds
% 1.64/1.11 % CPU time: 4.353037 seconds
% 1.64/1.11 % Total memory used: 144.227 MB
% 1.64/1.11 % Net memory used: 140.989 MB
%------------------------------------------------------------------------------