%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : PUZ034-1.004 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n009.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 12:31:18 PM UTC 2026
% Result : Unsatisfiable 19.62s 3.63s
% Output : Refutation 20.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 53
% Syntax : Number of formulae : 360 ( 65 unt; 35 def)
% Number of atoms : 1105 ( 0 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 1337 ( 592 ~; 710 |; 0 &)
% ( 35 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 5 avg)
% Maximal term depth : 11 ( 3 avg)
% Number of predicates : 45 ( 44 usr; 36 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 326 ( 0 sgn 326 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1] :
( ~ sum(X0,s(n0),X3)
| ~ less(X0,X1)
| range(X0,X1,cons(X0,X2))
| ~ range(X3,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',make_list_of_numbers1) ).
fof(f2,axiom,
! [X0] : range(X0,X0,cons(X0,empty_list)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',make_list_of_numbers2) ).
fof(f3,axiom,
! [X0] : less(n0,s(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less1) ).
fof(f4,axiom,
! [X0,X1] :
( less(s(X0),s(X1))
| ~ less(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',less2) ).
fof(f5,axiom,
! [X0] : sum(X0,n0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',add_0) ).
fof(f6,axiom,
! [X2,X0,X1] :
( sum(X0,s(X1),s(X2))
| ~ sum(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',add) ).
fof(f7,axiom,
! [X0,X1] : select(X0,cons(X0,X1),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',select1) ).
fof(f8,axiom,
! [X2,X3,X0,X1] :
( select(X0,cons(X1,X2),cons(X1,X3))
| ~ select(X0,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',select2) ).
fof(f9,axiom,
! [X0] : ~ same(s(X0),n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',same_definition1) ).
fof(f10,axiom,
! [X0] : ~ same(n0,s(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',same_definition2) ).
fof(f11,axiom,
! [X0,X1] :
( ~ same(s(X0),s(X1))
| same(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',same_definition3) ).
fof(f12,axiom,
! [X0,X1] :
( diagonal_attack(X0,s(n0),X1)
| ~ attack(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',attack) ).
fof(f13,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ diagonal_attack(X0,X1,cons(X2,X3))
| ~ sum(X4,X1,X2)
| same(X4,X0)
| ~ sum(X2,X1,X5)
| same(X5,X0)
| ~ sum(X1,s(n0),X6)
| diagonal_attack(X0,X6,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',check_diagonals1) ).
fof(f14,axiom,
! [X0,X1] : ~ diagonal_attack(X0,X1,empty_list),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',check_diagonals2) ).
fof(f15,axiom,
! [X2,X3,X0,X1,X4] :
( ~ do_queens(X4,cons(X3,X1),X2)
| ~ select(X3,X0,X4)
| attack(X3,X1)
| do_queens(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',place_a_queen1) ).
fof(f16,axiom,
! [X0] : do_queens(empty_list,X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',place_a_queen2) ).
fof(f17,axiom,
! [X2,X3,X0,X1,X4] :
( ~ sum(X0,s(n0),X2)
| queens(X0,X1)
| ~ sum(X0,X0,X3)
| ~ range(X2,X3,X4)
| ~ do_queens(X4,empty_list,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',set_up_queens) ).
fof(f18,negated_conjecture,
! [X0] : ~ queens(s(s(s(s(n0)))),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',place_queens) ).
fof(f19,plain,
! [X2,X3,X0,X1,X4] :
( ~ range(s(X3),X2,X4)
| ~ sum(X0,X0,X2)
| queens(X0,X1)
| ~ do_queens(X4,empty_list,X1)
| ~ sum(X0,n0,X3) ),
inference(resolution,[],[f17,f6]) ).
fof(f21,plain,
! [X2,X3,X0,X1] :
( ~ range(s(X3),X1,X2)
| range(X0,X1,cons(X0,X2))
| ~ less(X0,X1)
| ~ sum(X0,n0,X3) ),
inference(resolution,[],[f1,f6]) ).
fof(f22,plain,
! [X0,X1] :
( range(X0,s(X1),cons(X0,cons(s(X1),empty_list)))
| ~ less(X0,s(X1))
| ~ sum(X0,n0,X1) ),
inference(resolution,[],[f21,f2]) ).
fof(f23,plain,
! [X2,X0,X1] :
( range(X2,s(X1),cons(X2,cons(s(X0),cons(s(X1),empty_list))))
| ~ sum(s(X0),n0,X1)
| ~ less(s(X0),s(X1))
| ~ less(X2,s(X1))
| ~ sum(X2,n0,X0) ),
inference(resolution,[],[f22,f21]) ).
fof(f25,plain,
! [X2,X0,X1] :
( do_queens(X1,X2,cons(X0,X2))
| attack(X0,X2)
| ~ select(X0,X1,empty_list) ),
inference(resolution,[],[f15,f16]) ).
fof(f28,plain,
! [X2,X3,X0,X1,X4] :
( ~ select(X1,X4,X3)
| ~ select(X0,X3,empty_list)
| attack(X0,cons(X1,X2))
| attack(X1,X2)
| do_queens(X4,X2,cons(X0,cons(X1,X2))) ),
inference(resolution,[],[f25,f15]) ).
fof(f31,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ sum(s(n0),s(n0),X4)
| same(X0,X2)
| ~ sum(X1,s(n0),X3)
| same(X3,X2)
| ~ sum(X0,s(n0),X1)
| diagonal_attack(X2,X4,X5)
| ~ attack(X2,cons(X1,X5)) ),
inference(resolution,[],[f13,f12]) ).
fof(f33,plain,
! [X2,X3,X0,X1] :
( do_queens(cons(X2,X1),X3,cons(X0,cons(X2,X3)))
| attack(X0,cons(X2,X3))
| attack(X2,X3)
| ~ select(X0,X1,empty_list) ),
inference(resolution,[],[f28,f7]) ).
fof(f36,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ select(X2,X5,cons(X1,X4))
| attack(X1,cons(X2,X3))
| ~ select(X0,X4,empty_list)
| attack(X0,cons(X1,cons(X2,X3)))
| attack(X2,X3)
| do_queens(X5,X3,cons(X0,cons(X1,cons(X2,X3)))) ),
inference(resolution,[],[f33,f15]) ).
fof(f37,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ attack(X1,cons(X2,X5))
| ~ sum(X2,s(n0),X3)
| same(X3,X1)
| ~ sum(X0,s(n0),X2)
| diagonal_attack(X1,s(X4),X5)
| same(X0,X1)
| ~ sum(s(n0),n0,X4) ),
inference(resolution,[],[f31,f6]) ).
fof(f42,plain,
! [X0] : ~ attack(X0,empty_list),
inference(resolution,[],[f14,f12]) ).
fof(f43,plain,
! [X2,X3,X0,X1] :
( range(X3,s(X1),cons(X3,cons(s(X2),cons(s(X0),cons(s(X1),empty_list)))))
| ~ less(s(X0),s(X1))
| ~ less(s(X2),s(X1))
| ~ sum(s(X2),n0,X0)
| ~ sum(s(X0),n0,X1)
| ~ less(X3,s(X1))
| ~ sum(X3,n0,X2) ),
inference(resolution,[],[f23,f21]) ).
fof(f61,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ select(X3,X4,empty_list)
| attack(X0,cons(X1,X2))
| attack(X3,cons(X0,cons(X1,X2)))
| attack(X1,X2)
| do_queens(cons(X0,X5),X2,cons(X3,cons(X0,cons(X1,X2))))
| ~ select(X1,X5,X4) ),
inference(resolution,[],[f36,f8]) ).
fof(f68,plain,
! [X2,X3,X0,X1,X4] :
( do_queens(cons(X0,X4),X2,cons(X3,cons(X0,cons(X1,X2))))
| attack(X3,cons(X0,cons(X1,X2)))
| attack(X1,X2)
| attack(X0,cons(X1,X2))
| ~ select(X1,X4,cons(X3,empty_list)) ),
inference(resolution,[],[f61,f7]) ).
fof(f72,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ select(X3,X6,cons(X1,X5))
| attack(X2,cons(X3,X4))
| attack(X1,cons(X2,cons(X3,X4)))
| ~ select(X2,X5,cons(X0,empty_list))
| attack(X0,cons(X1,cons(X2,cons(X3,X4))))
| attack(X3,X4)
| do_queens(X6,X4,cons(X0,cons(X1,cons(X2,cons(X3,X4))))) ),
inference(resolution,[],[f68,f15]) ).
fof(f91,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ do_queens(cons(s(X3),cons(s(X2),cons(s(X0),cons(s(X1),empty_list)))),empty_list,X5)
| ~ less(s(X2),s(X1))
| ~ sum(s(X2),n0,X0)
| ~ sum(s(X0),n0,X1)
| ~ less(s(X3),s(X1))
| ~ sum(s(X3),n0,X2)
| ~ sum(X4,X4,s(X1))
| queens(X4,X5)
| ~ less(s(X0),s(X1))
| ~ sum(X4,n0,X3) ),
inference(resolution,[],[f43,f19]) ).
fof(f126,definition,
( spl0_3
<=> less(s(n0),s(s(n0))) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f127,plain,
( less(s(n0),s(s(n0)))
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f126]) ).
fof(f128,plain,
( ~ less(s(n0),s(s(n0)))
| spl0_3 ),
inference(avatar_component_clause,[],[f126]) ).
fof(f163,plain,
( ~ less(n0,s(n0))
| spl0_3 ),
inference(resolution,[],[f128,f4]) ).
fof(f164,plain,
( $false
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f163,f3]) ).
fof(f165,plain,
spl0_3,
inference(avatar_contradiction_clause,[],[f164]) ).
fof(f188,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ select(X0,X4,cons(X5,empty_list))
| attack(X3,cons(X0,cons(X1,X2)))
| attack(X0,cons(X1,X2))
| attack(X5,cons(X3,cons(X0,cons(X1,X2))))
| attack(X1,X2)
| do_queens(cons(X3,X6),X2,cons(X5,cons(X3,cons(X0,cons(X1,X2)))))
| ~ select(X1,X6,X4) ),
inference(resolution,[],[f72,f8]) ).
fof(f222,definition,
( spl0_8
<=> ! [X2] : ~ sum(s(n0),n0,X2) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f223,plain,
( ! [X2] : ~ sum(s(n0),n0,X2)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f222]) ).
fof(f283,definition,
( spl0_13
<=> less(s(s(s(s(s(n0))))),s(s(s(s(s(s(n0))))))) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f285,plain,
( ~ less(s(s(s(s(s(n0))))),s(s(s(s(s(s(n0)))))))
| spl0_13 ),
inference(avatar_component_clause,[],[f283]) ).
fof(f328,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ select(X2,X5,cons(X4,X6))
| attack(X1,cons(X2,X3))
| attack(X4,cons(X0,cons(X1,cons(X2,X3))))
| attack(X2,X3)
| do_queens(cons(X0,X5),X3,cons(X4,cons(X0,cons(X1,cons(X2,X3)))))
| attack(X0,cons(X1,cons(X2,X3)))
| ~ select(X1,X6,empty_list) ),
inference(resolution,[],[f188,f8]) ).
fof(f342,plain,
! [X2,X3,X0,X1,X4,X5] :
( do_queens(cons(X4,cons(X1,cons(X3,X5))),X2,cons(X3,cons(X4,cons(X0,cons(X1,X2)))))
| attack(X3,cons(X4,cons(X0,cons(X1,X2))))
| attack(X1,X2)
| attack(X0,cons(X1,X2))
| attack(X4,cons(X0,cons(X1,X2)))
| ~ select(X0,X5,empty_list) ),
inference(resolution,[],[f328,f7]) ).
fof(f344,plain,
! [X2,X3,X0,X1,X4,X5] :
( attack(s(X0),cons(s(X1),cons(X2,cons(s(X3),empty_list))))
| attack(s(X3),empty_list)
| attack(X2,cons(s(X3),empty_list))
| attack(s(X1),cons(X2,cons(s(X3),empty_list)))
| ~ select(X2,cons(s(X4),empty_list),empty_list)
| ~ less(s(X3),s(X4))
| ~ sum(s(X3),n0,X0)
| ~ sum(s(X0),n0,X4)
| ~ less(s(X1),s(X4))
| ~ sum(s(X1),n0,X3)
| ~ sum(X5,X5,s(X4))
| queens(X5,cons(s(X0),cons(s(X1),cons(X2,cons(s(X3),empty_list)))))
| ~ less(s(X0),s(X4))
| ~ sum(X5,n0,X1) ),
inference(resolution,[],[f342,f91]) ).
fof(f348,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ select(X2,cons(s(X4),empty_list),empty_list)
| attack(X2,cons(s(X3),empty_list))
| attack(s(X1),cons(X2,cons(s(X3),empty_list)))
| attack(s(X0),cons(s(X1),cons(X2,cons(s(X3),empty_list))))
| ~ less(s(X3),s(X4))
| ~ sum(s(X3),n0,X0)
| ~ sum(s(X0),n0,X4)
| ~ less(s(X1),s(X4))
| ~ sum(s(X1),n0,X3)
| ~ sum(X5,X5,s(X4))
| queens(X5,cons(s(X0),cons(s(X1),cons(X2,cons(s(X3),empty_list)))))
| ~ less(s(X0),s(X4))
| ~ sum(X5,n0,X1) ),
inference(forward_subsumption_resolution,[],[f344,f42]) ).
fof(f418,definition,
( spl0_14
<=> less(s(s(n0)),s(s(s(s(n0))))) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f419,plain,
( less(s(s(n0)),s(s(s(s(n0)))))
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f418]) ).
fof(f420,plain,
( ~ less(s(s(n0)),s(s(s(s(n0)))))
| spl0_14 ),
inference(avatar_component_clause,[],[f418]) ).
fof(f426,definition,
( spl0_16
<=> less(s(s(n0)),s(s(s(n0)))) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f427,plain,
( less(s(s(n0)),s(s(s(n0))))
| ~ spl0_16 ),
inference(avatar_component_clause,[],[f426]) ).
fof(f428,plain,
( ~ less(s(s(n0)),s(s(s(n0))))
| spl0_16 ),
inference(avatar_component_clause,[],[f426]) ).
fof(f442,plain,
( ~ less(s(n0),s(s(s(n0))))
| spl0_14 ),
inference(resolution,[],[f420,f4]) ).
fof(f443,plain,
( ~ less(n0,s(s(n0)))
| spl0_14 ),
inference(resolution,[],[f442,f4]) ).
fof(f444,plain,
( $false
| spl0_14 ),
inference(forward_subsumption_resolution,[],[f443,f3]) ).
fof(f445,plain,
spl0_14,
inference(avatar_contradiction_clause,[],[f444]) ).
fof(f446,plain,
( ~ less(s(n0),s(s(n0)))
| spl0_16 ),
inference(resolution,[],[f428,f4]) ).
fof(f447,plain,
( $false
| ~ spl0_3
| spl0_16 ),
inference(forward_subsumption_resolution,[],[f446,f127]) ).
fof(f448,plain,
( ~ spl0_3
| spl0_16 ),
inference(avatar_contradiction_clause,[],[f447]) ).
fof(f487,plain,
( $false
| ~ spl0_8 ),
inference(resolution,[],[f223,f5]) ).
fof(f488,plain,
~ spl0_8,
inference(avatar_contradiction_clause,[],[f487]) ).
fof(f628,definition,
( spl0_28
<=> less(s(s(s(s(n0)))),s(s(s(s(s(s(n0))))))) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f629,plain,
( less(s(s(s(s(n0)))),s(s(s(s(s(s(n0)))))))
| ~ spl0_28 ),
inference(avatar_component_clause,[],[f628]) ).
fof(f630,plain,
( ~ less(s(s(s(s(n0)))),s(s(s(s(s(s(n0)))))))
| spl0_28 ),
inference(avatar_component_clause,[],[f628]) ).
fof(f649,definition,
( spl0_34
<=> less(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(n0)))))))) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f651,plain,
( ~ less(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(n0))))))))
| spl0_34 ),
inference(avatar_component_clause,[],[f649]) ).
fof(f653,plain,
( ~ less(s(s(s(n0))),s(s(s(s(s(n0))))))
| spl0_28 ),
inference(resolution,[],[f630,f4]) ).
fof(f654,plain,
( ~ less(s(s(n0)),s(s(s(s(n0)))))
| spl0_28 ),
inference(resolution,[],[f653,f4]) ).
fof(f655,plain,
( $false
| ~ spl0_14
| spl0_28 ),
inference(forward_subsumption_resolution,[],[f654,f419]) ).
fof(f656,plain,
( ~ spl0_14
| spl0_28 ),
inference(avatar_contradiction_clause,[],[f655]) ).
fof(f884,plain,
! [X2,X3,X0,X1,X4] :
( ~ sum(s(X3),n0,X0)
| attack(s(X2),cons(s(X0),cons(s(X1),empty_list)))
| attack(s(X3),cons(s(X2),cons(s(X0),cons(s(X1),empty_list))))
| ~ less(s(X1),s(X0))
| ~ sum(s(X1),n0,X3)
| attack(s(X0),cons(s(X1),empty_list))
| ~ less(s(X2),s(X0))
| ~ sum(s(X2),n0,X1)
| ~ sum(X4,X4,s(X0))
| queens(X4,cons(s(X3),cons(s(X2),cons(s(X0),cons(s(X1),empty_list)))))
| ~ less(s(X3),s(X0))
| ~ sum(X4,n0,X2) ),
inference(resolution,[],[f348,f7]) ).
fof(f885,plain,
! [X2,X3,X0,X1] :
( ~ sum(X3,X3,s(s(X1)))
| attack(s(X1),cons(s(X0),cons(s(s(X1)),cons(s(X2),empty_list))))
| ~ less(s(X2),s(s(X1)))
| ~ sum(s(X2),n0,X1)
| attack(s(s(X1)),cons(s(X2),empty_list))
| ~ less(s(X0),s(s(X1)))
| ~ sum(s(X0),n0,X2)
| attack(s(X0),cons(s(s(X1)),cons(s(X2),empty_list)))
| queens(X3,cons(s(X1),cons(s(X0),cons(s(s(X1)),cons(s(X2),empty_list)))))
| ~ less(s(X1),s(s(X1)))
| ~ sum(X3,n0,X0) ),
inference(resolution,[],[f884,f5]) ).
fof(f886,plain,
! [X2,X3,X0,X1] :
( ~ sum(s(X3),X3,s(X0))
| ~ less(s(X2),s(s(X0)))
| ~ sum(s(X2),n0,X0)
| attack(s(s(X0)),cons(s(X2),empty_list))
| ~ less(s(X1),s(s(X0)))
| ~ sum(s(X1),n0,X2)
| attack(s(X1),cons(s(s(X0)),cons(s(X2),empty_list)))
| queens(s(X3),cons(s(X0),cons(s(X1),cons(s(s(X0)),cons(s(X2),empty_list)))))
| ~ less(s(X0),s(s(X0)))
| ~ sum(s(X3),n0,X1)
| attack(s(X0),cons(s(X1),cons(s(s(X0)),cons(s(X2),empty_list)))) ),
inference(resolution,[],[f885,f6]) ).
fof(f887,plain,
! [X2,X3,X0,X1] :
( ~ sum(s(s(X3)),n0,X2)
| ~ sum(s(X0),n0,X1)
| attack(s(s(X1)),cons(s(X0),empty_list))
| ~ less(s(X2),s(s(X1)))
| ~ sum(s(X2),n0,X0)
| attack(s(X2),cons(s(s(X1)),cons(s(X0),empty_list)))
| queens(s(s(X3)),cons(s(X1),cons(s(X2),cons(s(s(X1)),cons(s(X0),empty_list)))))
| ~ less(s(X1),s(s(X1)))
| ~ less(s(X0),s(s(X1)))
| attack(s(X1),cons(s(X2),cons(s(s(X1)),cons(s(X0),empty_list))))
| ~ sum(s(s(X3)),X3,X1) ),
inference(resolution,[],[f886,f6]) ).
fof(f890,plain,
! [X2,X0,X1] :
( queens(s(s(X2)),cons(s(X1),cons(s(s(s(X2))),cons(s(s(X1)),cons(s(X0),empty_list)))))
| attack(s(s(X1)),cons(s(X0),empty_list))
| ~ less(s(s(s(X2))),s(s(X1)))
| ~ sum(s(s(s(X2))),n0,X0)
| attack(s(s(s(X2))),cons(s(s(X1)),cons(s(X0),empty_list)))
| ~ sum(s(X0),n0,X1)
| ~ less(s(X1),s(s(X1)))
| ~ less(s(X0),s(s(X1)))
| attack(s(X1),cons(s(s(s(X2))),cons(s(s(X1)),cons(s(X0),empty_list))))
| ~ sum(s(s(X2)),X2,X1) ),
inference(resolution,[],[f887,f5]) ).
fof(f891,plain,
! [X0,X1] :
( attack(s(X0),cons(s(s(s(s(s(n0))))),cons(s(s(X0)),cons(s(X1),empty_list))))
| ~ less(s(s(s(s(s(n0))))),s(s(X0)))
| ~ sum(s(s(s(s(s(n0))))),n0,X1)
| attack(s(s(s(s(s(n0))))),cons(s(s(X0)),cons(s(X1),empty_list)))
| ~ sum(s(X1),n0,X0)
| ~ less(s(X0),s(s(X0)))
| ~ less(s(X1),s(s(X0)))
| attack(s(s(X0)),cons(s(X1),empty_list))
| ~ sum(s(s(s(s(n0)))),s(s(n0)),X0) ),
inference(resolution,[],[f890,f18]) ).
fof(f892,plain,
! [X2,X3,X0,X1,X4] :
( ~ sum(s(s(s(s(s(n0))))),s(n0),X2)
| ~ sum(s(s(s(s(s(n0))))),n0,X1)
| attack(s(s(s(s(s(n0))))),cons(s(s(X0)),cons(s(X1),empty_list)))
| ~ sum(s(X1),n0,X0)
| ~ less(s(X0),s(s(X0)))
| ~ less(s(X1),s(s(X0)))
| attack(s(s(X0)),cons(s(X1),empty_list))
| ~ sum(s(s(s(s(n0)))),s(s(n0)),X0)
| ~ less(s(s(s(s(s(n0))))),s(s(X0)))
| same(X2,s(X0))
| ~ sum(X3,s(n0),s(s(s(s(s(n0))))))
| diagonal_attack(s(X0),s(X4),cons(s(s(X0)),cons(s(X1),empty_list)))
| same(X3,s(X0))
| ~ sum(s(n0),n0,X4) ),
inference(resolution,[],[f891,f37]) ).
fof(f893,plain,
! [X2,X3,X0,X1,X4] :
( ~ sum(s(s(s(s(n0)))),s(s(n0)),X1)
| attack(s(s(s(s(s(n0))))),cons(s(s(X1)),cons(s(X0),empty_list)))
| ~ sum(s(X0),n0,X1)
| ~ less(s(X1),s(s(X1)))
| ~ less(s(X0),s(s(X1)))
| attack(s(s(X1)),cons(s(X0),empty_list))
| ~ sum(s(s(s(s(s(n0))))),n0,X0)
| ~ less(s(s(s(s(s(n0))))),s(s(X1)))
| same(s(X2),s(X1))
| ~ sum(X3,s(n0),s(s(s(s(s(n0))))))
| diagonal_attack(s(X1),s(X4),cons(s(s(X1)),cons(s(X0),empty_list)))
| same(X3,s(X1))
| ~ sum(s(n0),n0,X4)
| ~ sum(s(s(s(s(s(n0))))),n0,X2) ),
inference(resolution,[],[f892,f6]) ).
fof(f894,plain,
! [X2,X3,X0,X1,X4] :
( ~ less(s(s(s(s(s(n0))))),s(s(s(X0))))
| ~ sum(s(X1),n0,s(X0))
| ~ less(s(s(X0)),s(s(s(X0))))
| ~ less(s(X1),s(s(s(X0))))
| attack(s(s(s(X0))),cons(s(X1),empty_list))
| ~ sum(s(s(s(s(s(n0))))),n0,X1)
| attack(s(s(s(s(s(n0))))),cons(s(s(s(X0))),cons(s(X1),empty_list)))
| same(s(X2),s(s(X0)))
| ~ sum(X3,s(n0),s(s(s(s(s(n0))))))
| diagonal_attack(s(s(X0)),s(X4),cons(s(s(s(X0))),cons(s(X1),empty_list)))
| same(X3,s(s(X0)))
| ~ sum(s(n0),n0,X4)
| ~ sum(s(s(s(s(s(n0))))),n0,X2)
| ~ sum(s(s(s(s(n0)))),s(n0),X0) ),
inference(resolution,[],[f893,f6]) ).
fof(f1068,plain,
! [X2,X3,X0,X1,X4] :
( ~ sum(X3,s(n0),s(s(s(s(s(n0))))))
| ~ less(s(s(X1)),s(s(s(X1))))
| ~ less(s(X0),s(s(s(X1))))
| attack(s(s(s(X1))),cons(s(X0),empty_list))
| ~ sum(s(s(s(s(s(n0))))),n0,X0)
| attack(s(s(s(s(s(n0))))),cons(s(s(s(X1))),cons(s(X0),empty_list)))
| same(s(X2),s(s(X1)))
| ~ sum(s(X0),n0,s(X1))
| diagonal_attack(s(s(X1)),s(X4),cons(s(s(s(X1))),cons(s(X0),empty_list)))
| same(X3,s(s(X1)))
| ~ sum(s(n0),n0,X4)
| ~ sum(s(s(s(s(s(n0))))),n0,X2)
| ~ sum(s(s(s(s(n0)))),s(n0),X1)
| ~ less(s(s(s(s(n0)))),s(s(X1))) ),
inference(resolution,[],[f894,f4]) ).
fof(f1069,plain,
! [X2,X3,X0,X1,X4] :
( ~ sum(s(s(s(s(s(n0))))),n0,X2)
| ~ less(s(X1),s(s(s(X0))))
| attack(s(s(s(X0))),cons(s(X1),empty_list))
| ~ sum(s(s(s(s(s(n0))))),n0,X1)
| attack(s(s(s(s(s(n0))))),cons(s(s(s(X0))),cons(s(X1),empty_list)))
| same(s(X2),s(s(X0)))
| ~ sum(s(X1),n0,s(X0))
| diagonal_attack(s(s(X0)),s(X3),cons(s(s(s(X0))),cons(s(X1),empty_list)))
| same(X4,s(s(X0)))
| ~ sum(s(n0),n0,X3)
| ~ less(s(s(X0)),s(s(s(X0))))
| ~ sum(s(s(s(s(n0)))),s(n0),X0)
| ~ less(s(s(s(s(n0)))),s(s(X0)))
| ~ sum(X4,n0,s(s(s(s(n0))))) ),
inference(resolution,[],[f1068,f6]) ).
fof(f1070,plain,
! [X2,X3,X0,X1] :
( ~ sum(s(s(s(s(s(n0))))),n0,X0)
| attack(s(s(s(X1))),cons(s(X0),empty_list))
| ~ less(s(X0),s(s(s(X1))))
| attack(s(s(s(s(s(n0))))),cons(s(s(s(X1))),cons(s(X0),empty_list)))
| same(s(s(s(s(s(s(n0)))))),s(s(X1)))
| ~ sum(s(X0),n0,s(X1))
| diagonal_attack(s(s(X1)),s(X2),cons(s(s(s(X1))),cons(s(X0),empty_list)))
| same(X3,s(s(X1)))
| ~ sum(s(n0),n0,X2)
| ~ less(s(s(X1)),s(s(s(X1))))
| ~ sum(s(s(s(s(n0)))),s(n0),X1)
| ~ less(s(s(s(s(n0)))),s(s(X1)))
| ~ sum(X3,n0,s(s(s(s(n0))))) ),
inference(resolution,[],[f1069,f5]) ).
fof(f1071,plain,
! [X2,X0,X1] :
( ~ less(s(s(s(s(s(s(n0)))))),s(s(s(X0))))
| attack(s(s(s(X0))),cons(s(s(s(s(s(s(n0)))))),empty_list))
| attack(s(s(s(s(s(n0))))),cons(s(s(s(X0))),cons(s(s(s(s(s(s(n0)))))),empty_list)))
| same(s(s(s(s(s(s(n0)))))),s(s(X0)))
| ~ sum(s(s(s(s(s(s(n0)))))),n0,s(X0))
| diagonal_attack(s(s(X0)),s(X1),cons(s(s(s(X0))),cons(s(s(s(s(s(s(n0)))))),empty_list)))
| same(X2,s(s(X0)))
| ~ sum(s(n0),n0,X1)
| ~ less(s(s(X0)),s(s(s(X0))))
| ~ sum(s(s(s(s(n0)))),s(n0),X0)
| ~ less(s(s(s(s(n0)))),s(s(X0)))
| ~ sum(X2,n0,s(s(s(s(n0))))) ),
inference(resolution,[],[f1070,f5]) ).
fof(f1072,plain,
! [X2,X0,X1] :
( ~ sum(s(s(s(s(s(s(n0)))))),n0,s(X0))
| attack(s(s(s(s(s(n0))))),cons(s(s(s(X0))),cons(s(s(s(s(s(s(n0)))))),empty_list)))
| same(s(s(s(s(s(s(n0)))))),s(s(X0)))
| attack(s(s(s(X0))),cons(s(s(s(s(s(s(n0)))))),empty_list))
| diagonal_attack(s(s(X0)),s(X1),cons(s(s(s(X0))),cons(s(s(s(s(s(s(n0)))))),empty_list)))
| same(X2,s(s(X0)))
| ~ sum(s(n0),n0,X1)
| ~ less(s(s(X0)),s(s(s(X0))))
| ~ sum(s(s(s(s(n0)))),s(n0),X0)
| ~ less(s(s(s(s(n0)))),s(s(X0)))
| ~ sum(X2,n0,s(s(s(s(n0)))))
| ~ less(s(s(s(s(s(n0))))),s(s(X0))) ),
inference(resolution,[],[f1071,f4]) ).
fof(f1092,plain,
! [X0,X1] :
( attack(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list)))
| same(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(n0))))))))
| attack(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list))
| diagonal_attack(s(s(s(s(s(s(s(n0))))))),s(X0),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list)))
| same(X1,s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(n0),n0,X0)
| ~ less(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(n0)))),s(n0),s(s(s(s(s(n0))))))
| ~ less(s(s(s(s(n0)))),s(s(s(s(s(s(s(n0))))))))
| ~ sum(X1,n0,s(s(s(s(n0)))))
| ~ less(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(n0)))))))) ),
inference(resolution,[],[f1072,f5]) ).
fof(f1094,definition,
( spl0_46
<=> less(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(n0)))))))) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f1096,plain,
( ~ less(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(n0))))))))
| spl0_46 ),
inference(avatar_component_clause,[],[f1094]) ).
fof(f1098,definition,
( spl0_47
<=> less(s(s(s(s(n0)))),s(s(s(s(s(s(s(n0)))))))) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f1100,plain,
( ~ less(s(s(s(s(n0)))),s(s(s(s(s(s(s(n0))))))))
| spl0_47 ),
inference(avatar_component_clause,[],[f1098]) ).
fof(f1102,definition,
( spl0_48
<=> sum(s(s(s(s(n0)))),s(n0),s(s(s(s(s(n0)))))) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f1103,plain,
( sum(s(s(s(s(n0)))),s(n0),s(s(s(s(s(n0))))))
| ~ spl0_48 ),
inference(avatar_component_clause,[],[f1102]) ).
fof(f1104,plain,
( ~ sum(s(s(s(s(n0)))),s(n0),s(s(s(s(s(n0))))))
| spl0_48 ),
inference(avatar_component_clause,[],[f1102]) ).
fof(f1106,definition,
( spl0_49
<=> less(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(s(n0))))))))) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f1108,plain,
( ~ less(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(s(n0)))))))))
| spl0_49 ),
inference(avatar_component_clause,[],[f1106]) ).
fof(f1110,definition,
( spl0_50
<=> ! [X1] :
( same(X1,s(s(s(s(s(s(s(n0))))))))
| ~ sum(X1,n0,s(s(s(s(n0))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f1111,plain,
( ! [X1] :
( same(X1,s(s(s(s(s(s(s(n0))))))))
| ~ sum(X1,n0,s(s(s(s(n0))))) )
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f1110]) ).
fof(f1113,definition,
( spl0_51
<=> ! [X0] :
( diagonal_attack(s(s(s(s(s(s(s(n0))))))),s(X0),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list)))
| ~ sum(s(n0),n0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f1114,plain,
( ! [X0] :
( diagonal_attack(s(s(s(s(s(s(s(n0))))))),s(X0),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list)))
| ~ sum(s(n0),n0,X0) )
| ~ spl0_51 ),
inference(avatar_component_clause,[],[f1113]) ).
fof(f1116,definition,
( spl0_52
<=> attack(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list)) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f1118,plain,
( attack(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list))
| ~ spl0_52 ),
inference(avatar_component_clause,[],[f1116]) ).
fof(f1120,definition,
( spl0_53
<=> same(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(n0)))))))) ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f1121,plain,
( ~ same(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(n0))))))))
| spl0_53 ),
inference(avatar_component_clause,[],[f1120]) ).
fof(f1122,plain,
( same(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(n0))))))))
| ~ spl0_53 ),
inference(avatar_component_clause,[],[f1120]) ).
fof(f1124,definition,
( spl0_54
<=> attack(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list))) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f1126,plain,
( attack(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list)))
| ~ spl0_54 ),
inference(avatar_component_clause,[],[f1124]) ).
fof(f1127,plain,
( ~ spl0_46
| ~ spl0_47
| ~ spl0_48
| ~ spl0_49
| spl0_50
| spl0_51
| spl0_52
| spl0_53
| spl0_54 ),
inference(avatar_split_clause,[],[f1092,f1124,f1120,f1116,f1113,f1110,f1106,f1102,f1098,f1094]) ).
fof(f1128,plain,
( ~ less(s(s(s(s(n0)))),s(s(s(s(s(s(n0)))))))
| spl0_46 ),
inference(resolution,[],[f1096,f4]) ).
fof(f1129,plain,
( $false
| ~ spl0_28
| spl0_46 ),
inference(forward_subsumption_resolution,[],[f1128,f629]) ).
fof(f1130,plain,
( ~ spl0_28
| spl0_46 ),
inference(avatar_contradiction_clause,[],[f1129]) ).
fof(f1137,plain,
( ~ less(s(s(s(n0))),s(s(s(s(s(s(n0)))))))
| spl0_47 ),
inference(resolution,[],[f1100,f4]) ).
fof(f1138,plain,
( ~ less(s(s(n0)),s(s(s(s(s(n0))))))
| spl0_47 ),
inference(resolution,[],[f1137,f4]) ).
fof(f1139,plain,
( ~ less(s(n0),s(s(s(s(n0)))))
| spl0_47 ),
inference(resolution,[],[f1138,f4]) ).
fof(f1140,plain,
( ~ less(n0,s(s(s(n0))))
| spl0_47 ),
inference(resolution,[],[f1139,f4]) ).
fof(f1141,plain,
( $false
| spl0_47 ),
inference(forward_subsumption_resolution,[],[f1140,f3]) ).
fof(f1142,plain,
spl0_47,
inference(avatar_contradiction_clause,[],[f1141]) ).
fof(f1143,plain,
( ~ sum(s(s(s(s(n0)))),n0,s(s(s(s(n0)))))
| spl0_48 ),
inference(resolution,[],[f1104,f6]) ).
fof(f1144,plain,
( $false
| spl0_48 ),
inference(forward_subsumption_resolution,[],[f1143,f5]) ).
fof(f1145,plain,
spl0_48,
inference(avatar_contradiction_clause,[],[f1144]) ).
fof(f1146,plain,
( ~ less(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(n0))))))))
| spl0_49 ),
inference(resolution,[],[f1108,f4]) ).
fof(f1147,plain,
( ~ spl0_34
| spl0_49 ),
inference(avatar_split_clause,[],[f1146,f1106,f649]) ).
fof(f1148,plain,
( ~ less(s(s(s(s(s(n0))))),s(s(s(s(s(s(n0)))))))
| spl0_34 ),
inference(resolution,[],[f651,f4]) ).
fof(f1149,plain,
( ~ spl0_13
| spl0_34 ),
inference(avatar_split_clause,[],[f1148,f649,f283]) ).
fof(f1150,plain,
( ~ less(s(s(s(s(n0)))),s(s(s(s(s(n0))))))
| spl0_13 ),
inference(resolution,[],[f285,f4]) ).
fof(f1151,plain,
( ~ less(s(s(s(n0))),s(s(s(s(n0)))))
| spl0_13 ),
inference(resolution,[],[f1150,f4]) ).
fof(f1174,plain,
( ~ less(s(s(n0)),s(s(s(n0))))
| spl0_13 ),
inference(resolution,[],[f1151,f4]) ).
fof(f1175,plain,
( $false
| spl0_13
| ~ spl0_16 ),
inference(forward_subsumption_resolution,[],[f1174,f427]) ).
fof(f1176,plain,
( spl0_13
| ~ spl0_16 ),
inference(avatar_contradiction_clause,[],[f1175]) ).
fof(f1327,plain,
( ! [X0] :
( ~ sum(s(X0),n0,s(s(s(s(n0)))))
| same(X0,s(s(s(s(s(s(n0))))))) )
| ~ spl0_50 ),
inference(resolution,[],[f1111,f11]) ).
fof(f1573,definition,
( spl0_124
<=> ! [X1] :
( ~ sum(X1,s(n0),s(s(s(s(s(s(s(s(n0)))))))))
| same(X1,s(s(s(s(s(n0)))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition]) ).
fof(f1574,plain,
( ! [X1] :
( ~ sum(X1,s(n0),s(s(s(s(s(s(s(s(n0)))))))))
| same(X1,s(s(s(s(s(n0)))))) )
| ~ spl0_124 ),
inference(avatar_component_clause,[],[f1573]) ).
fof(f1576,definition,
( spl0_125
<=> ! [X0] :
( ~ sum(s(s(s(s(s(s(s(s(n0)))))))),s(n0),X0)
| same(X0,s(s(s(s(s(n0)))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_125])],[avatar_definition]) ).
fof(f1577,plain,
( ! [X0] :
( ~ sum(s(s(s(s(s(s(s(s(n0)))))))),s(n0),X0)
| same(X0,s(s(s(s(s(n0)))))) )
| ~ spl0_125 ),
inference(avatar_component_clause,[],[f1576]) ).
fof(f1598,plain,
( same(s(s(s(n0))),s(s(s(s(s(s(n0)))))))
| ~ spl0_50 ),
inference(resolution,[],[f1327,f5]) ).
fof(f1603,plain,
( same(s(s(n0)),s(s(s(s(s(n0))))))
| ~ spl0_50 ),
inference(resolution,[],[f1598,f11]) ).
fof(f1874,plain,
( same(s(n0),s(s(s(s(n0)))))
| ~ spl0_50 ),
inference(resolution,[],[f1603,f11]) ).
fof(f1875,plain,
( same(n0,s(s(s(n0))))
| ~ spl0_50 ),
inference(resolution,[],[f1874,f11]) ).
fof(f1876,plain,
( $false
| ~ spl0_50 ),
inference(forward_subsumption_resolution,[],[f1875,f10]) ).
fof(f1877,plain,
~ spl0_50,
inference(avatar_contradiction_clause,[],[f1876]) ).
fof(f1878,plain,
( ! [X2,X3,X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(n0)))))))),s(X0),X2)
| ~ sum(X1,s(X0),s(s(s(s(s(s(s(s(n0)))))))))
| same(X1,s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(n0),n0,X0)
| same(X2,s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(X0),s(n0),X3)
| diagonal_attack(s(s(s(s(s(s(s(n0))))))),X3,cons(s(s(s(s(s(s(n0)))))),empty_list)) )
| ~ spl0_51 ),
inference(resolution,[],[f1114,f13]) ).
fof(f1879,plain,
( ! [X2,X3,X0,X1] :
( ~ sum(X0,s(X1),s(s(s(s(s(s(s(s(n0)))))))))
| same(X0,s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(n0),n0,X1)
| same(s(X2),s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(X1),s(n0),X3)
| diagonal_attack(s(s(s(s(s(s(s(n0))))))),X3,cons(s(s(s(s(s(s(n0)))))),empty_list))
| ~ sum(s(s(s(s(s(s(s(s(n0)))))))),X1,X2) )
| ~ spl0_51 ),
inference(resolution,[],[f1878,f6]) ).
fof(f1880,plain,
( ! [X2,X3,X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(n0)))))))),X1,X2)
| ~ sum(s(n0),n0,X1)
| same(s(X2),s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(X1),s(n0),X3)
| diagonal_attack(s(s(s(s(s(s(s(n0))))))),X3,cons(s(s(s(s(s(s(n0)))))),empty_list))
| same(X0,s(s(s(s(s(s(s(n0))))))))
| ~ sum(X0,X1,s(s(s(s(s(s(s(n0)))))))) )
| ~ spl0_51 ),
inference(resolution,[],[f1879,f6]) ).
fof(f1884,plain,
( ! [X2,X3,X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(n0)))))))),X0,X1)
| same(s(s(X1)),s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(s(X0)),s(n0),X2)
| diagonal_attack(s(s(s(s(s(s(s(n0))))))),X2,cons(s(s(s(s(s(s(n0)))))),empty_list))
| same(X3,s(s(s(s(s(s(s(n0))))))))
| ~ sum(X3,s(X0),s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(n0),n0,s(X0)) )
| ~ spl0_51 ),
inference(resolution,[],[f1880,f6]) ).
fof(f2176,definition,
( spl0_169
<=> ! [X2] :
( diagonal_attack(s(s(s(s(s(n0))))),s(X2),cons(s(s(s(s(s(s(n0)))))),empty_list))
| ~ sum(s(n0),n0,X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_169])],[avatar_definition]) ).
fof(f2177,plain,
( ! [X2] :
( diagonal_attack(s(s(s(s(s(n0))))),s(X2),cons(s(s(s(s(s(s(n0)))))),empty_list))
| ~ sum(s(n0),n0,X2) )
| ~ spl0_169 ),
inference(avatar_component_clause,[],[f2176]) ).
fof(f2282,definition,
( spl0_172
<=> same(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(n0)))))) ),
introduced(definition,[new_symbols(definition,[spl0_172])],[avatar_definition]) ).
fof(f2283,plain,
( ~ same(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(n0))))))
| spl0_172 ),
inference(avatar_component_clause,[],[f2282]) ).
fof(f2284,plain,
( same(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(n0))))))
| ~ spl0_172 ),
inference(avatar_component_clause,[],[f2282]) ).
fof(f2286,plain,
( ! [X0] :
( ~ sum(X0,n0,s(s(s(s(s(s(s(n0))))))))
| same(X0,s(s(s(s(s(n0)))))) )
| ~ spl0_124 ),
inference(resolution,[],[f1574,f6]) ).
fof(f2287,plain,
( same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(n0))))))
| ~ spl0_124 ),
inference(resolution,[],[f2286,f5]) ).
fof(f2288,plain,
( same(s(s(s(s(s(s(n0)))))),s(s(s(s(n0)))))
| ~ spl0_124 ),
inference(resolution,[],[f2287,f11]) ).
fof(f2289,plain,
( same(s(s(s(s(s(n0))))),s(s(s(n0))))
| ~ spl0_124 ),
inference(resolution,[],[f2288,f11]) ).
fof(f2290,plain,
( same(s(s(s(s(n0)))),s(s(n0)))
| ~ spl0_124 ),
inference(resolution,[],[f2289,f11]) ).
fof(f2291,plain,
( same(s(s(s(n0))),s(n0))
| ~ spl0_124 ),
inference(resolution,[],[f2290,f11]) ).
fof(f2292,plain,
( same(s(s(n0)),n0)
| ~ spl0_124 ),
inference(resolution,[],[f2291,f11]) ).
fof(f2293,plain,
( $false
| ~ spl0_124 ),
inference(forward_subsumption_resolution,[],[f2292,f9]) ).
fof(f2294,plain,
~ spl0_124,
inference(avatar_contradiction_clause,[],[f2293]) ).
fof(f2295,plain,
( ! [X0] :
( ~ sum(s(s(s(s(s(s(s(s(n0)))))))),n0,X0)
| same(s(X0),s(s(s(s(s(n0)))))) )
| ~ spl0_125 ),
inference(resolution,[],[f1577,f6]) ).
fof(f2296,plain,
( same(s(s(s(s(s(s(s(s(s(n0))))))))),s(s(s(s(s(n0))))))
| ~ spl0_125 ),
inference(resolution,[],[f2295,f5]) ).
fof(f2297,plain,
( same(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(n0)))))
| ~ spl0_125 ),
inference(resolution,[],[f2296,f11]) ).
fof(f2298,plain,
( same(s(s(s(s(s(s(s(n0))))))),s(s(s(n0))))
| ~ spl0_125 ),
inference(resolution,[],[f2297,f11]) ).
fof(f2299,plain,
( same(s(s(s(s(s(s(n0)))))),s(s(n0)))
| ~ spl0_125 ),
inference(resolution,[],[f2298,f11]) ).
fof(f2300,plain,
( same(s(s(s(s(s(n0))))),s(n0))
| ~ spl0_125 ),
inference(resolution,[],[f2299,f11]) ).
fof(f2301,plain,
( same(s(s(s(s(n0)))),n0)
| ~ spl0_125 ),
inference(resolution,[],[f2300,f11]) ).
fof(f2302,plain,
( $false
| ~ spl0_125 ),
inference(forward_subsumption_resolution,[],[f2301,f9]) ).
fof(f2303,plain,
~ spl0_125,
inference(avatar_contradiction_clause,[],[f2302]) ).
fof(f2348,plain,
( same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(n0)))))
| ~ spl0_172 ),
inference(resolution,[],[f2284,f11]) ).
fof(f2352,plain,
( same(s(s(s(s(s(s(n0)))))),s(s(s(n0))))
| ~ spl0_172 ),
inference(resolution,[],[f2348,f11]) ).
fof(f2353,plain,
( same(s(s(s(s(s(n0))))),s(s(n0)))
| ~ spl0_172 ),
inference(resolution,[],[f2352,f11]) ).
fof(f2358,definition,
( spl0_179
<=> sum(s(s(s(s(n0)))),s(s(n0)),s(s(s(s(s(s(n0))))))) ),
introduced(definition,[new_symbols(definition,[spl0_179])],[avatar_definition]) ).
fof(f2359,plain,
( sum(s(s(s(s(n0)))),s(s(n0)),s(s(s(s(s(s(n0)))))))
| ~ spl0_179 ),
inference(avatar_component_clause,[],[f2358]) ).
fof(f2360,plain,
( ~ sum(s(s(s(s(n0)))),s(s(n0)),s(s(s(s(s(s(n0)))))))
| spl0_179 ),
inference(avatar_component_clause,[],[f2358]) ).
fof(f2370,plain,
( ~ sum(s(s(s(s(n0)))),s(n0),s(s(s(s(s(n0))))))
| spl0_179 ),
inference(resolution,[],[f2360,f6]) ).
fof(f2371,plain,
( $false
| ~ spl0_48
| spl0_179 ),
inference(forward_subsumption_resolution,[],[f2370,f1103]) ).
fof(f2372,plain,
( ~ spl0_48
| spl0_179 ),
inference(avatar_contradiction_clause,[],[f2371]) ).
fof(f2499,plain,
( same(s(s(s(s(n0)))),s(n0))
| ~ spl0_172 ),
inference(resolution,[],[f2353,f11]) ).
fof(f2504,plain,
( same(s(s(s(n0))),n0)
| ~ spl0_172 ),
inference(resolution,[],[f2499,f11]) ).
fof(f2505,plain,
( $false
| ~ spl0_172 ),
inference(forward_subsumption_resolution,[],[f2504,f9]) ).
fof(f2506,plain,
~ spl0_172,
inference(avatar_contradiction_clause,[],[f2505]) ).
fof(f2623,definition,
( spl0_205
<=> ! [X1] :
( same(X1,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(s(s(n0)))))),s(n0),X1) ) ),
introduced(definition,[new_symbols(definition,[spl0_205])],[avatar_definition]) ).
fof(f2624,plain,
( ! [X1] :
( ~ sum(s(s(s(s(s(s(n0)))))),s(n0),X1)
| same(X1,s(s(s(s(s(s(s(s(n0))))))))) )
| ~ spl0_205 ),
inference(avatar_component_clause,[],[f2623]) ).
fof(f2626,definition,
( spl0_206
<=> ! [X0] :
( same(X0,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(X0,s(n0),s(s(s(s(s(s(n0))))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_206])],[avatar_definition]) ).
fof(f2627,plain,
( ! [X0] :
( ~ sum(X0,s(n0),s(s(s(s(s(s(n0)))))))
| same(X0,s(s(s(s(s(s(s(s(n0))))))))) )
| ~ spl0_206 ),
inference(avatar_component_clause,[],[f2626]) ).
fof(f2727,plain,
( ! [X0,X1] :
( same(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(s(n0)),s(n0),X0)
| diagonal_attack(s(s(s(s(s(s(s(n0))))))),X0,cons(s(s(s(s(s(s(n0)))))),empty_list))
| same(X1,s(s(s(s(s(s(s(n0))))))))
| ~ sum(X1,s(n0),s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(n0),n0,s(n0)) )
| ~ spl0_51 ),
inference(resolution,[],[f1884,f5]) ).
fof(f2728,plain,
( ! [X0,X1] :
( same(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(s(n0)),s(n0),X0)
| diagonal_attack(s(s(s(s(s(s(s(n0))))))),X0,cons(s(s(s(s(s(s(n0)))))),empty_list))
| same(X1,s(s(s(s(s(s(s(n0))))))))
| ~ sum(X1,s(n0),s(s(s(s(s(s(s(n0)))))))) )
| ~ spl0_51 ),
inference(forward_subsumption_resolution,[],[f2727,f5]) ).
fof(f2730,definition,
( spl0_209
<=> ! [X1] :
( same(X1,s(s(s(s(s(s(s(n0))))))))
| ~ sum(X1,s(n0),s(s(s(s(s(s(s(n0)))))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_209])],[avatar_definition]) ).
fof(f2731,plain,
( ! [X1] :
( ~ sum(X1,s(n0),s(s(s(s(s(s(s(n0))))))))
| same(X1,s(s(s(s(s(s(s(n0)))))))) )
| ~ spl0_209 ),
inference(avatar_component_clause,[],[f2730]) ).
fof(f2733,definition,
( spl0_210
<=> ! [X0] :
( ~ sum(s(s(n0)),s(n0),X0)
| diagonal_attack(s(s(s(s(s(s(s(n0))))))),X0,cons(s(s(s(s(s(s(n0)))))),empty_list)) ) ),
introduced(definition,[new_symbols(definition,[spl0_210])],[avatar_definition]) ).
fof(f2734,plain,
( ! [X0] :
( diagonal_attack(s(s(s(s(s(s(s(n0))))))),X0,cons(s(s(s(s(s(s(n0)))))),empty_list))
| ~ sum(s(s(n0)),s(n0),X0) )
| ~ spl0_210 ),
inference(avatar_component_clause,[],[f2733]) ).
fof(f2736,definition,
( spl0_211
<=> same(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(n0)))))))) ),
introduced(definition,[new_symbols(definition,[spl0_211])],[avatar_definition]) ).
fof(f2738,plain,
( same(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(n0))))))))
| ~ spl0_211 ),
inference(avatar_component_clause,[],[f2736]) ).
fof(f2739,plain,
( spl0_209
| spl0_210
| spl0_211
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f2728,f1113,f2736,f2733,f2730]) ).
fof(f2740,plain,
( ! [X2,X0,X1] :
( ~ sum(s(s(s(s(s(s(n0)))))),s(n0),X0)
| same(X0,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(X1,s(n0),s(s(s(s(s(s(n0)))))))
| diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(X2),empty_list)
| same(X1,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(n0),n0,X2) )
| ~ spl0_52 ),
inference(resolution,[],[f1118,f37]) ).
fof(f2741,plain,
( ! [X2,X0,X1] :
( ~ sum(s(s(s(s(s(s(n0)))))),s(n0),X0)
| same(X0,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(X1,s(n0),s(s(s(s(s(s(n0)))))))
| same(X1,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(n0),n0,X2) )
| ~ spl0_52 ),
inference(forward_subsumption_resolution,[],[f2740,f14]) ).
fof(f2742,plain,
( spl0_8
| spl0_206
| spl0_205
| ~ spl0_52 ),
inference(avatar_split_clause,[],[f2741,f1116,f2623,f2626,f222]) ).
fof(f2743,plain,
( same(s(s(s(s(s(n0))))),s(s(s(s(s(s(n0)))))))
| ~ spl0_53 ),
inference(resolution,[],[f1122,f11]) ).
fof(f2752,plain,
( same(s(s(s(s(n0)))),s(s(s(s(s(n0))))))
| ~ spl0_53 ),
inference(resolution,[],[f2743,f11]) ).
fof(f2753,plain,
( same(s(s(s(n0))),s(s(s(s(n0)))))
| ~ spl0_53 ),
inference(resolution,[],[f2752,f11]) ).
fof(f2754,plain,
( same(s(s(n0)),s(s(s(n0))))
| ~ spl0_53 ),
inference(resolution,[],[f2753,f11]) ).
fof(f2755,plain,
( same(s(n0),s(s(n0)))
| ~ spl0_53 ),
inference(resolution,[],[f2754,f11]) ).
fof(f2756,plain,
( same(n0,s(n0))
| ~ spl0_53 ),
inference(resolution,[],[f2755,f11]) ).
fof(f2757,plain,
( $false
| ~ spl0_53 ),
inference(forward_subsumption_resolution,[],[f2756,f10]) ).
fof(f2758,plain,
~ spl0_53,
inference(avatar_contradiction_clause,[],[f2757]) ).
fof(f2760,plain,
( ! [X2,X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(n0)))))))),s(n0),X0)
| same(X0,s(s(s(s(s(n0))))))
| ~ sum(X1,s(n0),s(s(s(s(s(s(s(s(n0)))))))))
| diagonal_attack(s(s(s(s(s(n0))))),s(X2),cons(s(s(s(s(s(s(n0)))))),empty_list))
| same(X1,s(s(s(s(s(n0))))))
| ~ sum(s(n0),n0,X2) )
| ~ spl0_54 ),
inference(resolution,[],[f1126,f37]) ).
fof(f2761,plain,
( spl0_169
| spl0_124
| spl0_125
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f2760,f1124,f1576,f1573,f2176]) ).
fof(f2762,plain,
( ! [X2,X3,X0,X1] :
( ~ sum(s(n0),n0,X0)
| ~ sum(X1,s(X0),s(s(s(s(s(s(n0)))))))
| same(X1,s(s(s(s(s(n0))))))
| ~ sum(s(s(s(s(s(s(n0)))))),s(X0),X2)
| same(X2,s(s(s(s(s(n0))))))
| ~ sum(s(X0),s(n0),X3)
| diagonal_attack(s(s(s(s(s(n0))))),X3,empty_list) )
| ~ spl0_169 ),
inference(resolution,[],[f2177,f13]) ).
fof(f2763,plain,
( ! [X2,X3,X0,X1] :
( ~ sum(s(s(s(s(s(s(n0)))))),s(X0),X2)
| ~ sum(X1,s(X0),s(s(s(s(s(s(n0)))))))
| same(X1,s(s(s(s(s(n0))))))
| ~ sum(s(n0),n0,X0)
| same(X2,s(s(s(s(s(n0))))))
| ~ sum(s(X0),s(n0),X3) )
| ~ spl0_169 ),
inference(forward_subsumption_resolution,[],[f2762,f14]) ).
fof(f2764,plain,
( ! [X2,X3,X0,X1] :
( ~ sum(X0,s(X1),s(s(s(s(s(s(n0)))))))
| same(X0,s(s(s(s(s(n0))))))
| ~ sum(s(n0),n0,X1)
| same(s(X2),s(s(s(s(s(n0))))))
| ~ sum(s(X1),s(n0),X3)
| ~ sum(s(s(s(s(s(s(n0)))))),X1,X2) )
| ~ spl0_169 ),
inference(resolution,[],[f2763,f6]) ).
fof(f2766,plain,
( ! [X0,X1] :
( same(s(s(s(s(n0)))),s(s(s(s(s(n0))))))
| ~ sum(s(n0),n0,s(n0))
| same(s(X0),s(s(s(s(s(n0))))))
| ~ sum(s(s(n0)),s(n0),X1)
| ~ sum(s(s(s(s(s(s(n0)))))),s(n0),X0) )
| ~ spl0_169
| ~ spl0_179 ),
inference(resolution,[],[f2764,f2359]) ).
fof(f2767,plain,
( ! [X0,X1] :
( same(s(s(s(s(n0)))),s(s(s(s(s(n0))))))
| same(s(X0),s(s(s(s(s(n0))))))
| ~ sum(s(s(n0)),s(n0),X1)
| ~ sum(s(s(s(s(s(s(n0)))))),s(n0),X0) )
| ~ spl0_169
| ~ spl0_179 ),
inference(forward_subsumption_resolution,[],[f2766,f5]) ).
fof(f2769,definition,
( spl0_213
<=> ! [X1] : ~ sum(s(s(n0)),s(n0),X1) ),
introduced(definition,[new_symbols(definition,[spl0_213])],[avatar_definition]) ).
fof(f2770,plain,
( ! [X1] : ~ sum(s(s(n0)),s(n0),X1)
| ~ spl0_213 ),
inference(avatar_component_clause,[],[f2769]) ).
fof(f2772,definition,
( spl0_214
<=> ! [X0] :
( same(s(X0),s(s(s(s(s(n0))))))
| ~ sum(s(s(s(s(s(s(n0)))))),s(n0),X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_214])],[avatar_definition]) ).
fof(f2773,plain,
( ! [X0] :
( ~ sum(s(s(s(s(s(s(n0)))))),s(n0),X0)
| same(s(X0),s(s(s(s(s(n0)))))) )
| ~ spl0_214 ),
inference(avatar_component_clause,[],[f2772]) ).
fof(f2775,definition,
( spl0_215
<=> same(s(s(s(s(n0)))),s(s(s(s(s(n0)))))) ),
introduced(definition,[new_symbols(definition,[spl0_215])],[avatar_definition]) ).
fof(f2777,plain,
( same(s(s(s(s(n0)))),s(s(s(s(s(n0))))))
| ~ spl0_215 ),
inference(avatar_component_clause,[],[f2775]) ).
fof(f2778,plain,
( spl0_213
| spl0_214
| spl0_215
| ~ spl0_169
| ~ spl0_179 ),
inference(avatar_split_clause,[],[f2767,f2358,f2176,f2775,f2772,f2769]) ).
fof(f2780,plain,
( ! [X0] :
( same(s(X0),s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(s(s(n0)))))),n0,X0) )
| ~ spl0_205 ),
inference(resolution,[],[f2624,f6]) ).
fof(f2781,plain,
( ! [X0] :
( ~ sum(s(s(s(s(s(s(n0)))))),n0,X0)
| same(X0,s(s(s(s(s(s(s(n0)))))))) )
| ~ spl0_205 ),
inference(resolution,[],[f2780,f11]) ).
fof(f2785,plain,
( same(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(n0))))))))
| ~ spl0_205 ),
inference(resolution,[],[f2781,f5]) ).
fof(f2786,plain,
( $false
| spl0_53
| ~ spl0_205 ),
inference(forward_subsumption_resolution,[],[f2785,f1121]) ).
fof(f2787,plain,
( spl0_53
| ~ spl0_205 ),
inference(avatar_contradiction_clause,[],[f2786]) ).
fof(f2788,plain,
( ! [X0] :
( same(X0,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(X0,n0,s(s(s(s(s(n0)))))) )
| ~ spl0_206 ),
inference(resolution,[],[f2627,f6]) ).
fof(f2789,plain,
( ! [X0] :
( ~ sum(s(X0),n0,s(s(s(s(s(n0))))))
| same(X0,s(s(s(s(s(s(s(n0)))))))) )
| ~ spl0_206 ),
inference(resolution,[],[f2788,f11]) ).
fof(f2791,plain,
( same(s(s(s(s(n0)))),s(s(s(s(s(s(s(n0))))))))
| ~ spl0_206 ),
inference(resolution,[],[f2789,f5]) ).
fof(f2792,plain,
( same(s(s(s(n0))),s(s(s(s(s(s(n0)))))))
| ~ spl0_206 ),
inference(resolution,[],[f2791,f11]) ).
fof(f2793,plain,
( same(s(s(n0)),s(s(s(s(s(n0))))))
| ~ spl0_206 ),
inference(resolution,[],[f2792,f11]) ).
fof(f2794,plain,
( same(s(n0),s(s(s(s(n0)))))
| ~ spl0_206 ),
inference(resolution,[],[f2793,f11]) ).
fof(f2795,plain,
( same(n0,s(s(s(n0))))
| ~ spl0_206 ),
inference(resolution,[],[f2794,f11]) ).
fof(f2796,plain,
( $false
| ~ spl0_206 ),
inference(forward_subsumption_resolution,[],[f2795,f10]) ).
fof(f2797,plain,
~ spl0_206,
inference(avatar_contradiction_clause,[],[f2796]) ).
fof(f2799,plain,
( ! [X0] :
( ~ sum(X0,n0,s(s(s(s(s(s(n0)))))))
| same(X0,s(s(s(s(s(s(s(n0)))))))) )
| ~ spl0_209 ),
inference(resolution,[],[f2731,f6]) ).
fof(f2800,plain,
( same(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(n0))))))))
| ~ spl0_209 ),
inference(resolution,[],[f2799,f5]) ).
fof(f2801,plain,
( $false
| spl0_53
| ~ spl0_209 ),
inference(forward_subsumption_resolution,[],[f2800,f1121]) ).
fof(f2802,plain,
( spl0_53
| ~ spl0_209 ),
inference(avatar_contradiction_clause,[],[f2801]) ).
fof(f2803,plain,
( ! [X2,X3,X0,X1] :
( ~ sum(s(s(n0)),s(n0),X0)
| ~ sum(X1,X0,s(s(s(s(s(s(n0)))))))
| same(X1,s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(s(s(s(s(s(n0)))))),X0,X2)
| same(X2,s(s(s(s(s(s(s(n0))))))))
| ~ sum(X0,s(n0),X3)
| diagonal_attack(s(s(s(s(s(s(s(n0))))))),X3,empty_list) )
| ~ spl0_210 ),
inference(resolution,[],[f2734,f13]) ).
fof(f2804,plain,
( ! [X2,X3,X0,X1] :
( ~ sum(s(s(s(s(s(s(n0)))))),X0,X2)
| ~ sum(X1,X0,s(s(s(s(s(s(n0)))))))
| same(X1,s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(s(n0)),s(n0),X0)
| same(X2,s(s(s(s(s(s(s(n0))))))))
| ~ sum(X0,s(n0),X3) )
| ~ spl0_210 ),
inference(forward_subsumption_resolution,[],[f2803,f14]) ).
fof(f2808,plain,
( ! [X2,X3,X0,X1] :
( ~ sum(X0,s(X1),s(s(s(s(s(s(n0)))))))
| same(X0,s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(s(n0)),s(n0),s(X1))
| same(s(X2),s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(X1),s(n0),X3)
| ~ sum(s(s(s(s(s(s(n0)))))),X1,X2) )
| ~ spl0_210 ),
inference(resolution,[],[f2804,f6]) ).
fof(f2822,plain,
( ! [X2,X3,X0,X1] :
( ~ sum(s(s(s(s(s(s(n0)))))),X1,X2)
| ~ sum(s(s(n0)),s(n0),s(X1))
| same(s(X2),s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(X1),s(n0),X3)
| same(X0,s(s(s(s(s(s(s(n0))))))))
| ~ sum(X0,X1,s(s(s(s(s(n0)))))) )
| ~ spl0_210 ),
inference(resolution,[],[f2808,f6]) ).
fof(f2839,plain,
( ! [X2,X3,X0,X1] :
( ~ sum(s(s(s(s(s(s(n0)))))),X0,X1)
| same(s(s(X1)),s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(s(X0)),s(n0),X2)
| same(X3,s(s(s(s(s(s(s(n0))))))))
| ~ sum(X3,s(X0),s(s(s(s(s(n0))))))
| ~ sum(s(s(n0)),s(n0),s(s(X0))) )
| ~ spl0_210 ),
inference(resolution,[],[f2822,f6]) ).
fof(f2925,definition,
( spl0_227
<=> same(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(n0))))))) ),
introduced(definition,[new_symbols(definition,[spl0_227])],[avatar_definition]) ).
fof(f2927,plain,
( same(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(n0)))))))
| ~ spl0_227 ),
inference(avatar_component_clause,[],[f2925]) ).
fof(f2980,plain,
( ! [X0] : ~ sum(s(s(n0)),n0,X0)
| ~ spl0_213 ),
inference(resolution,[],[f2770,f6]) ).
fof(f2981,plain,
( $false
| ~ spl0_213 ),
inference(resolution,[],[f2980,f5]) ).
fof(f2982,plain,
~ spl0_213,
inference(avatar_contradiction_clause,[],[f2981]) ).
fof(f3053,definition,
( spl0_238
<=> same(s(s(s(s(s(s(s(s(s(n0))))))))),s(s(s(s(s(s(n0))))))) ),
introduced(definition,[new_symbols(definition,[spl0_238])],[avatar_definition]) ).
fof(f3055,plain,
( same(s(s(s(s(s(s(s(s(s(n0))))))))),s(s(s(s(s(s(n0)))))))
| ~ spl0_238 ),
inference(avatar_component_clause,[],[f3053]) ).
fof(f3216,plain,
( ! [X2,X3,X0,X1] :
( ~ sum(X3,s(s(X1)),s(s(s(s(s(n0))))))
| ~ sum(s(s(s(X1))),s(n0),X2)
| same(X3,s(s(s(s(s(s(s(n0))))))))
| same(s(s(s(X0))),s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(s(n0)),s(n0),s(s(s(X1))))
| ~ sum(s(s(s(s(s(s(n0)))))),X1,X0) )
| ~ spl0_210 ),
inference(resolution,[],[f2839,f6]) ).
fof(f3218,plain,
( ! [X2,X3,X0,X1] :
( ~ sum(s(s(s(s(s(s(n0)))))),X0,X3)
| same(X2,s(s(s(s(s(s(s(n0))))))))
| same(s(s(s(X3))),s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(s(n0)),s(n0),s(s(s(X0))))
| ~ sum(s(s(s(X0))),s(n0),X1)
| ~ sum(X2,s(X0),s(s(s(s(n0))))) )
| ~ spl0_210 ),
inference(resolution,[],[f3216,f6]) ).
fof(f3220,plain,
( ! [X0,X1] :
( same(X0,s(s(s(s(s(s(s(n0))))))))
| same(s(s(s(s(s(s(s(s(s(n0))))))))),s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(s(n0)),s(n0),s(s(s(n0))))
| ~ sum(s(s(s(n0))),s(n0),X1)
| ~ sum(X0,s(n0),s(s(s(s(n0))))) )
| ~ spl0_210 ),
inference(resolution,[],[f3218,f5]) ).
fof(f3222,definition,
( spl0_242
<=> ! [X1] : ~ sum(s(s(s(n0))),s(n0),X1) ),
introduced(definition,[new_symbols(definition,[spl0_242])],[avatar_definition]) ).
fof(f3223,plain,
( ! [X1] : ~ sum(s(s(s(n0))),s(n0),X1)
| ~ spl0_242 ),
inference(avatar_component_clause,[],[f3222]) ).
fof(f3225,definition,
( spl0_243
<=> sum(s(s(n0)),s(n0),s(s(s(n0)))) ),
introduced(definition,[new_symbols(definition,[spl0_243])],[avatar_definition]) ).
fof(f3227,plain,
( ~ sum(s(s(n0)),s(n0),s(s(s(n0))))
| spl0_243 ),
inference(avatar_component_clause,[],[f3225]) ).
fof(f3229,definition,
( spl0_244
<=> same(s(s(s(s(s(s(s(s(s(n0))))))))),s(s(s(s(s(s(s(n0)))))))) ),
introduced(definition,[new_symbols(definition,[spl0_244])],[avatar_definition]) ).
fof(f3231,plain,
( same(s(s(s(s(s(s(s(s(s(n0))))))))),s(s(s(s(s(s(s(n0))))))))
| ~ spl0_244 ),
inference(avatar_component_clause,[],[f3229]) ).
fof(f3233,definition,
( spl0_245
<=> ! [X0] :
( same(X0,s(s(s(s(s(s(s(n0))))))))
| ~ sum(X0,s(n0),s(s(s(s(n0))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_245])],[avatar_definition]) ).
fof(f3234,plain,
( ! [X0] :
( same(X0,s(s(s(s(s(s(s(n0))))))))
| ~ sum(X0,s(n0),s(s(s(s(n0))))) )
| ~ spl0_245 ),
inference(avatar_component_clause,[],[f3233]) ).
fof(f3235,plain,
( spl0_242
| ~ spl0_243
| spl0_244
| spl0_245
| ~ spl0_210 ),
inference(avatar_split_clause,[],[f3220,f2733,f3233,f3229,f3225,f3222]) ).
fof(f3236,plain,
( ~ sum(s(s(n0)),n0,s(s(n0)))
| spl0_243 ),
inference(resolution,[],[f3227,f6]) ).
fof(f3237,plain,
( $false
| spl0_243 ),
inference(forward_subsumption_resolution,[],[f3236,f5]) ).
fof(f3238,plain,
spl0_243,
inference(avatar_contradiction_clause,[],[f3237]) ).
fof(f3239,plain,
( same(s(s(s(s(s(s(s(s(s(n0))))))))),s(s(s(s(s(s(n0)))))))
| ~ spl0_211 ),
inference(resolution,[],[f2738,f11]) ).
fof(f3240,plain,
( spl0_238
| ~ spl0_211 ),
inference(avatar_split_clause,[],[f3239,f2736,f3053]) ).
fof(f3241,plain,
( ! [X0] :
( ~ sum(s(s(s(s(s(s(n0)))))),n0,X0)
| same(s(s(X0)),s(s(s(s(s(n0)))))) )
| ~ spl0_214 ),
inference(resolution,[],[f2773,f6]) ).
fof(f3244,plain,
( same(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(n0))))))
| ~ spl0_214 ),
inference(resolution,[],[f3241,f5]) ).
fof(f3245,plain,
( $false
| spl0_172
| ~ spl0_214 ),
inference(forward_subsumption_resolution,[],[f3244,f2283]) ).
fof(f3246,plain,
( spl0_172
| ~ spl0_214 ),
inference(avatar_contradiction_clause,[],[f3245]) ).
fof(f3247,plain,
( same(s(s(s(n0))),s(s(s(s(n0)))))
| ~ spl0_215 ),
inference(resolution,[],[f2777,f11]) ).
fof(f3249,plain,
( same(s(s(n0)),s(s(s(n0))))
| ~ spl0_215 ),
inference(resolution,[],[f3247,f11]) ).
fof(f3531,plain,
( same(s(n0),s(s(n0)))
| ~ spl0_215 ),
inference(resolution,[],[f3249,f11]) ).
fof(f3532,plain,
( same(n0,s(n0))
| ~ spl0_215 ),
inference(resolution,[],[f3531,f11]) ).
fof(f3533,plain,
( $false
| ~ spl0_215 ),
inference(forward_subsumption_resolution,[],[f3532,f10]) ).
fof(f3534,plain,
~ spl0_215,
inference(avatar_contradiction_clause,[],[f3533]) ).
fof(f3539,plain,
( same(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(n0))))))
| ~ spl0_238 ),
inference(resolution,[],[f3055,f11]) ).
fof(f3540,plain,
( $false
| spl0_172
| ~ spl0_238 ),
inference(forward_subsumption_resolution,[],[f3539,f2283]) ).
fof(f3541,plain,
( spl0_172
| ~ spl0_238 ),
inference(avatar_contradiction_clause,[],[f3540]) ).
fof(f3544,plain,
( ! [X0] : ~ sum(s(s(s(n0))),n0,X0)
| ~ spl0_242 ),
inference(resolution,[],[f3223,f6]) ).
fof(f3545,plain,
( $false
| ~ spl0_242 ),
inference(resolution,[],[f3544,f5]) ).
fof(f3546,plain,
~ spl0_242,
inference(avatar_contradiction_clause,[],[f3545]) ).
fof(f3547,plain,
( same(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(n0)))))))
| ~ spl0_244 ),
inference(resolution,[],[f3231,f11]) ).
fof(f3548,plain,
( spl0_227
| ~ spl0_244 ),
inference(avatar_split_clause,[],[f3547,f3229,f2925]) ).
fof(f3549,plain,
( same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(n0))))))
| ~ spl0_227 ),
inference(resolution,[],[f2927,f11]) ).
fof(f3559,plain,
( same(s(s(s(s(s(s(n0)))))),s(s(s(s(n0)))))
| ~ spl0_227 ),
inference(resolution,[],[f3549,f11]) ).
fof(f3562,plain,
( same(s(s(s(s(s(n0))))),s(s(s(n0))))
| ~ spl0_227 ),
inference(resolution,[],[f3559,f11]) ).
fof(f3563,plain,
( same(s(s(s(s(n0)))),s(s(n0)))
| ~ spl0_227 ),
inference(resolution,[],[f3562,f11]) ).
fof(f3564,plain,
( same(s(s(s(n0))),s(n0))
| ~ spl0_227 ),
inference(resolution,[],[f3563,f11]) ).
fof(f3800,plain,
( same(s(s(n0)),n0)
| ~ spl0_227 ),
inference(resolution,[],[f3564,f11]) ).
fof(f3801,plain,
( $false
| ~ spl0_227 ),
inference(forward_subsumption_resolution,[],[f3800,f9]) ).
fof(f3802,plain,
~ spl0_227,
inference(avatar_contradiction_clause,[],[f3801]) ).
fof(f3805,plain,
( ! [X0] :
( ~ sum(s(X0),s(n0),s(s(s(s(n0)))))
| same(X0,s(s(s(s(s(s(n0))))))) )
| ~ spl0_245 ),
inference(resolution,[],[f3234,f11]) ).
fof(f3809,plain,
( ! [X0] :
( same(X0,s(s(s(s(s(s(n0)))))))
| ~ sum(s(X0),n0,s(s(s(n0)))) )
| ~ spl0_245 ),
inference(resolution,[],[f3805,f6]) ).
fof(f3813,plain,
( ! [X0] :
( ~ sum(s(s(X0)),n0,s(s(s(n0))))
| same(X0,s(s(s(s(s(n0)))))) )
| ~ spl0_245 ),
inference(resolution,[],[f3809,f11]) ).
fof(f3815,plain,
( same(s(n0),s(s(s(s(s(n0))))))
| ~ spl0_245 ),
inference(resolution,[],[f3813,f5]) ).
fof(f3816,plain,
( same(n0,s(s(s(s(n0)))))
| ~ spl0_245 ),
inference(resolution,[],[f3815,f11]) ).
fof(f3817,plain,
( $false
| ~ spl0_245 ),
inference(forward_subsumption_resolution,[],[f3816,f10]) ).
fof(f3818,plain,
~ spl0_245,
inference(avatar_contradiction_clause,[],[f3817]) ).
cnf(s3,plain,
spl0_3,
inference(sat_conversion,[],[f165]) ).
cnf(s8,plain,
spl0_14,
inference(sat_conversion,[],[f445]) ).
cnf(s9,plain,
( ~ spl0_3
| spl0_16 ),
inference(sat_conversion,[],[f448]) ).
cnf(s14,plain,
~ spl0_8,
inference(sat_conversion,[],[f488]) ).
cnf(s16,plain,
( ~ spl0_14
| spl0_28 ),
inference(sat_conversion,[],[f656]) ).
cnf(s28,plain,
( ~ spl0_46
| ~ spl0_47
| ~ spl0_48
| ~ spl0_49
| spl0_50
| spl0_51
| spl0_52
| spl0_53
| spl0_54 ),
inference(sat_conversion,[],[f1127]) ).
cnf(s29,plain,
( ~ spl0_28
| spl0_46 ),
inference(sat_conversion,[],[f1130]) ).
cnf(s30,plain,
spl0_47,
inference(sat_conversion,[],[f1142]) ).
cnf(s31,plain,
spl0_48,
inference(sat_conversion,[],[f1145]) ).
cnf(s32,plain,
( ~ spl0_34
| spl0_49 ),
inference(sat_conversion,[],[f1147]) ).
cnf(s33,plain,
( ~ spl0_13
| spl0_34 ),
inference(sat_conversion,[],[f1149]) ).
cnf(s35,plain,
( spl0_13
| ~ spl0_16 ),
inference(sat_conversion,[],[f1176]) ).
cnf(s81,plain,
~ spl0_50,
inference(sat_conversion,[],[f1877]) ).
cnf(s109,plain,
~ spl0_124,
inference(sat_conversion,[],[f2294]) ).
cnf(s110,plain,
~ spl0_125,
inference(sat_conversion,[],[f2303]) ).
cnf(s118,plain,
( ~ spl0_48
| spl0_179 ),
inference(sat_conversion,[],[f2372]) ).
cnf(s130,plain,
~ spl0_172,
inference(sat_conversion,[],[f2506]) ).
cnf(s143,plain,
( ~ spl0_51
| spl0_209
| spl0_210
| spl0_211 ),
inference(sat_conversion,[],[f2739]) ).
cnf(s144,plain,
( spl0_8
| ~ spl0_52
| spl0_205
| spl0_206 ),
inference(sat_conversion,[],[f2742]) ).
cnf(s146,plain,
~ spl0_53,
inference(sat_conversion,[],[f2758]) ).
cnf(s147,plain,
( ~ spl0_54
| spl0_124
| spl0_125
| spl0_169 ),
inference(sat_conversion,[],[f2761]) ).
cnf(s148,plain,
( ~ spl0_169
| ~ spl0_179
| spl0_213
| spl0_214
| spl0_215 ),
inference(sat_conversion,[],[f2778]) ).
cnf(s149,plain,
( spl0_53
| ~ spl0_205 ),
inference(sat_conversion,[],[f2787]) ).
cnf(s150,plain,
~ spl0_206,
inference(sat_conversion,[],[f2797]) ).
cnf(s151,plain,
( spl0_53
| ~ spl0_209 ),
inference(sat_conversion,[],[f2802]) ).
cnf(s163,plain,
~ spl0_213,
inference(sat_conversion,[],[f2982]) ).
cnf(s172,plain,
( ~ spl0_210
| spl0_242
| ~ spl0_243
| spl0_244
| spl0_245 ),
inference(sat_conversion,[],[f3235]) ).
cnf(s173,plain,
spl0_243,
inference(sat_conversion,[],[f3238]) ).
cnf(s174,plain,
( ~ spl0_211
| spl0_238 ),
inference(sat_conversion,[],[f3240]) ).
cnf(s175,plain,
( spl0_172
| ~ spl0_214 ),
inference(sat_conversion,[],[f3246]) ).
cnf(s199,plain,
~ spl0_215,
inference(sat_conversion,[],[f3534]) ).
cnf(s201,plain,
( spl0_172
| ~ spl0_238 ),
inference(sat_conversion,[],[f3541]) ).
cnf(s202,plain,
~ spl0_242,
inference(sat_conversion,[],[f3546]) ).
cnf(s203,plain,
( spl0_227
| ~ spl0_244 ),
inference(sat_conversion,[],[f3548]) ).
cnf(s210,plain,
~ spl0_227,
inference(sat_conversion,[],[f3802]) ).
cnf(s211,plain,
~ spl0_245,
inference(sat_conversion,[],[f3818]) ).
cnf(s212,plain,
~ spl0_244,
inference(rat,[],[s203,s210]) ).
cnf(s214,plain,
~ spl0_210,
inference(rat,[],[s172,s211,s212,s173,s202]) ).
cnf(s220,plain,
( ~ spl0_169
| ~ spl0_179
| spl0_214 ),
inference(rat,[],[s148,s199,s163]) ).
cnf(s222,plain,
~ spl0_209,
inference(rat,[],[s151,s146]) ).
cnf(s223,plain,
~ spl0_205,
inference(rat,[],[s149,s146]) ).
cnf(s225,plain,
( spl0_8
| ~ spl0_52 ),
inference(rat,[],[s144,s150,s223]) ).
cnf(s226,plain,
( ~ spl0_51
| spl0_211 ),
inference(rat,[],[s143,s214,s222]) ).
cnf(s230,plain,
~ spl0_238,
inference(rat,[],[s201,s130]) ).
cnf(s231,plain,
~ spl0_214,
inference(rat,[],[s175,s130]) ).
cnf(s232,plain,
~ spl0_211,
inference(rat,[],[s174,s230]) ).
cnf(s233,plain,
~ spl0_51,
inference(rat,[],[s226,s232]) ).
cnf(s255,plain,
spl0_179,
inference(rat,[],[s118,s31]) ).
cnf(s256,plain,
~ spl0_169,
inference(rat,[],[s220,s231,s255]) ).
cnf(s257,plain,
~ spl0_54,
inference(rat,[],[s147,s109,s110,s256]) ).
cnf(s263,plain,
( ~ spl0_46
| ~ spl0_49
| spl0_52 ),
inference(rat,[],[s28,s257,s146,s233,s81,s31,s30]) ).
cnf(s268,plain,
~ spl0_52,
inference(rat,[],[s225,s14]) ).
cnf(s280,plain,
spl0_28,
inference(rat,[],[s16,s8]) ).
cnf(s281,plain,
spl0_46,
inference(rat,[],[s29,s280]) ).
cnf(s283,plain,
~ spl0_49,
inference(rat,[],[s263,s268,s281]) ).
cnf(s285,plain,
~ spl0_34,
inference(rat,[],[s32,s283]) ).
cnf(s286,plain,
~ spl0_13,
inference(rat,[],[s33,s285]) ).
cnf(s287,plain,
~ spl0_16,
inference(rat,[],[s35,s286]) ).
cnf(s288,plain,
~ spl0_3,
inference(rat,[],[s9,s287]) ).
cnf(s290,plain,
$false,
inference(rat,[],[s3,s288]) ).
fof(f3819,plain,
$false,
inference(avatar_sat_refutation,[],[s290]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ034-1.004 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n009.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 22:31:45 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.43/2.62 % (2475915)Input is clausal, will run a generic CNF schedule.
% 12.43/2.62 % (2475920)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=2485460986:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 12.43/2.62 % (2475924)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2045291666:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 12.43/2.62 % (2475922)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=58045649:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 12.43/2.62 % (2475926)dis-21_1_sil=8000:lcm=predicate:random_seed=3595852802:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 12.43/2.62 % (2475921)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1466582767:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 12.43/2.62 % (2475923)lrs+10_1_sil=8000:sp=occurrence:random_seed=930329512:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 12.43/2.62 % (2475925)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1169684122:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 12.43/2.62 % (2475923)Instruction limit reached!
% 12.43/2.62 % (2475923)------------------------------
% 12.43/2.62 % (2475923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.43/2.62 % (2475923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.43/2.62 % (2475923)CaDiCaL version: 2.1.3
% 12.43/2.62 % (2475923)Termination reason: Instruction limit
% 12.43/2.62 % (2475923)Termination phase: Saturation
% 12.43/2.62 % (2475923)Time elapsed: 0.062 s
% 12.43/2.62 % (2475923)Peak memory usage: 89 MB
% 12.43/2.62 % (2475923)Instructions burned: 109 (million)
% 12.43/2.62 % (2475924)Instruction limit reached!
% 12.43/2.62 % (2475924)------------------------------
% 12.43/2.62 % (2475924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.43/2.62 % (2475924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.43/2.62 % (2475924)CaDiCaL version: 2.1.3
% 12.43/2.62 % (2475924)Termination reason: Instruction limit
% 12.43/2.62 % (2475924)Termination phase: Saturation
% 12.43/2.62 % (2475924)Time elapsed: 0.067 s
% 12.43/2.62 % (2475924)Peak memory usage: 89 MB
% 12.43/2.62 % (2475924)Instructions burned: 116 (million)
% 12.43/2.62 % (2475926)Instruction limit reached!
% 12.43/2.62 % (2475926)------------------------------
% 12.43/2.62 % (2475926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.43/2.62 % (2475926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.43/2.62 % (2475926)CaDiCaL version: 2.1.3
% 12.43/2.62 % (2475926)Termination reason: Instruction limit
% 12.43/2.62 % (2475926)Termination phase: Saturation
% 12.43/2.62 % (2475926)Time elapsed: 0.068 s
% 12.43/2.62 % (2475926)Peak memory usage: 88 MB
% 12.43/2.62 % (2475926)Instructions burned: 117 (million)
% 12.43/2.62 % (2475925)Instruction limit reached!
% 12.43/2.62 % (2475925)------------------------------
% 12.43/2.62 % (2475925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.43/2.62 % (2475925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.43/2.62 % (2475925)CaDiCaL version: 2.1.3
% 12.43/2.62 % (2475925)Termination reason: Instruction limit
% 12.43/2.62 % (2475925)Termination phase: Saturation
% 12.43/2.62 % (2475925)Time elapsed: 0.116 s
% 12.43/2.62 % (2475925)Peak memory usage: 90 MB
% 12.43/2.62 % (2475925)Instructions burned: 181 (million)
% 12.43/2.62 % (2475934)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=3078709502:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 12.43/2.62 % (2475935)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3245448369:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 12.43/2.62 % (2475936)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2202111256:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 12.43/2.62 % (2475934)Refutation not found, incomplete strategy
% 12.43/2.62 % (2475934)------------------------------
% 12.43/2.62 % (2475934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.62/3.63 % (2475936)Refutation not found, incomplete strategy
% 19.62/3.63 % (2475936)------------------------------
% 19.62/3.63 % (2475936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.62/3.63 % (2475936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.62/3.63 % (2475934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.62/3.63 % (2475936)CaDiCaL version: 2.1.3
% 19.62/3.63 % (2475934)CaDiCaL version: 2.1.3
% 19.62/3.63 % (2475934)Termination reason: Refutation not found, incomplete strategy
% 19.62/3.63 % (2475934)Time elapsed: 0.001 s
% 19.62/3.63 % (2475936)Termination reason: Refutation not found, incomplete strategy
% 19.62/3.63 % (2475936)Time elapsed: 0.001 s
% 19.62/3.63 % (2475934)Peak memory usage: 87 MB
% 19.62/3.63 % (2475936)Peak memory usage: 87 MB
% 19.62/3.63 % (2475935)Refutation not found, incomplete strategy
% 19.62/3.63 % (2475935)------------------------------
% 19.62/3.63 % (2475935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.62/3.63 % (2475935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.62/3.63 % (2475935)CaDiCaL version: 2.1.3
% 19.62/3.63 % (2475935)Termination reason: Refutation not found, incomplete strategy
% 19.62/3.63 % (2475935)Time elapsed: 0.002 s
% 19.62/3.63 % (2475935)Peak memory usage: 87 MB
% 19.62/3.63 % (2475935)Instructions burned: 1 (million)
% 19.62/3.63 % (2475937)lrs+10_64_to=lpo:sil=8000:random_seed=34065687:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 19.62/3.63 % (2475937)Instruction limit reached!
% 19.62/3.63 % (2475937)------------------------------
% 19.62/3.63 % (2475937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.62/3.63 % (2475937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.62/3.63 % (2475937)CaDiCaL version: 2.1.3
% 19.62/3.63 % (2475937)Termination reason: Instruction limit
% 19.62/3.63 % (2475937)Termination phase: Saturation
% 19.62/3.63 % (2475937)Time elapsed: 0.077 s
% 19.62/3.63 % (2475937)Peak memory usage: 89 MB
% 19.62/3.63 % (2475937)Instructions burned: 126 (million)
% 19.62/3.63 % (2475934)------------------------------
% 19.62/3.63 % (2475934)------------------------------
% 19.62/3.63 % (2475935)------------------------------
% 19.62/3.63 % (2475935)------------------------------
% 19.62/3.63 % (2475936)------------------------------
% 19.62/3.63 % (2475936)------------------------------
% 19.62/3.63 % (2475942)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3950031497:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 19.62/3.63 % (2475944)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=609610665:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 19.62/3.63 % (2475943)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1392698812:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 19.62/3.63 % (2475945)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=3446150920:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 19.62/3.63 % (2475942)Instruction limit reached!
% 19.62/3.63 % (2475942)------------------------------
% 19.62/3.63 % (2475942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.62/3.63 % (2475942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.62/3.63 % (2475942)CaDiCaL version: 2.1.3
% 19.62/3.63 % (2475942)Termination reason: Instruction limit
% 19.62/3.63 % (2475942)Termination phase: Saturation
% 19.62/3.63 % (2475942)Time elapsed: 0.119 s
% 19.62/3.63 % (2475942)Peak memory usage: 90 MB
% 19.62/3.63 % (2475942)Instructions burned: 195 (million)
% 19.62/3.63 % (2475945)Instruction limit reached!
% 19.62/3.63 % (2475945)------------------------------
% 19.62/3.63 % (2475945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.62/3.63 % (2475945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.62/3.63 % (2475945)CaDiCaL version: 2.1.3
% 19.62/3.63 % (2475945)Termination reason: Instruction limit
% 19.62/3.63 % (2475945)Termination phase: Saturation
% 19.62/3.63 % (2475945)Time elapsed: 0.047 s
% 19.62/3.63 % (2475945)Peak memory usage: 88 MB
% 19.62/3.63 % (2475945)Instructions burned: 108 (million)
% 19.62/3.63 % (2475943)Instruction limit reached!
% 19.62/3.63 % (2475943)------------------------------
% 19.62/3.63 % (2475943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.62/3.63 % (2475943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.62/3.63 % (2475943)CaDiCaL version: 2.1.3
% 19.62/3.63 % (2475943)Termination reason: Instruction limit
% 19.62/3.63 % (2475943)Termination phase: Saturation
% 19.62/3.63 % (2475943)Time elapsed: 0.096 s
% 19.62/3.63 % (2475943)Peak memory usage: 90 MB
% 19.62/3.63 % (2475943)Instructions burned: 157 (million)
% 19.62/3.63 % (2475950)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2259713990:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 19.62/3.63 % (2475950)Refutation not found, incomplete strategy
% 19.62/3.63 % (2475950)------------------------------
% 19.62/3.63 % (2475950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.62/3.63 % (2475950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.62/3.63 % (2475950)CaDiCaL version: 2.1.3
% 19.62/3.63 % (2475950)Termination reason: Refutation not found, incomplete strategy
% 19.62/3.63 % (2475950)Time elapsed: 0.001 s
% 19.62/3.63 % (2475950)Peak memory usage: 87 MB
% 19.62/3.63 % (2475951)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=18693234:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 19.62/3.63 % (2475952)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3539832206:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 19.62/3.63 % (2475951)Instruction limit reached!
% 19.62/3.63 % (2475951)------------------------------
% 19.62/3.63 % (2475951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.62/3.63 % (2475951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.62/3.63 % (2475951)CaDiCaL version: 2.1.3
% 19.62/3.63 % (2475951)Termination reason: Instruction limit
% 19.62/3.63 % (2475951)Termination phase: Saturation
% 19.62/3.63 % (2475951)Time elapsed: 0.107 s
% 19.62/3.63 % (2475951)Peak memory usage: 88 MB
% 19.62/3.63 % (2475951)Instructions burned: 244 (million)
% 19.62/3.63 % (2475950)------------------------------
% 19.62/3.63 % (2475950)------------------------------
% 19.62/3.63 % (2475956)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3565039161:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 19.62/3.63 % (2475956)Instruction limit reached!
% 19.62/3.63 % (2475956)------------------------------
% 19.62/3.63 % (2475956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.62/3.63 % (2475956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.62/3.63 % (2475956)CaDiCaL version: 2.1.3
% 19.62/3.63 % (2475956)Termination reason: Instruction limit
% 19.62/3.63 % (2475956)Termination phase: Saturation
% 19.62/3.63 % (2475956)Time elapsed: 0.081 s
% 19.62/3.63 % (2475956)Peak memory usage: 89 MB
% 19.62/3.63 % (2475956)Instructions burned: 134 (million)
% 19.62/3.63 % (2475957)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2029601147:i=499:bd=all_2987 on theBenchmark for (2987ds/499Mi)
% 19.62/3.63 % (2475959)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2028554312:i=191:fgj=on:bd=all_2986 on theBenchmark for (2986ds/191Mi)
% 19.62/3.63 % (2475957)Instruction limit reached!
% 19.62/3.63 % (2475957)------------------------------
% 19.62/3.63 % (2475957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.62/3.63 % (2475957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.62/3.63 % (2475957)CaDiCaL version: 2.1.3
% 19.62/3.63 % (2475957)Termination reason: Instruction limit
% 19.62/3.63 % (2475957)Termination phase: Saturation
% 19.62/3.63 % (2475957)Time elapsed: 0.244 s
% 19.62/3.63 % (2475957)Peak memory usage: 89 MB
% 19.62/3.63 % (2475957)Instructions burned: 499 (million)
% 19.62/3.63 % (2475959)Instruction limit reached!
% 19.62/3.63 % (2475959)------------------------------
% 19.62/3.63 % (2475959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.62/3.63 % (2475959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.62/3.63 % (2475959)CaDiCaL version: 2.1.3
% 19.62/3.63 % (2475959)Termination reason: Instruction limit
% 19.62/3.63 % (2475959)Termination phase: Saturation
% 19.62/3.63 % (2475959)Time elapsed: 0.119 s
% 19.62/3.63 % (2475959)Peak memory usage: 91 MB
% 19.62/3.63 % (2475959)Instructions burned: 191 (million)
% 19.62/3.63 % (2475962)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1636825628:i=264:kws=precedence:fsr=off_2983 on theBenchmark for (2983ds/264Mi)
% 19.62/3.63 % (2475963)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3777271907:cond=on:i=156:bs=on:gtg=exists_all:er=known_2983 on theBenchmark for (2983ds/156Mi)
% 19.62/3.63 % (2475963)Instruction limit reached!
% 19.62/3.63 % (2475963)------------------------------
% 19.62/3.63 % (2475963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.62/3.63 % (2475963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.62/3.63 % (2475963)CaDiCaL version: 2.1.3
% 19.62/3.63 % (2475963)Termination reason: Instruction limit
% 19.62/3.63 % (2475963)Termination phase: Saturation
% 19.62/3.63 % (2475963)Time elapsed: 0.093 s
% 19.62/3.63 % (2475963)Peak memory usage: 89 MB
% 19.62/3.63 % (2475963)Instructions burned: 157 (million)
% 19.62/3.63 % (2475962)Instruction limit reached!
% 19.62/3.63 % (2475962)------------------------------
% 19.62/3.63 % (2475962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.62/3.63 % (2475962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.62/3.63 % (2475962)CaDiCaL version: 2.1.3
% 19.62/3.63 % (2475962)Termination reason: Instruction limit
% 19.62/3.63 % (2475962)Termination phase: Saturation
% 19.62/3.63 % (2475962)Time elapsed: 0.159 s
% 19.62/3.63 % (2475962)Peak memory usage: 90 MB
% 19.62/3.63 % (2475962)Instructions burned: 264 (million)
% 19.62/3.63 % (2475966)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=2618465667:i=3256:kws=precedence:bd=preordered:av=off_2981 on theBenchmark for (2981ds/3256Mi)
% 19.62/3.63 % (2475967)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1282353809:i=537:av=off:ss=included_2980 on theBenchmark for (2980ds/537Mi)
% 19.62/3.63 % (2475967)Instruction limit reached!
% 19.62/3.63 % (2475967)------------------------------
% 19.62/3.63 % (2475967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.62/3.63 % (2475967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.62/3.63 % (2475967)CaDiCaL version: 2.1.3
% 19.62/3.63 % (2475967)Termination reason: Instruction limit
% 19.62/3.63 % (2475967)Termination phase: Saturation
% 19.62/3.63 % (2475967)Time elapsed: 0.277 s
% 19.62/3.63 % (2475967)Peak memory usage: 90 MB
% 19.62/3.63 % (2475967)Instructions burned: 539 (million)
% 19.62/3.63 % (2475944)First to succeed.
% 19.62/3.63 % (2475944)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2475915"
% 19.62/3.63 % (2475970)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=405831486:i=180:bd=preordered:av=off_2976 on theBenchmark for (2976ds/180Mi)
% 19.62/3.63 % (2475970)Instruction limit reached!
% 19.62/3.63 % (2475970)------------------------------
% 19.62/3.63 % (2475970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.62/3.63 % (2475970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.62/3.63 % (2475970)CaDiCaL version: 2.1.3
% 19.62/3.63 % (2475970)Termination reason: Instruction limit
% 19.62/3.63 % (2475970)Termination phase: Saturation
% 19.62/3.63 % (2475970)Time elapsed: 0.091 s
% 19.62/3.63 % (2475970)Peak memory usage: 87 MB
% 19.62/3.63 % (2475970)Instructions burned: 182 (million)
% 19.62/3.63 % (2475944)Refutation found. Thanks to Tanya!
% 19.62/3.63 % SZS status Unsatisfiable for theBenchmark
% 19.62/3.63 % SZS output start Proof for theBenchmark
% See solution above
% 20.19/3.83 % (2475944)------------------------------
% 20.19/3.83 % (2475944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.19/3.83 % (2475944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.19/3.83 % (2475944)CaDiCaL version: 2.1.3
% 20.19/3.83 % (2475944)Termination reason: Refutation
% 20.19/3.83 % (2475944)Time elapsed: 1.692 s
% 20.19/3.83 % (2475944)Peak memory usage: 141 MB
% 20.19/3.83 % (2475944)Instructions burned: 2457 (million)
% 20.19/3.83 % (2475944)------------------------------
% 20.19/3.83 % (2475944)------------------------------
% 20.19/3.83 % (2475915)Success in time 2.772 s
% 20.19/3.83 % Vampire exiting
%------------------------------------------------------------------------------