%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX050+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n011.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 : Tue Sep 29 01:45:45 PM UTC 2026
% Result : Theorem 4.85s 1.44s
% Output : Refutation 6.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 25
% Syntax : Number of formulae : 193 ( 26 unt; 14 def)
% Number of atoms : 825 ( 263 equ)
% Maximal formula atoms : 13 ( 4 avg)
% Number of connectives : 1044 ( 412 ~; 530 |; 66 &)
% ( 15 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 18 ( 16 usr; 13 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 13 con; 0-3 aty)
% Number of variables : 290 ( 0 sgn 248 !; 42 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [X0,X1] : nil != cons(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id5) ).
fof(f8,axiom,
! [X0,X1,X2,X3] :
( cons(X0,X1) = cons(X2,X3)
=> X1 = X3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id8) ).
fof(f9,axiom,
! [X0,X1,X2,X3] :
( cons(X0,X1) = cons(X2,X3)
=> X0 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id9) ).
fof(f61,axiom,
! [X0,X1,X2] :
( delete_succeeds(X0,X1,X2)
<=> ( ? [X3,X4,X5] :
( X1 = cons(X3,X4)
& X2 = cons(X3,X5)
& delete_succeeds(X0,X4,X5) )
| X1 = cons(X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',id61) ).
fof(f256,axiom,
! [X0,X1,X2] :
( ( delete_succeeds(X0,X1,X2)
& list_succeeds(X1) )
=> list_succeeds(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom-(delete:types:1)') ).
fof(f273,axiom,
! [X0,X1,X2] :
( list_succeeds(X1)
=> ( occ(X0,X1) = X2
<=> occ_succeeds(X0,X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','occ/2') ).
fof(f283,axiom,
! [X0,X1,X2] :
( occ_succeeds(X0,X1,X2)
=> ( list_succeeds(X1)
& nat_succeeds(X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(occ:types)') ).
fof(f287,axiom,
! [X0,X1,X2] :
( ( list_succeeds(X2)
& X0 != X1 )
=> occ(X0,cons(X1,X2)) = occ(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(occ:cons:diff)') ).
fof(f288,axiom,
! [X0,X1] :
( list_succeeds(X1)
=> occ(X0,cons(X0,X1)) = s(occ(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(occ:cons:eq)') ).
fof(f291,axiom,
( ! [X0] :
( ( ? [X1,X2] :
( X0 = cons(X1,X2)
& list_succeeds(X2)
& ! [X3,X4,X5] :
( ( X3 != X4
& delete_succeeds(X3,X2,X5) )
=> occ(X4,X2) = occ(X4,X5) ) )
| X0 = nil )
=> ! [X3,X4,X5] :
( ( X3 != X4
& delete_succeeds(X3,X0,X5) )
=> occ(X4,X0) = occ(X4,X5) ) )
=> ! [X0] :
( list_succeeds(X0)
=> ! [X3,X4,X5] :
( ( X3 != X4
& delete_succeeds(X3,X0,X5) )
=> occ(X4,X0) = occ(X4,X5) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',induction) ).
fof(f292,conjecture,
! [X0,X1,X2,X3] :
( ( list_succeeds(X2)
& delete_succeeds(X0,X2,X3)
& X0 != X1 )
=> occ(X1,X2) = occ(X1,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','lemma-(delete:occ:diff)') ).
fof(f293,negated_conjecture,
~ ! [X0,X1,X2,X3] :
( ( list_succeeds(X2)
& delete_succeeds(X0,X2,X3)
& X0 != X1 )
=> occ(X1,X2) = occ(X1,X3) ),
inference(negated_conjecture,[status(cth)],[f292]) ).
fof(f318,plain,
( ! [X0] :
( ( ? [X1,X2] :
( X0 = cons(X1,X2)
& list_succeeds(X2)
& ! [X3,X4,X5] :
( ( X3 != X4
& delete_succeeds(X3,X2,X5) )
=> occ(X4,X2) = occ(X4,X5) ) )
| X0 = nil )
=> ! [X6,X7,X8] :
( ( X6 != X7
& delete_succeeds(X6,X0,X8) )
=> occ(X7,X8) = occ(X7,X0) ) )
=> ! [X9] :
( list_succeeds(X9)
=> ! [X10,X11,X12] :
( ( X10 != X11
& delete_succeeds(X10,X9,X12) )
=> occ(X11,X12) = occ(X11,X9) ) ) ),
inference(rectify,[],[f291]) ).
fof(f320,plain,
! [X0,X1,X2,X3] :
( X1 = X3
| cons(X0,X1) != cons(X2,X3) ),
inference(ennf_transformation,[],[f8]) ).
fof(f321,plain,
! [X0,X1,X2,X3] :
( X0 = X2
| cons(X0,X1) != cons(X2,X3) ),
inference(ennf_transformation,[],[f9]) ).
fof(f614,plain,
! [X0,X1,X2] :
( list_succeeds(X2)
| ~ delete_succeeds(X0,X1,X2)
| ~ list_succeeds(X1) ),
inference(ennf_transformation,[],[f256]) ).
fof(f615,plain,
! [X0,X1,X2] :
( list_succeeds(X2)
| ~ delete_succeeds(X0,X1,X2)
| ~ list_succeeds(X1) ),
inference(flattening,[],[f614]) ).
fof(f640,plain,
! [X0,X1,X2] :
( ( occ(X0,X1) = X2
<=> occ_succeeds(X0,X1,X2) )
| ~ list_succeeds(X1) ),
inference(ennf_transformation,[],[f273]) ).
fof(f656,plain,
! [X0,X1,X2] :
( ( list_succeeds(X1)
& nat_succeeds(X2) )
| ~ occ_succeeds(X0,X1,X2) ),
inference(ennf_transformation,[],[f283]) ).
fof(f660,plain,
! [X0,X1,X2] :
( occ(X0,cons(X1,X2)) = occ(X0,X2)
| ~ list_succeeds(X2)
| X0 = X1 ),
inference(ennf_transformation,[],[f287]) ).
fof(f661,plain,
! [X0,X1,X2] :
( occ(X0,cons(X1,X2)) = occ(X0,X2)
| ~ list_succeeds(X2)
| X0 = X1 ),
inference(flattening,[],[f660]) ).
fof(f662,plain,
! [X0,X1] :
( occ(X0,cons(X0,X1)) = s(occ(X0,X1))
| ~ list_succeeds(X1) ),
inference(ennf_transformation,[],[f288]) ).
fof(f666,plain,
( ! [X9] :
( ! [X10,X11,X12] :
( occ(X11,X12) = occ(X11,X9)
| X10 = X11
| ~ delete_succeeds(X10,X9,X12) )
| ~ list_succeeds(X9) )
| ? [X0] :
( ? [X6,X7,X8] :
( occ(X7,X8) != occ(X7,X0)
& X6 != X7
& delete_succeeds(X6,X0,X8) )
& ( ? [X1,X2] :
( X0 = cons(X1,X2)
& list_succeeds(X2)
& ! [X3,X4,X5] :
( occ(X4,X2) = occ(X4,X5)
| X3 = X4
| ~ delete_succeeds(X3,X2,X5) ) )
| X0 = nil ) ) ),
inference(ennf_transformation,[],[f318]) ).
fof(f667,plain,
( ! [X9] :
( ! [X10,X11,X12] :
( occ(X11,X12) = occ(X11,X9)
| X10 = X11
| ~ delete_succeeds(X10,X9,X12) )
| ~ list_succeeds(X9) )
| ? [X0] :
( ? [X6,X7,X8] :
( occ(X7,X8) != occ(X7,X0)
& X6 != X7
& delete_succeeds(X6,X0,X8) )
& ( ? [X1,X2] :
( X0 = cons(X1,X2)
& list_succeeds(X2)
& ! [X3,X4,X5] :
( occ(X4,X2) = occ(X4,X5)
| X3 = X4
| ~ delete_succeeds(X3,X2,X5) ) )
| X0 = nil ) ) ),
inference(flattening,[],[f666]) ).
fof(f668,plain,
? [X0,X1,X2,X3] :
( occ(X1,X2) != occ(X1,X3)
& list_succeeds(X2)
& delete_succeeds(X0,X2,X3)
& X0 != X1 ),
inference(ennf_transformation,[],[f293]) ).
fof(f669,plain,
? [X0,X1,X2,X3] :
( occ(X1,X2) != occ(X1,X3)
& list_succeeds(X2)
& delete_succeeds(X0,X2,X3)
& X0 != X1 ),
inference(flattening,[],[f668]) ).
fof(f737,plain,
! [X0,X1,X2] :
( ( delete_succeeds(X0,X1,X2)
| ( ! [X3,X4,X5] :
( cons(X3,X4) != X1
| cons(X3,X5) != X2
| ~ delete_succeeds(X0,X4,X5) )
& cons(X0,X2) != X1 ) )
& ( ? [X3,X4,X5] :
( X1 = cons(X3,X4)
& X2 = cons(X3,X5)
& delete_succeeds(X0,X4,X5) )
| X1 = cons(X0,X2)
| ~ delete_succeeds(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f61]) ).
fof(f738,plain,
! [X0,X1,X2] :
( ( delete_succeeds(X0,X1,X2)
| ( ! [X3,X4,X5] :
( cons(X3,X4) != X1
| cons(X3,X5) != X2
| ~ delete_succeeds(X0,X4,X5) )
& cons(X0,X2) != X1 ) )
& ( ? [X3,X4,X5] :
( X1 = cons(X3,X4)
& X2 = cons(X3,X5)
& delete_succeeds(X0,X4,X5) )
| X1 = cons(X0,X2)
| ~ delete_succeeds(X0,X1,X2) ) ),
inference(flattening,[],[f737]) ).
fof(f739,plain,
! [X0,X1,X2] :
( ( delete_succeeds(X0,X1,X2)
| ( ! [X3,X4,X5] :
( cons(X3,X4) != X1
| cons(X3,X5) != X2
| ~ delete_succeeds(X0,X4,X5) )
& cons(X0,X2) != X1 ) )
& ( ? [X6,X7,X8] :
( cons(X6,X7) = X1
& cons(X6,X8) = X2
& delete_succeeds(X0,X7,X8) )
| X1 = cons(X0,X2)
| ~ delete_succeeds(X0,X1,X2) ) ),
inference(rectify,[],[f738]) ).
fof(f740,plain,
! [X0,X1,X2] :
( ( delete_succeeds(X0,X1,X2)
| ( ! [X3,X4,X5] :
( cons(X3,X4) != X1
| cons(X3,X5) != X2
| ~ delete_succeeds(X0,X4,X5) )
& cons(X0,X2) != X1 ) )
& ( ( cons(sK36(X0,X1,X2),sK37(X0,X1,X2)) = X1
& cons(sK36(X0,X1,X2),sK38(X0,X1,X2)) = X2
& delete_succeeds(X0,sK37(X0,X1,X2),sK38(X0,X1,X2)) )
| X1 = cons(X0,X2)
| ~ delete_succeeds(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK36,sK37,sK38]),skolemize(X6,sK36(X0,X1,X2)),skolemize(X7,sK37(X0,X1,X2)),skolemize(X8,sK38(X0,X1,X2))],[f739]) ).
fof(f879,plain,
! [X0,X1,X2] :
( ( ( occ(X0,X1) = X2
| ~ occ_succeeds(X0,X1,X2) )
& ( occ_succeeds(X0,X1,X2)
| occ(X0,X1) != X2 ) )
| ~ list_succeeds(X1) ),
inference(nnf_transformation,[],[f640]) ).
fof(f881,plain,
( ! [X0] :
( ! [X1,X2,X3] :
( occ(X2,X3) = occ(X2,X0)
| X1 = X2
| ~ delete_succeeds(X1,X0,X3) )
| ~ list_succeeds(X0) )
| ? [X4] :
( ? [X5,X6,X7] :
( occ(X6,X7) != occ(X6,X4)
& X5 != X6
& delete_succeeds(X5,X4,X7) )
& ( ? [X8,X9] :
( cons(X8,X9) = X4
& list_succeeds(X9)
& ! [X10,X11,X12] :
( occ(X11,X12) = occ(X11,X9)
| X10 = X11
| ~ delete_succeeds(X10,X9,X12) ) )
| nil = X4 ) ) ),
inference(rectify,[],[f667]) ).
fof(f882,plain,
( ! [X0] :
( ! [X1,X2,X3] :
( occ(X2,X3) = occ(X2,X0)
| X1 = X2
| ~ delete_succeeds(X1,X0,X3) )
| ~ list_succeeds(X0) )
| ( occ(sK132,sK133) != occ(sK132,sK130)
& sK131 != sK132
& delete_succeeds(sK131,sK130,sK133)
& ( ( sK130 = cons(sK134,sK135)
& list_succeeds(sK135)
& ! [X10,X11,X12] :
( occ(X11,X12) = occ(X11,sK135)
| X10 = X11
| ~ delete_succeeds(X10,sK135,X12) ) )
| nil = sK130 ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK130,sK131,sK132,sK133,sK134,sK135]),skolemize(X4,sK130),skolemize(X5,sK131),skolemize(X6,sK132),skolemize(X7,sK133),skolemize(X8,sK134),skolemize(X9,sK135)],[f881]) ).
fof(f883,plain,
( occ(sK137,sK138) != occ(sK137,sK139)
& list_succeeds(sK138)
& delete_succeeds(sK136,sK138,sK139)
& sK136 != sK137 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK136,sK137,sK138,sK139]),skolemize(X0,sK136),skolemize(X1,sK137),skolemize(X2,sK138),skolemize(X3,sK139)],[f669]) ).
fof(f888,plain,
! [X0,X1] : nil != cons(X0,X1),
inference(cnf_transformation,[],[f5]) ).
fof(f891,plain,
! [X2,X3,X0,X1] :
( cons(X0,X1) != cons(X2,X3)
| X1 = X3 ),
inference(cnf_transformation,[],[f320]) ).
fof(f892,plain,
! [X2,X3,X0,X1] :
( cons(X0,X1) != cons(X2,X3)
| X0 = X2 ),
inference(cnf_transformation,[],[f321]) ).
fof(f1032,plain,
! [X2,X0,X1] :
( delete_succeeds(X0,sK37(X0,X1,X2),sK38(X0,X1,X2))
| cons(X0,X2) = X1
| ~ delete_succeeds(X0,X1,X2) ),
inference(cnf_transformation,[],[f740]) ).
fof(f1033,plain,
! [X2,X0,X1] :
( ~ delete_succeeds(X0,X1,X2)
| cons(X0,X2) = X1
| cons(sK36(X0,X1,X2),sK38(X0,X1,X2)) = X2 ),
inference(cnf_transformation,[],[f740]) ).
fof(f1034,plain,
! [X2,X0,X1] :
( ~ delete_succeeds(X0,X1,X2)
| cons(X0,X2) = X1
| cons(sK36(X0,X1,X2),sK37(X0,X1,X2)) = X1 ),
inference(cnf_transformation,[],[f740]) ).
fof(f1375,plain,
! [X2,X0,X1] :
( ~ delete_succeeds(X0,X1,X2)
| list_succeeds(X2)
| ~ list_succeeds(X1) ),
inference(cnf_transformation,[],[f615]) ).
fof(f1402,plain,
! [X2,X0,X1] :
( occ_succeeds(X0,X1,X2)
| occ(X0,X1) != X2
| ~ list_succeeds(X1) ),
inference(cnf_transformation,[],[f879]) ).
fof(f1403,plain,
! [X2,X0,X1] :
( occ(X0,X1) = X2
| ~ occ_succeeds(X0,X1,X2)
| ~ list_succeeds(X1) ),
inference(cnf_transformation,[],[f879]) ).
fof(f1415,plain,
! [X2,X0,X1] :
( list_succeeds(X1)
| ~ occ_succeeds(X0,X1,X2) ),
inference(cnf_transformation,[],[f656]) ).
fof(f1419,plain,
! [X2,X0,X1] :
( ~ list_succeeds(X2)
| occ(X0,cons(X1,X2)) = occ(X0,X2)
| X0 = X1 ),
inference(cnf_transformation,[],[f661]) ).
fof(f1420,plain,
! [X0,X1] :
( ~ list_succeeds(X1)
| occ(X0,cons(X0,X1)) = s(occ(X0,X1)) ),
inference(cnf_transformation,[],[f662]) ).
fof(f1423,plain,
! [X2,X3,X10,X0,X11,X1,X12] :
( occ(X2,X3) = occ(X2,X0)
| X1 = X2
| ~ delete_succeeds(X1,X0,X3)
| ~ list_succeeds(X0)
| occ(X11,X12) = occ(X11,sK135)
| X10 = X11
| ~ delete_succeeds(X10,sK135,X12)
| nil = sK130 ),
inference(cnf_transformation,[],[f882]) ).
fof(f1424,plain,
! [X2,X3,X0,X1] :
( occ(X2,X3) = occ(X2,X0)
| X1 = X2
| ~ delete_succeeds(X1,X0,X3)
| ~ list_succeeds(X0)
| list_succeeds(sK135)
| nil = sK130 ),
inference(cnf_transformation,[],[f882]) ).
fof(f1425,plain,
! [X2,X3,X0,X1] :
( occ(X2,X3) = occ(X2,X0)
| X1 = X2
| ~ delete_succeeds(X1,X0,X3)
| ~ list_succeeds(X0)
| sK130 = cons(sK134,sK135)
| nil = sK130 ),
inference(cnf_transformation,[],[f882]) ).
fof(f1426,plain,
! [X2,X3,X0,X1] :
( occ(X2,X3) = occ(X2,X0)
| X1 = X2
| ~ delete_succeeds(X1,X0,X3)
| ~ list_succeeds(X0)
| delete_succeeds(sK131,sK130,sK133) ),
inference(cnf_transformation,[],[f882]) ).
fof(f1427,plain,
! [X2,X3,X0,X1] :
( occ(X2,X3) = occ(X2,X0)
| X1 = X2
| ~ delete_succeeds(X1,X0,X3)
| ~ list_succeeds(X0)
| sK131 != sK132 ),
inference(cnf_transformation,[],[f882]) ).
fof(f1428,plain,
! [X2,X3,X0,X1] :
( occ(X2,X3) = occ(X2,X0)
| X1 = X2
| ~ delete_succeeds(X1,X0,X3)
| ~ list_succeeds(X0)
| occ(sK132,sK133) != occ(sK132,sK130) ),
inference(cnf_transformation,[],[f882]) ).
fof(f1429,plain,
sK136 != sK137,
inference(cnf_transformation,[],[f883]) ).
fof(f1430,plain,
delete_succeeds(sK136,sK138,sK139),
inference(cnf_transformation,[],[f883]) ).
fof(f1431,plain,
list_succeeds(sK138),
inference(cnf_transformation,[],[f883]) ).
fof(f1432,plain,
occ(sK137,sK138) != occ(sK137,sK139),
inference(cnf_transformation,[],[f883]) ).
fof(f1546,plain,
! [X0,X1] :
( occ_succeeds(X0,X1,occ(X0,X1))
| ~ list_succeeds(X1) ),
inference(equality_resolution,[],[f1402]) ).
fof(f1548,definition,
sF140 = occ(sK137,sK138),
introduced(definition,[new_symbols(definition,[sF140])],[function_definition]) ).
fof(f1549,plain,
occ(sK137,sK138) = sF140,
inference(reorient_equations,[],[f1548]) ).
fof(f1550,definition,
sF141 = occ(sK137,sK139),
introduced(definition,[new_symbols(definition,[sF141])],[function_definition]) ).
fof(f1551,plain,
occ(sK137,sK139) = sF141,
inference(reorient_equations,[],[f1550]) ).
fof(f1552,plain,
sF140 != sF141,
inference(definition_folding,[],[f1432,f1551,f1549]) ).
fof(f1554,definition,
( spl142_1
<=> nil = sK130 ),
introduced(definition,[new_symbols(definition,[spl142_1])],[avatar_definition]) ).
fof(f1556,plain,
( nil = sK130
| ~ spl142_1 ),
inference(avatar_component_clause,[],[f1554]) ).
fof(f1558,definition,
( spl142_2
<=> ! [X12,X11,X10] :
( occ(X11,X12) = occ(X11,sK135)
| ~ delete_succeeds(X10,sK135,X12)
| X10 = X11 ) ),
introduced(definition,[new_symbols(definition,[spl142_2])],[avatar_definition]) ).
fof(f1559,plain,
( ! [X10,X11,X12] :
( ~ delete_succeeds(X10,sK135,X12)
| occ(X11,X12) = occ(X11,sK135)
| X10 = X11 )
| ~ spl142_2 ),
inference(avatar_component_clause,[],[f1558]) ).
fof(f1561,definition,
( spl142_3
<=> ! [X0,X3,X2,X1] :
( occ(X2,X3) = occ(X2,X0)
| ~ list_succeeds(X0)
| ~ delete_succeeds(X1,X0,X3)
| X1 = X2 ) ),
introduced(definition,[new_symbols(definition,[spl142_3])],[avatar_definition]) ).
fof(f1562,plain,
( ! [X2,X3,X0,X1] :
( ~ delete_succeeds(X1,X0,X3)
| ~ list_succeeds(X0)
| occ(X2,X3) = occ(X2,X0)
| X1 = X2 )
| ~ spl142_3 ),
inference(avatar_component_clause,[],[f1561]) ).
fof(f1563,plain,
( spl142_1
| spl142_2
| spl142_3 ),
inference(avatar_split_clause,[],[f1423,f1561,f1558,f1554]) ).
fof(f1565,definition,
( spl142_4
<=> list_succeeds(sK135) ),
introduced(definition,[new_symbols(definition,[spl142_4])],[avatar_definition]) ).
fof(f1567,plain,
( list_succeeds(sK135)
| ~ spl142_4 ),
inference(avatar_component_clause,[],[f1565]) ).
fof(f1568,plain,
( spl142_1
| spl142_4
| spl142_3 ),
inference(avatar_split_clause,[],[f1424,f1561,f1565,f1554]) ).
fof(f1570,definition,
( spl142_5
<=> sK130 = cons(sK134,sK135) ),
introduced(definition,[new_symbols(definition,[spl142_5])],[avatar_definition]) ).
fof(f1572,plain,
( sK130 = cons(sK134,sK135)
| ~ spl142_5 ),
inference(avatar_component_clause,[],[f1570]) ).
fof(f1573,plain,
( spl142_1
| spl142_5
| spl142_3 ),
inference(avatar_split_clause,[],[f1425,f1561,f1570,f1554]) ).
fof(f1575,definition,
( spl142_6
<=> delete_succeeds(sK131,sK130,sK133) ),
introduced(definition,[new_symbols(definition,[spl142_6])],[avatar_definition]) ).
fof(f1577,plain,
( delete_succeeds(sK131,sK130,sK133)
| ~ spl142_6 ),
inference(avatar_component_clause,[],[f1575]) ).
fof(f1578,plain,
( spl142_6
| spl142_3 ),
inference(avatar_split_clause,[],[f1426,f1561,f1575]) ).
fof(f1580,definition,
( spl142_7
<=> sK131 = sK132 ),
introduced(definition,[new_symbols(definition,[spl142_7])],[avatar_definition]) ).
fof(f1582,plain,
( sK131 != sK132
| spl142_7 ),
inference(avatar_component_clause,[],[f1580]) ).
fof(f1583,plain,
( ~ spl142_7
| spl142_3 ),
inference(avatar_split_clause,[],[f1427,f1561,f1580]) ).
fof(f1585,definition,
( spl142_8
<=> occ(sK132,sK133) = occ(sK132,sK130) ),
introduced(definition,[new_symbols(definition,[spl142_8])],[avatar_definition]) ).
fof(f1587,plain,
( occ(sK132,sK133) != occ(sK132,sK130)
| spl142_8 ),
inference(avatar_component_clause,[],[f1585]) ).
fof(f1588,plain,
( ~ spl142_8
| spl142_3 ),
inference(avatar_split_clause,[],[f1428,f1561,f1585]) ).
fof(f1589,plain,
! [X2,X0,X1] :
( ~ occ_succeeds(X0,X1,X2)
| occ(X0,X1) = X2 ),
inference(forward_subsumption_resolution,[],[f1403,f1415]) ).
fof(f1590,plain,
( ! [X0] :
( ~ list_succeeds(sK138)
| occ(X0,sK139) = occ(X0,sK138)
| sK136 = X0 )
| ~ spl142_3 ),
inference(resolution,[],[f1562,f1430]) ).
fof(f1591,plain,
( ! [X0] :
( occ(X0,sK139) = occ(X0,sK138)
| sK136 = X0 )
| ~ spl142_3 ),
inference(forward_subsumption_resolution,[],[f1590,f1431]) ).
fof(f1592,plain,
( occ(sK137,sK138) = sF141
| sK136 = sK137
| ~ spl142_3 ),
inference(superposition,[],[f1591,f1551]) ).
fof(f1595,plain,
( occ(sK137,sK138) = sF141
| ~ spl142_3 ),
inference(forward_subsumption_resolution,[],[f1592,f1429]) ).
fof(f1597,plain,
( sF140 = sF141
| ~ spl142_3 ),
inference(forward_demodulation,[],[f1595,f1549]) ).
fof(f1600,plain,
( $false
| ~ spl142_3 ),
inference(forward_subsumption_resolution,[],[f1597,f1552]) ).
fof(f1601,plain,
~ spl142_3,
inference(avatar_contradiction_clause,[],[f1600]) ).
fof(f1602,plain,
( delete_succeeds(sK131,nil,sK133)
| ~ spl142_1
| ~ spl142_6 ),
inference(forward_demodulation,[],[f1577,f1556]) ).
fof(f1660,plain,
( nil = cons(sK131,sK133)
| nil = cons(sK36(sK131,nil,sK133),sK37(sK131,nil,sK133))
| ~ spl142_1
| ~ spl142_6 ),
inference(resolution,[],[f1034,f1602]) ).
fof(f1662,plain,
( nil = cons(sK131,sK133)
| ~ spl142_1
| ~ spl142_6 ),
inference(forward_subsumption_resolution,[],[f1660,f888]) ).
fof(f1668,plain,
( $false
| ~ spl142_1
| ~ spl142_6 ),
inference(forward_subsumption_resolution,[],[f1662,f888]) ).
fof(f1669,plain,
( ~ spl142_1
| ~ spl142_6 ),
inference(avatar_contradiction_clause,[],[f1668]) ).
fof(f1670,plain,
( sK130 = cons(sK131,sK133)
| sK130 = cons(sK36(sK131,sK130,sK133),sK37(sK131,sK130,sK133))
| ~ spl142_6 ),
inference(resolution,[],[f1577,f1034]) ).
fof(f1672,plain,
( sK130 = cons(sK131,sK133)
| sK133 = cons(sK36(sK131,sK130,sK133),sK38(sK131,sK130,sK133))
| ~ spl142_6 ),
inference(resolution,[],[f1577,f1033]) ).
fof(f1686,definition,
( spl142_16
<=> sK133 = cons(sK36(sK131,sK130,sK133),sK38(sK131,sK130,sK133)) ),
introduced(definition,[new_symbols(definition,[spl142_16])],[avatar_definition]) ).
fof(f1688,plain,
( sK133 = cons(sK36(sK131,sK130,sK133),sK38(sK131,sK130,sK133))
| ~ spl142_16 ),
inference(avatar_component_clause,[],[f1686]) ).
fof(f1690,definition,
( spl142_17
<=> sK130 = cons(sK131,sK133) ),
introduced(definition,[new_symbols(definition,[spl142_17])],[avatar_definition]) ).
fof(f1691,plain,
( sK130 != cons(sK131,sK133)
| spl142_17 ),
inference(avatar_component_clause,[],[f1690]) ).
fof(f1692,plain,
( sK130 = cons(sK131,sK133)
| ~ spl142_17 ),
inference(avatar_component_clause,[],[f1690]) ).
fof(f1693,plain,
( spl142_16
| spl142_17
| ~ spl142_6 ),
inference(avatar_split_clause,[],[f1672,f1575,f1690,f1686]) ).
fof(f1696,definition,
( spl142_18
<=> sK130 = cons(sK36(sK131,sK130,sK133),sK37(sK131,sK130,sK133)) ),
introduced(definition,[new_symbols(definition,[spl142_18])],[avatar_definition]) ).
fof(f1698,plain,
( sK130 = cons(sK36(sK131,sK130,sK133),sK37(sK131,sK130,sK133))
| ~ spl142_18 ),
inference(avatar_component_clause,[],[f1696]) ).
fof(f1699,plain,
( spl142_18
| spl142_17
| ~ spl142_6 ),
inference(avatar_split_clause,[],[f1670,f1575,f1690,f1696]) ).
fof(f1700,plain,
( ! [X0,X1] :
( occ(X0,cons(X1,sK135)) = occ(X0,sK135)
| X0 = X1 )
| ~ spl142_4 ),
inference(resolution,[],[f1567,f1419]) ).
fof(f1701,plain,
( ! [X0] : occ(X0,cons(X0,sK135)) = s(occ(X0,sK135))
| ~ spl142_4 ),
inference(resolution,[],[f1567,f1420]) ).
fof(f1704,plain,
( s(occ(sK134,sK135)) = occ(sK134,sK130)
| ~ spl142_4
| ~ spl142_5 ),
inference(superposition,[],[f1701,f1572]) ).
fof(f1776,plain,
( ! [X0,X1] :
( cons(X0,X1) != sK130
| sK134 = X0 )
| ~ spl142_5 ),
inference(superposition,[],[f892,f1572]) ).
fof(f1783,plain,
( ! [X0,X1] :
( cons(X0,X1) != sK130
| sK135 = X1 )
| ~ spl142_5 ),
inference(superposition,[],[f891,f1572]) ).
fof(f1784,plain,
( ! [X0,X1] :
( cons(X0,X1) != sK130
| sK133 = X1 )
| ~ spl142_17 ),
inference(superposition,[],[f891,f1692]) ).
fof(f1787,plain,
( sK130 != sK130
| sK133 = sK135
| ~ spl142_5
| ~ spl142_17 ),
inference(superposition,[],[f1784,f1572]) ).
fof(f1789,plain,
( sK133 = sK135
| ~ spl142_5
| ~ spl142_17 ),
inference(trivial_inequality_removal,[],[f1787]) ).
fof(f1800,plain,
( occ(sK132,sK130) != occ(sK132,sK135)
| ~ spl142_5
| spl142_8
| ~ spl142_17 ),
inference(superposition,[],[f1587,f1789]) ).
fof(f1803,plain,
( sK130 = cons(sK131,sK135)
| ~ spl142_5
| ~ spl142_17 ),
inference(superposition,[],[f1692,f1789]) ).
fof(f1835,plain,
( ! [X0] :
( occ(X0,sK135) = occ(X0,sK130)
| sK131 = X0 )
| ~ spl142_4
| ~ spl142_5
| ~ spl142_17 ),
inference(superposition,[],[f1700,f1803]) ).
fof(f1873,plain,
( occ(sK132,sK130) != occ(sK132,sK130)
| sK131 = sK132
| ~ spl142_4
| ~ spl142_5
| spl142_8
| ~ spl142_17 ),
inference(superposition,[],[f1800,f1835]) ).
fof(f1875,plain,
( sK131 = sK132
| ~ spl142_4
| ~ spl142_5
| spl142_8
| ~ spl142_17 ),
inference(trivial_inequality_removal,[],[f1873]) ).
fof(f1877,plain,
( $false
| ~ spl142_4
| ~ spl142_5
| spl142_7
| spl142_8
| ~ spl142_17 ),
inference(forward_subsumption_resolution,[],[f1875,f1582]) ).
fof(f1878,plain,
( ~ spl142_4
| ~ spl142_5
| spl142_7
| spl142_8
| ~ spl142_17 ),
inference(avatar_contradiction_clause,[],[f1877]) ).
fof(f1905,plain,
( sK130 != sK130
| sK135 = sK37(sK131,sK130,sK133)
| ~ spl142_5
| ~ spl142_18 ),
inference(superposition,[],[f1783,f1698]) ).
fof(f1908,plain,
( sK135 = sK37(sK131,sK130,sK133)
| ~ spl142_5
| ~ spl142_18 ),
inference(trivial_inequality_removal,[],[f1905]) ).
fof(f1927,plain,
( sK130 = cons(sK36(sK131,sK130,sK133),sK135)
| ~ spl142_5
| ~ spl142_18 ),
inference(superposition,[],[f1698,f1908]) ).
fof(f1928,plain,
( ! [X0] :
( occ(X0,sK135) = occ(X0,sK130)
| sK36(sK131,sK130,sK133) = X0 )
| ~ spl142_4
| ~ spl142_5
| ~ spl142_18 ),
inference(superposition,[],[f1700,f1927]) ).
fof(f1929,plain,
( s(occ(sK36(sK131,sK130,sK133),sK135)) = occ(sK36(sK131,sK130,sK133),sK130)
| ~ spl142_4
| ~ spl142_5
| ~ spl142_18 ),
inference(superposition,[],[f1701,f1927]) ).
fof(f1941,plain,
( ! [X0] :
( sK133 = cons(X0,sK38(sK131,sK130,sK133))
| occ(X0,sK135) = occ(X0,sK130) )
| ~ spl142_4
| ~ spl142_5
| ~ spl142_16
| ~ spl142_18 ),
inference(superposition,[],[f1688,f1928]) ).
fof(f1998,plain,
( delete_succeeds(sK131,sK135,sK38(sK131,sK130,sK133))
| sK130 = cons(sK131,sK133)
| ~ delete_succeeds(sK131,sK130,sK133)
| ~ spl142_5
| ~ spl142_18 ),
inference(superposition,[],[f1032,f1908]) ).
fof(f1999,plain,
( delete_succeeds(sK131,sK135,sK38(sK131,sK130,sK133))
| ~ delete_succeeds(sK131,sK130,sK133)
| ~ spl142_5
| spl142_17
| ~ spl142_18 ),
inference(forward_subsumption_resolution,[],[f1998,f1691]) ).
fof(f2000,plain,
( delete_succeeds(sK131,sK135,sK38(sK131,sK130,sK133))
| ~ spl142_5
| ~ spl142_6
| spl142_17
| ~ spl142_18 ),
inference(forward_subsumption_resolution,[],[f1999,f1577]) ).
fof(f2001,plain,
( ! [X0] :
( occ(X0,sK135) = occ(X0,sK38(sK131,sK130,sK133))
| sK131 = X0 )
| ~ spl142_2
| ~ spl142_5
| ~ spl142_6
| spl142_17
| ~ spl142_18 ),
inference(resolution,[],[f2000,f1559]) ).
fof(f2005,plain,
( list_succeeds(sK38(sK131,sK130,sK133))
| ~ list_succeeds(sK135)
| ~ spl142_5
| ~ spl142_6
| spl142_17
| ~ spl142_18 ),
inference(resolution,[],[f2000,f1375]) ).
fof(f2008,plain,
( list_succeeds(sK38(sK131,sK130,sK133))
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| spl142_17
| ~ spl142_18 ),
inference(forward_subsumption_resolution,[],[f2005,f1567]) ).
fof(f2023,plain,
( ! [X0] :
( occ_succeeds(X0,sK38(sK131,sK130,sK133),occ(X0,sK135))
| ~ list_succeeds(sK38(sK131,sK130,sK133))
| sK131 = X0 )
| ~ spl142_2
| ~ spl142_5
| ~ spl142_6
| spl142_17
| ~ spl142_18 ),
inference(superposition,[],[f1546,f2001]) ).
fof(f2026,plain,
( ! [X0] :
( occ_succeeds(X0,sK38(sK131,sK130,sK133),occ(X0,sK135))
| sK131 = X0 )
| ~ spl142_2
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| spl142_17
| ~ spl142_18 ),
inference(forward_subsumption_resolution,[],[f2023,f2008]) ).
fof(f2029,plain,
( ! [X0,X1] :
( occ(X0,sK38(sK131,sK130,sK133)) = occ(X0,cons(X1,sK38(sK131,sK130,sK133)))
| X0 = X1 )
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| spl142_17
| ~ spl142_18 ),
inference(resolution,[],[f2008,f1419]) ).
fof(f2030,plain,
( ! [X0] : occ(X0,cons(X0,sK38(sK131,sK130,sK133))) = s(occ(X0,sK38(sK131,sK130,sK133)))
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| spl142_17
| ~ spl142_18 ),
inference(resolution,[],[f2008,f1420]) ).
fof(f2031,plain,
( ! [X0] :
( occ(X0,sK133) = s(occ(X0,sK38(sK131,sK130,sK133)))
| occ(X0,sK135) = occ(X0,sK130) )
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| ~ spl142_16
| spl142_17
| ~ spl142_18 ),
inference(superposition,[],[f2030,f1941]) ).
fof(f2158,plain,
( sK130 != sK130
| sK134 = sK36(sK131,sK130,sK133)
| ~ spl142_5
| ~ spl142_18 ),
inference(superposition,[],[f1776,f1927]) ).
fof(f2161,plain,
( sK134 = sK36(sK131,sK130,sK133)
| ~ spl142_5
| ~ spl142_18 ),
inference(trivial_inequality_removal,[],[f2158]) ).
fof(f2167,plain,
( sK133 = cons(sK134,sK38(sK131,sK130,sK133))
| ~ spl142_5
| ~ spl142_16
| ~ spl142_18 ),
inference(superposition,[],[f1688,f2161]) ).
fof(f2171,plain,
( s(occ(sK134,sK38(sK131,sK130,sK133))) = occ(sK134,sK133)
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| ~ spl142_16
| spl142_17
| ~ spl142_18 ),
inference(superposition,[],[f2030,f2167]) ).
fof(f2267,plain,
( ! [X0] :
( occ(X0,sK133) = s(occ(X0,sK135))
| occ(X0,sK135) = occ(X0,sK130)
| sK131 = X0 )
| ~ spl142_2
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| ~ spl142_16
| spl142_17
| ~ spl142_18 ),
inference(superposition,[],[f2031,f2001]) ).
fof(f2275,plain,
( ! [X0] :
( occ(X0,sK133) = occ(X0,sK38(sK131,sK130,sK133))
| sK134 = X0 )
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| ~ spl142_16
| spl142_17
| ~ spl142_18 ),
inference(superposition,[],[f2029,f2167]) ).
fof(f2413,plain,
( ! [X0] :
( s(occ(X0,sK135)) = occ(X0,sK130)
| occ(X0,sK135) = occ(X0,sK130) )
| ~ spl142_4
| ~ spl142_5
| ~ spl142_18 ),
inference(superposition,[],[f1929,f1928]) ).
fof(f2432,plain,
( ! [X0] :
( occ(X0,sK133) = occ(X0,sK130)
| occ(X0,sK135) = occ(X0,sK130)
| sK131 = X0
| occ(X0,sK135) = occ(X0,sK130) )
| ~ spl142_2
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| ~ spl142_16
| spl142_17
| ~ spl142_18 ),
inference(superposition,[],[f2267,f2413]) ).
fof(f2436,plain,
( ! [X0] :
( occ(X0,sK133) = occ(X0,sK130)
| occ(X0,sK135) = occ(X0,sK130)
| sK131 = X0 )
| ~ spl142_2
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| ~ spl142_16
| spl142_17
| ~ spl142_18 ),
inference(duplicate_literal_removal,[],[f2432]) ).
fof(f2441,plain,
( occ(sK132,sK130) != occ(sK132,sK130)
| occ(sK132,sK130) = occ(sK132,sK135)
| sK131 = sK132
| ~ spl142_2
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| spl142_8
| ~ spl142_16
| spl142_17
| ~ spl142_18 ),
inference(superposition,[],[f1587,f2436]) ).
fof(f2442,plain,
( occ(sK132,sK130) = occ(sK132,sK135)
| sK131 = sK132
| ~ spl142_2
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| spl142_8
| ~ spl142_16
| spl142_17
| ~ spl142_18 ),
inference(trivial_inequality_removal,[],[f2441]) ).
fof(f2444,plain,
( occ(sK132,sK130) = occ(sK132,sK135)
| ~ spl142_2
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| spl142_7
| spl142_8
| ~ spl142_16
| spl142_17
| ~ spl142_18 ),
inference(forward_subsumption_resolution,[],[f2442,f1582]) ).
fof(f2445,plain,
( occ_succeeds(sK132,sK38(sK131,sK130,sK133),occ(sK132,sK130))
| sK131 = sK132
| ~ spl142_2
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| spl142_7
| spl142_8
| ~ spl142_16
| spl142_17
| ~ spl142_18 ),
inference(superposition,[],[f2026,f2444]) ).
fof(f2450,plain,
( occ_succeeds(sK132,sK38(sK131,sK130,sK133),occ(sK132,sK130))
| ~ spl142_2
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| spl142_7
| spl142_8
| ~ spl142_16
| spl142_17
| ~ spl142_18 ),
inference(forward_subsumption_resolution,[],[f2445,f1582]) ).
fof(f2453,plain,
( occ(sK132,sK130) = occ(sK132,sK38(sK131,sK130,sK133))
| ~ spl142_2
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| spl142_7
| spl142_8
| ~ spl142_16
| spl142_17
| ~ spl142_18 ),
inference(resolution,[],[f2450,f1589]) ).
fof(f2504,definition,
( spl142_60
<=> sK132 = sK134 ),
introduced(definition,[new_symbols(definition,[spl142_60])],[avatar_definition]) ).
fof(f2506,plain,
( sK132 = sK134
| ~ spl142_60 ),
inference(avatar_component_clause,[],[f2504]) ).
fof(f2544,plain,
( occ(sK132,sK133) = occ(sK132,sK130)
| sK132 = sK134
| ~ spl142_2
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| spl142_7
| spl142_8
| ~ spl142_16
| spl142_17
| ~ spl142_18 ),
inference(superposition,[],[f2453,f2275]) ).
fof(f2545,plain,
( sK132 = sK134
| ~ spl142_2
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| spl142_7
| spl142_8
| ~ spl142_16
| spl142_17
| ~ spl142_18 ),
inference(forward_subsumption_resolution,[],[f2544,f1587]) ).
fof(f2549,plain,
( spl142_60
| ~ spl142_2
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| spl142_7
| spl142_8
| ~ spl142_16
| spl142_17
| ~ spl142_18 ),
inference(avatar_split_clause,[],[f2545,f1696,f1690,f1686,f1585,f1580,f1575,f1570,f1565,f1558,f2504]) ).
fof(f2553,plain,
( occ(sK132,sK130) = s(occ(sK132,sK135))
| ~ spl142_4
| ~ spl142_5
| ~ spl142_60 ),
inference(superposition,[],[f1704,f2506]) ).
fof(f2558,plain,
( occ(sK132,sK133) = s(occ(sK132,sK38(sK131,sK130,sK133)))
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| ~ spl142_16
| spl142_17
| ~ spl142_18
| ~ spl142_60 ),
inference(superposition,[],[f2171,f2506]) ).
fof(f2568,plain,
( occ(sK132,sK133) = s(occ(sK132,sK130))
| ~ spl142_2
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| spl142_7
| spl142_8
| ~ spl142_16
| spl142_17
| ~ spl142_18
| ~ spl142_60 ),
inference(forward_demodulation,[],[f2558,f2453]) ).
fof(f2572,plain,
( occ(sK132,sK130) = s(occ(sK132,sK130))
| ~ spl142_2
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| spl142_7
| spl142_8
| ~ spl142_16
| spl142_17
| ~ spl142_18
| ~ spl142_60 ),
inference(forward_demodulation,[],[f2553,f2444]) ).
fof(f2573,plain,
( occ(sK132,sK133) = occ(sK132,sK130)
| ~ spl142_2
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| spl142_7
| spl142_8
| ~ spl142_16
| spl142_17
| ~ spl142_18
| ~ spl142_60 ),
inference(forward_demodulation,[],[f2572,f2568]) ).
fof(f2574,plain,
( $false
| ~ spl142_2
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| spl142_7
| spl142_8
| ~ spl142_16
| spl142_17
| ~ spl142_18
| ~ spl142_60 ),
inference(forward_subsumption_resolution,[],[f2573,f1587]) ).
fof(f2575,plain,
( ~ spl142_2
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| spl142_7
| spl142_8
| ~ spl142_16
| spl142_17
| ~ spl142_18
| ~ spl142_60 ),
inference(avatar_contradiction_clause,[],[f2574]) ).
cnf(s1,plain,
( spl142_1
| spl142_2
| spl142_3 ),
inference(sat_conversion,[],[f1563]) ).
cnf(s2,plain,
( spl142_1
| spl142_3
| spl142_4 ),
inference(sat_conversion,[],[f1568]) ).
cnf(s3,plain,
( spl142_1
| spl142_3
| spl142_5 ),
inference(sat_conversion,[],[f1573]) ).
cnf(s4,plain,
( spl142_3
| spl142_6 ),
inference(sat_conversion,[],[f1578]) ).
cnf(s5,plain,
( spl142_3
| ~ spl142_7 ),
inference(sat_conversion,[],[f1583]) ).
cnf(s6,plain,
( spl142_3
| ~ spl142_8 ),
inference(sat_conversion,[],[f1588]) ).
cnf(s8,plain,
~ spl142_3,
inference(sat_conversion,[],[f1601]) ).
cnf(s13,plain,
( ~ spl142_1
| ~ spl142_6 ),
inference(sat_conversion,[],[f1669]) ).
cnf(s15,plain,
( ~ spl142_6
| spl142_16
| spl142_17 ),
inference(sat_conversion,[],[f1693]) ).
cnf(s17,plain,
( ~ spl142_6
| spl142_17
| spl142_18 ),
inference(sat_conversion,[],[f1699]) ).
cnf(s20,plain,
( ~ spl142_4
| ~ spl142_5
| spl142_7
| spl142_8
| ~ spl142_17 ),
inference(sat_conversion,[],[f1878]) ).
cnf(s51,plain,
( ~ spl142_2
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| spl142_7
| spl142_8
| ~ spl142_16
| spl142_17
| ~ spl142_18
| spl142_60 ),
inference(sat_conversion,[],[f2549]) ).
cnf(s55,plain,
( ~ spl142_2
| ~ spl142_4
| ~ spl142_5
| ~ spl142_6
| spl142_7
| spl142_8
| ~ spl142_16
| spl142_17
| ~ spl142_18
| ~ spl142_60 ),
inference(sat_conversion,[],[f2575]) ).
cnf(s57,plain,
~ spl142_8,
inference(rat,[],[s6,s8]) ).
cnf(s58,plain,
~ spl142_7,
inference(rat,[],[s5,s8]) ).
cnf(s59,plain,
spl142_6,
inference(rat,[],[s4,s8]) ).
cnf(s60,plain,
~ spl142_1,
inference(rat,[],[s13,s59]) ).
cnf(s61,plain,
spl142_5,
inference(rat,[],[s3,s8,s60]) ).
cnf(s62,plain,
spl142_4,
inference(rat,[],[s2,s8,s60]) ).
cnf(s63,plain,
~ spl142_17,
inference(rat,[],[s20,s61,s57,s58,s62]) ).
cnf(s64,plain,
spl142_18,
inference(rat,[],[s17,s59,s63]) ).
cnf(s65,plain,
spl142_16,
inference(rat,[],[s15,s59,s63]) ).
cnf(s66,plain,
spl142_2,
inference(rat,[],[s1,s8,s60]) ).
cnf(s67,plain,
~ spl142_60,
inference(rat,[],[s55,s65,s64,s63,s62,s57,s58,s59,s61,s66]) ).
cnf(s68,plain,
$false,
inference(rat,[],[s51,s65,s64,s63,s62,s57,s58,s59,s61,s67,s66]) ).
fof(f2576,plain,
$false,
inference(avatar_sat_refutation,[],[s68]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX050+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n011.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 14:54:46 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.85/1.44 % (3445936)Detected formulas, will run a generic FOF schedule.
% 4.85/1.44 % (3445941)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2947028063:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.85/1.44 % (3445945)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=135274130:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.85/1.44 % (3445947)dis-21_1_sil=8000:lcm=predicate:random_seed=857714812:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 4.85/1.44 % (3445942)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1207629263:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.85/1.44 % (3445946)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2156874835:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.85/1.44 % (3445944)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2347690665:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.85/1.44 % (3445943)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=2222122891:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.85/1.44 % (3445944)Instruction limit reached!
% 4.85/1.44 % (3445944)------------------------------
% 4.85/1.44 % (3445944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.85/1.44 % (3445944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.44 % (3445944)CaDiCaL version: 2.1.3
% 4.85/1.44 % (3445944)Termination reason: Instruction limit
% 4.85/1.44 % (3445944)Termination phase: Saturation
% 4.85/1.44 % (3445944)Time elapsed: 0.063 s
% 4.85/1.44 % (3445944)Peak memory usage: 89 MB
% 4.85/1.44 % (3445944)Instructions burned: 110 (million)
% 4.85/1.44 % (3445945)Instruction limit reached!
% 4.85/1.44 % (3445945)------------------------------
% 4.85/1.44 % (3445945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.85/1.44 % (3445945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.44 % (3445945)CaDiCaL version: 2.1.3
% 4.85/1.44 % (3445945)Termination reason: Instruction limit
% 4.85/1.44 % (3445945)Termination phase: Saturation
% 4.85/1.44 % (3445945)Time elapsed: 0.068 s
% 4.85/1.44 % (3445945)Peak memory usage: 88 MB
% 4.85/1.44 % (3445945)Instructions burned: 119 (million)
% 4.85/1.44 % (3445947)Instruction limit reached!
% 4.85/1.44 % (3445947)------------------------------
% 4.85/1.44 % (3445947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.85/1.44 % (3445947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.44 % (3445947)CaDiCaL version: 2.1.3
% 4.85/1.44 % (3445947)Termination reason: Instruction limit
% 4.85/1.44 % (3445947)Termination phase: Saturation
% 4.85/1.44 % (3445947)Time elapsed: 0.082 s
% 4.85/1.44 % (3445947)Peak memory usage: 89 MB
% 4.85/1.44 % (3445947)Instructions burned: 129 (million)
% 4.85/1.44 % (3445946)Instruction limit reached!
% 4.85/1.44 % (3445946)------------------------------
% 4.85/1.44 % (3445946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.85/1.44 % (3445946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.44 % (3445946)CaDiCaL version: 2.1.3
% 4.85/1.44 % (3445946)Termination reason: Instruction limit
% 4.85/1.44 % (3445946)Termination phase: Saturation
% 4.85/1.44 % (3445946)Time elapsed: 0.097 s
% 4.85/1.44 % (3445946)Peak memory usage: 90 MB
% 4.85/1.44 % (3445946)Instructions burned: 139 (million)
% 4.85/1.44 % (3445956)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2446306893:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 4.85/1.44 % (3445955)lrs+10_1_sil=8000:sp=occurrence:random_seed=2612044067:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 4.85/1.44 % (3445957)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1267911677:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 4.85/1.44 % (3445958)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3631925084:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 4.85/1.44 % (3445956)Instruction limit reached!
% 4.85/1.44 % (3445956)------------------------------
% 4.85/1.44 % (3445956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.85/1.44 % (3445956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.44 % (3445956)CaDiCaL version: 2.1.3
% 4.85/1.44 % (3445956)Termination reason: Instruction limit
% 4.85/1.44 % (3445956)Termination phase: Saturation
% 4.85/1.44 % (3445956)Time elapsed: 0.093 s
% 4.85/1.44 % (3445956)Peak memory usage: 91 MB
% 4.85/1.44 % (3445956)Instructions burned: 158 (million)
% 4.85/1.44 % (3445958)Instruction limit reached!
% 4.85/1.44 % (3445958)------------------------------
% 4.85/1.44 % (3445958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.85/1.44 % (3445958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.44 % (3445958)CaDiCaL version: 2.1.3
% 4.85/1.44 % (3445958)Termination reason: Instruction limit
% 4.85/1.44 % (3445958)Termination phase: Saturation
% 4.85/1.44 % (3445958)Time elapsed: 0.143 s
% 4.85/1.44 % (3445958)Peak memory usage: 94 MB
% 4.85/1.44 % (3445958)Instructions burned: 248 (million)
% 4.85/1.44 % (3445955)Instruction limit reached!
% 4.85/1.44 % (3445955)------------------------------
% 4.85/1.44 % (3445955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.85/1.44 % (3445955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.44 % (3445955)CaDiCaL version: 2.1.3
% 4.85/1.44 % (3445955)Termination reason: Instruction limit
% 4.85/1.44 % (3445955)Termination phase: Saturation
% 4.85/1.44 % (3445955)Time elapsed: 0.192 s
% 4.85/1.44 % (3445955)Peak memory usage: 93 MB
% 4.85/1.44 % (3445955)Instructions burned: 286 (million)
% 4.85/1.44 % (3445957)Instruction limit reached!
% 4.85/1.44 % (3445957)------------------------------
% 4.85/1.44 % (3445957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.85/1.44 % (3445957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.44 % (3445957)CaDiCaL version: 2.1.3
% 4.85/1.44 % (3445957)Termination reason: Instruction limit
% 4.85/1.44 % (3445957)Termination phase: Saturation
% 4.85/1.44 % (3445957)Time elapsed: 0.208 s
% 4.85/1.44 % (3445957)Peak memory usage: 92 MB
% 4.85/1.44 % (3445957)Instructions burned: 325 (million)
% 4.85/1.44 % (3445963)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=782786761:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 4.85/1.44 % (3445941)First to succeed.
% 4.85/1.44 % (3445941)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3445936"
% 4.85/1.44 % (3445963)Refutation not found, incomplete strategy
% 4.85/1.44 % (3445963)------------------------------
% 4.85/1.44 % (3445963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.85/1.44 % (3445963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.44 % (3445963)CaDiCaL version: 2.1.3
% 4.85/1.44 % (3445963)Termination reason: Refutation not found, incomplete strategy
% 4.85/1.44 % (3445963)Time elapsed: 0.015 s
% 4.85/1.44 % (3445963)Peak memory usage: 89 MB
% 4.85/1.44 % (3445963)Instructions burned: 23 (million)
% 4.85/1.44 % (3445964)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3582267794:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 4.85/1.44 % (3445965)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1608452832:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 4.85/1.44 % (3445967)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=952739195:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 4.85/1.44 % (3445941)Refutation found. Thanks to Tanya!
% 4.85/1.44 % SZS status Theorem for theBenchmark
% 4.85/1.44 % SZS output start Proof for theBenchmark
% See solution above
% 6.05/1.64 % (3445941)------------------------------
% 6.05/1.64 % (3445941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.05/1.64 % (3445941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.05/1.64 % (3445941)CaDiCaL version: 2.1.3
% 6.05/1.64 % (3445941)Termination reason: Refutation
% 6.05/1.64 % (3445941)Time elapsed: 0.493 s
% 6.05/1.64 % (3445941)Peak memory usage: 137 MB
% 6.05/1.64 % (3445941)Instructions burned: 1279 (million)
% 6.05/1.64 % (3445941)------------------------------
% 6.05/1.64 % (3445941)------------------------------
% 6.05/1.64 % (3445936)Success in time 0.769 s
% 6.05/1.64 % Vampire exiting
%------------------------------------------------------------------------------