%------------------------------------------------------------------------------
% File : Vampire-SAT---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/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:32:00 PM UTC 2026
% Result : Unsatisfiable 3.21s 0.92s
% Output : Refutation 3.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 42
% Syntax : Number of formulae : 313 ( 55 unt; 24 def)
% Number of atoms : 876 ( 0 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 1058 ( 495 ~; 539 |; 0 &)
% ( 24 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 13 ( 3 avg)
% Number of predicates : 34 ( 33 usr; 25 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 279 ( 0 sgn 279 !; 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/sandbox/benchmark/theBenchmark.p',make_list_of_numbers1) ).
fof(f2,axiom,
! [X0] : range(X0,X0,cons(X0,empty_list)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',make_list_of_numbers2) ).
fof(f3,axiom,
! [X0] : less(n0,s(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less1) ).
fof(f4,axiom,
! [X0,X1] :
( less(s(X0),s(X1))
| ~ less(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',less2) ).
fof(f5,axiom,
! [X0] : sum(X0,n0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',add_0) ).
fof(f6,axiom,
! [X2,X0,X1] :
( sum(X0,s(X1),s(X2))
| ~ sum(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',add) ).
fof(f7,axiom,
! [X0,X1] : select(X0,cons(X0,X1),X1),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',select2) ).
fof(f9,axiom,
! [X0] : ~ same(s(X0),n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',same_definition1) ).
fof(f10,axiom,
! [X0] : ~ same(n0,s(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',same_definition2) ).
fof(f11,axiom,
! [X0,X1] :
( ~ same(s(X0),s(X1))
| same(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',same_definition3) ).
fof(f12,axiom,
! [X0,X1] :
( diagonal_attack(X0,s(n0),X1)
| ~ attack(X0,X1) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',check_diagonals1) ).
fof(f14,axiom,
! [X0,X1] : ~ diagonal_attack(X0,X1,empty_list),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',place_a_queen1) ).
fof(f16,axiom,
! [X0] : do_queens(empty_list,X0,X0),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',set_up_queens) ).
fof(f18,negated_conjecture,
! [X0] : ~ queens(s(s(s(s(n0)))),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',place_queens) ).
fof(f19,plain,
! [X0] : ~ attack(X0,empty_list),
inference(resolution,[],[f12,f14]) ).
fof(f20,plain,
! [X2,X3,X0,X1,X4] :
( ~ range(s(X1),X3,X4)
| queens(X0,X2)
| ~ sum(X0,X0,X3)
| ~ sum(X0,n0,X1)
| ~ do_queens(X4,empty_list,X2) ),
inference(resolution,[],[f6,f17]) ).
fof(f22,plain,
! [X2,X0,X1] :
( do_queens(X1,X2,cons(X0,X2))
| attack(X0,X2)
| ~ select(X0,X1,empty_list) ),
inference(resolution,[],[f15,f16]) ).
fof(f24,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,[],[f22,f15]) ).
fof(f26,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(f27,plain,
! [X0,X1] :
( range(X0,s(X1),cons(X0,cons(s(X1),empty_list)))
| ~ less(X0,s(X1))
| ~ sum(X0,n0,X1) ),
inference(resolution,[],[f26,f2]) ).
fof(f30,plain,
! [X2,X0,X1] :
( ~ less(s(X0),s(X1))
| ~ sum(s(X0),n0,X1)
| range(X2,s(X1),cons(X2,cons(s(X0),cons(s(X1),empty_list))))
| ~ less(X2,s(X1))
| ~ sum(X2,n0,X0) ),
inference(resolution,[],[f27,f26]) ).
fof(f36,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ select(X0,cons(X1,X2),empty_list)
| attack(X0,cons(X3,X4))
| attack(X3,X4)
| do_queens(cons(X1,X5),X4,cons(X0,cons(X3,X4)))
| ~ select(X3,X5,X2) ),
inference(resolution,[],[f24,f8]) ).
fof(f60,plain,
! [X2,X3,X0,X1] :
( do_queens(cons(X0,X3),X2,cons(X0,cons(X1,X2)))
| attack(X1,X2)
| attack(X0,cons(X1,X2))
| ~ select(X1,X3,empty_list) ),
inference(resolution,[],[f36,f7]) ).
fof(f65,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ select(X0,X4,empty_list)
| attack(X3,cons(X0,cons(X1,X2)))
| attack(X0,cons(X1,X2))
| ~ select(X1,X5,cons(X3,X4))
| attack(X1,X2)
| do_queens(X5,X2,cons(X3,cons(X0,cons(X1,X2)))) ),
inference(resolution,[],[f60,f15]) ).
fof(f70,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(f73,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,[],[f70,f6]) ).
fof(f76,plain,
! [X2,X0,X1] :
( ~ sum(s(X0),n0,X1)
| range(X2,s(X1),cons(X2,cons(s(X0),cons(s(X1),empty_list))))
| ~ less(X2,s(X1))
| ~ sum(X2,n0,X0)
| ~ less(X0,X1) ),
inference(resolution,[],[f30,f4]) ).
fof(f77,plain,
! [X0,X1] :
( ~ sum(X0,n0,X1)
| ~ less(X0,s(s(X1)))
| range(X0,s(s(X1)),cons(X0,cons(s(X1),cons(s(s(X1)),empty_list))))
| ~ less(X1,s(X1)) ),
inference(resolution,[],[f76,f5]) ).
fof(f78,plain,
! [X0] :
( ~ less(X0,s(s(X0)))
| range(X0,s(s(X0)),cons(X0,cons(s(X0),cons(s(s(X0)),empty_list))))
| ~ less(X0,s(X0)) ),
inference(resolution,[],[f77,f5]) ).
fof(f80,plain,
! [X0] :
( ~ less(s(X0),s(s(X0)))
| range(s(X0),s(s(s(X0))),cons(s(X0),cons(s(s(X0)),cons(s(s(s(X0))),empty_list))))
| ~ less(X0,s(s(X0))) ),
inference(resolution,[],[f78,f4]) ).
fof(f86,plain,
! [X0] :
( range(s(X0),s(s(s(X0))),cons(s(X0),cons(s(s(X0)),cons(s(s(s(X0))),empty_list))))
| ~ less(X0,s(s(X0)))
| ~ less(X0,s(X0)) ),
inference(resolution,[],[f80,f4]) ).
fof(f87,plain,
! [X0,X1] :
( ~ sum(X1,n0,X0)
| ~ less(X0,s(X0))
| range(X1,s(s(s(X0))),cons(X1,cons(s(X0),cons(s(s(X0)),cons(s(s(s(X0))),empty_list)))))
| ~ less(X1,s(s(s(X0))))
| ~ less(X0,s(s(X0))) ),
inference(resolution,[],[f86,f26]) ).
fof(f92,definition,
( spl0_1
<=> less(s(s(s(s(n0)))),s(s(s(s(s(n0)))))) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f93,plain,
( less(s(s(s(s(n0)))),s(s(s(s(s(n0))))))
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f92]) ).
fof(f94,plain,
( ~ less(s(s(s(s(n0)))),s(s(s(s(s(n0))))))
| spl0_1 ),
inference(avatar_component_clause,[],[f92]) ).
fof(f106,plain,
( ~ less(s(s(s(n0))),s(s(s(s(n0)))))
| spl0_1 ),
inference(resolution,[],[f94,f4]) ).
fof(f107,plain,
( ~ less(s(s(n0)),s(s(s(n0))))
| spl0_1 ),
inference(resolution,[],[f106,f4]) ).
fof(f111,plain,
( ~ less(s(n0),s(s(n0)))
| spl0_1 ),
inference(resolution,[],[f107,f4]) ).
fof(f112,plain,
( ~ less(n0,s(n0))
| spl0_1 ),
inference(resolution,[],[f111,f4]) ).
fof(f113,plain,
( $false
| spl0_1 ),
inference(forward_subsumption_resolution,[],[f112,f3]) ).
fof(f114,plain,
spl0_1,
inference(avatar_contradiction_clause,[],[f113]) ).
fof(f122,definition,
( spl0_4
<=> less(s(s(s(n0))),s(s(s(s(s(n0)))))) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f123,plain,
( less(s(s(s(n0))),s(s(s(s(s(n0))))))
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f122]) ).
fof(f124,plain,
( ~ less(s(s(s(n0))),s(s(s(s(s(n0))))))
| spl0_4 ),
inference(avatar_component_clause,[],[f122]) ).
fof(f131,plain,
( ~ less(s(s(n0)),s(s(s(s(n0)))))
| spl0_4 ),
inference(resolution,[],[f124,f4]) ).
fof(f132,plain,
( ~ less(s(n0),s(s(s(n0))))
| spl0_4 ),
inference(resolution,[],[f131,f4]) ).
fof(f133,plain,
( ~ less(n0,s(s(n0)))
| spl0_4 ),
inference(resolution,[],[f132,f4]) ).
fof(f134,plain,
( $false
| spl0_4 ),
inference(forward_subsumption_resolution,[],[f133,f3]) ).
fof(f135,plain,
spl0_4,
inference(avatar_contradiction_clause,[],[f134]) ).
fof(f161,plain,
! [X2,X3,X0,X1,X4] :
( ~ select(X2,X4,cons(X0,cons(X1,empty_list)))
| attack(X1,cons(X2,X3))
| attack(X0,cons(X1,cons(X2,X3)))
| attack(X2,X3)
| do_queens(X4,X3,cons(X0,cons(X1,cons(X2,X3)))) ),
inference(resolution,[],[f65,f7]) ).
fof(f163,plain,
! [X2,X3,X0,X1] :
( do_queens(cons(X1,cons(X3,cons(X0,empty_list))),X2,cons(X3,cons(X0,cons(X1,X2))))
| attack(X3,cons(X0,cons(X1,X2)))
| attack(X1,X2)
| attack(X0,cons(X1,X2)) ),
inference(resolution,[],[f161,f7]) ).
fof(f169,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ select(X3,X5,cons(X2,cons(X0,cons(X1,empty_list))))
| attack(X2,cons(X3,X4))
| attack(X1,cons(X2,cons(X3,X4)))
| attack(X0,cons(X1,cons(X2,cons(X3,X4))))
| attack(X3,X4)
| do_queens(X5,X4,cons(X0,cons(X1,cons(X2,cons(X3,X4))))) ),
inference(resolution,[],[f163,f15]) ).
fof(f221,plain,
! [X0] :
( ~ less(X0,s(s(s(X0))))
| range(X0,s(s(s(X0))),cons(X0,cons(s(X0),cons(s(s(X0)),cons(s(s(s(X0))),empty_list)))))
| ~ less(X0,s(X0))
| ~ less(X0,s(s(X0))) ),
inference(resolution,[],[f87,f5]) ).
fof(f223,plain,
! [X0] :
( range(s(X0),s(s(s(s(X0)))),cons(s(X0),cons(s(s(X0)),cons(s(s(s(X0))),cons(s(s(s(s(X0)))),empty_list)))))
| ~ less(s(X0),s(s(X0)))
| ~ less(s(X0),s(s(s(X0))))
| ~ less(X0,s(s(s(X0)))) ),
inference(resolution,[],[f221,f4]) ).
fof(f249,definition,
( spl0_20
<=> less(s(n0),s(s(s(s(n0))))) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f250,plain,
( less(s(n0),s(s(s(s(n0)))))
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f249]) ).
fof(f251,plain,
( ~ less(s(n0),s(s(s(s(n0)))))
| spl0_20 ),
inference(avatar_component_clause,[],[f249]) ).
fof(f253,plain,
( ~ less(n0,s(s(s(n0))))
| spl0_20 ),
inference(resolution,[],[f251,f4]) ).
fof(f254,plain,
( $false
| spl0_20 ),
inference(forward_subsumption_resolution,[],[f253,f3]) ).
fof(f255,plain,
spl0_20,
inference(avatar_contradiction_clause,[],[f254]) ).
fof(f296,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ select(X1,X5,cons(X4,cons(X3,empty_list)))
| attack(X3,cons(X0,cons(X1,X2)))
| attack(X4,cons(X3,cons(X0,cons(X1,X2))))
| attack(X1,X2)
| do_queens(cons(X0,X5),X2,cons(X4,cons(X3,cons(X0,cons(X1,X2)))))
| attack(X0,cons(X1,X2)) ),
inference(resolution,[],[f169,f8]) ).
fof(f329,definition,
( spl0_32
<=> ! [X2] : ~ sum(s(n0),n0,X2) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f330,plain,
( ! [X2] : ~ sum(s(n0),n0,X2)
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f329]) ).
fof(f343,plain,
( $false
| ~ spl0_32 ),
inference(resolution,[],[f330,f5]) ).
fof(f344,plain,
~ spl0_32,
inference(avatar_contradiction_clause,[],[f343]) ).
fof(f351,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ select(X2,X5,cons(X0,empty_list))
| attack(X4,cons(X0,cons(X1,cons(X2,X3))))
| attack(X2,X3)
| do_queens(cons(X1,cons(X4,X5)),X3,cons(X4,cons(X0,cons(X1,cons(X2,X3)))))
| attack(X1,cons(X2,X3))
| attack(X0,cons(X1,cons(X2,X3))) ),
inference(resolution,[],[f296,f8]) ).
fof(f501,plain,
! [X2,X3,X0,X1,X4] :
( do_queens(cons(X2,cons(X0,cons(X3,cons(X1,empty_list)))),X4,cons(X0,cons(X1,cons(X2,cons(X3,X4)))))
| attack(X3,X4)
| attack(X0,cons(X1,cons(X2,cons(X3,X4))))
| attack(X2,cons(X3,X4))
| attack(X1,cons(X2,cons(X3,X4))) ),
inference(resolution,[],[f351,f7]) ).
fof(f520,plain,
! [X2,X0,X1] :
( ~ sum(X1,n0,X0)
| ~ less(s(X0),s(s(s(X0))))
| ~ less(X0,s(s(s(X0))))
| queens(X1,X2)
| ~ sum(X1,X1,s(s(s(s(X0)))))
| ~ less(s(X0),s(s(X0)))
| ~ do_queens(cons(s(X0),cons(s(s(X0)),cons(s(s(s(X0))),cons(s(s(s(s(X0)))),empty_list)))),empty_list,X2) ),
inference(resolution,[],[f223,f20]) ).
fof(f1341,definition,
( spl0_167
<=> ! [X2] : ~ sum(s(s(n0)),s(n0),X2) ),
introduced(definition,[new_symbols(definition,[spl0_167])],[avatar_definition]) ).
fof(f1342,plain,
( ! [X2] : ~ sum(s(s(n0)),s(n0),X2)
| ~ spl0_167 ),
inference(avatar_component_clause,[],[f1341]) ).
fof(f1350,plain,
( ! [X0] : ~ sum(s(s(n0)),n0,X0)
| ~ spl0_167 ),
inference(resolution,[],[f1342,f6]) ).
fof(f1354,plain,
( $false
| ~ spl0_167 ),
inference(resolution,[],[f1350,f5]) ).
fof(f1355,plain,
~ spl0_167,
inference(avatar_contradiction_clause,[],[f1354]) ).
fof(f2073,plain,
! [X0,X1] :
( ~ sum(X0,X0,s(s(s(s(X0)))))
| ~ less(X0,s(s(s(X0))))
| queens(X0,X1)
| ~ less(s(X0),s(s(s(X0))))
| ~ less(s(X0),s(s(X0)))
| ~ do_queens(cons(s(X0),cons(s(s(X0)),cons(s(s(s(X0))),cons(s(s(s(s(X0)))),empty_list)))),empty_list,X1) ),
inference(resolution,[],[f520,f5]) ).
fof(f3588,plain,
! [X0,X1] :
( ~ sum(s(X0),X0,s(s(s(s(X0)))))
| queens(s(X0),X1)
| ~ less(s(s(X0)),s(s(s(s(X0)))))
| ~ less(s(s(X0)),s(s(s(X0))))
| ~ do_queens(cons(s(s(X0)),cons(s(s(s(X0))),cons(s(s(s(s(X0)))),cons(s(s(s(s(s(X0))))),empty_list)))),empty_list,X1)
| ~ less(s(X0),s(s(s(s(X0))))) ),
inference(resolution,[],[f2073,f6]) ).
fof(f3811,definition,
( spl0_469
<=> ! [X2] : ~ sum(s(s(s(n0))),s(n0),X2) ),
introduced(definition,[new_symbols(definition,[spl0_469])],[avatar_definition]) ).
fof(f3812,plain,
( ! [X2] : ~ sum(s(s(s(n0))),s(n0),X2)
| ~ spl0_469 ),
inference(avatar_component_clause,[],[f3811]) ).
fof(f3820,plain,
( ! [X0] : ~ sum(s(s(s(n0))),n0,X0)
| ~ spl0_469 ),
inference(resolution,[],[f3812,f6]) ).
fof(f3821,plain,
( $false
| ~ spl0_469 ),
inference(resolution,[],[f3820,f5]) ).
fof(f3822,plain,
~ spl0_469,
inference(avatar_contradiction_clause,[],[f3821]) ).
fof(f5340,plain,
! [X0,X1] :
( ~ less(s(s(X0)),s(s(s(s(s(X0))))))
| ~ less(s(s(s(X0))),s(s(s(s(s(X0))))))
| ~ less(s(s(s(X0))),s(s(s(s(X0)))))
| ~ do_queens(cons(s(s(s(X0))),cons(s(s(s(s(X0)))),cons(s(s(s(s(s(X0))))),cons(s(s(s(s(s(s(X0)))))),empty_list)))),empty_list,X1)
| queens(s(s(X0)),X1)
| ~ sum(s(s(X0)),X0,s(s(s(s(X0))))) ),
inference(resolution,[],[f3588,f6]) ).
fof(f5429,definition,
( spl0_665
<=> ! [X1] :
( ~ sum(s(s(s(s(s(n0))))),s(s(n0)),X1)
| same(X1,s(s(s(s(s(s(n0))))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_665])],[avatar_definition]) ).
fof(f5430,plain,
( ! [X1] :
( ~ sum(s(s(s(s(s(n0))))),s(s(n0)),X1)
| same(X1,s(s(s(s(s(s(n0))))))) )
| ~ spl0_665 ),
inference(avatar_component_clause,[],[f5429]) ).
fof(f5432,definition,
( spl0_666
<=> ! [X0] :
( ~ sum(X0,s(s(n0)),s(s(s(s(s(n0))))))
| same(X0,s(s(s(s(s(s(n0))))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_666])],[avatar_definition]) ).
fof(f5433,plain,
( ! [X0] :
( ~ sum(X0,s(s(n0)),s(s(s(s(s(n0))))))
| same(X0,s(s(s(s(s(s(n0))))))) )
| ~ spl0_666 ),
inference(avatar_component_clause,[],[f5432]) ).
fof(f5435,plain,
( ! [X0] :
( same(s(X0),s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(n0))))),s(n0),X0) )
| ~ spl0_665 ),
inference(resolution,[],[f5430,f6]) ).
fof(f5437,plain,
( ! [X0] :
( ~ sum(s(s(s(s(s(n0))))),s(n0),X0)
| same(X0,s(s(s(s(s(n0)))))) )
| ~ spl0_665 ),
inference(resolution,[],[f5435,f11]) ).
fof(f5438,plain,
( ! [X0] :
( same(s(X0),s(s(s(s(s(n0))))))
| ~ sum(s(s(s(s(s(n0))))),n0,X0) )
| ~ spl0_665 ),
inference(resolution,[],[f5437,f6]) ).
fof(f5439,plain,
( ! [X0] :
( ~ sum(s(s(s(s(s(n0))))),n0,X0)
| same(X0,s(s(s(s(n0))))) )
| ~ spl0_665 ),
inference(resolution,[],[f5438,f11]) ).
fof(f5445,plain,
( same(s(s(s(s(s(n0))))),s(s(s(s(n0)))))
| ~ spl0_665 ),
inference(resolution,[],[f5439,f5]) ).
fof(f5446,plain,
( same(s(s(s(s(n0)))),s(s(s(n0))))
| ~ spl0_665 ),
inference(resolution,[],[f5445,f11]) ).
fof(f5450,plain,
( same(s(s(s(n0))),s(s(n0)))
| ~ spl0_665 ),
inference(resolution,[],[f5446,f11]) ).
fof(f5451,plain,
( same(s(s(n0)),s(n0))
| ~ spl0_665 ),
inference(resolution,[],[f5450,f11]) ).
fof(f5452,plain,
( same(s(n0),n0)
| ~ spl0_665 ),
inference(resolution,[],[f5451,f11]) ).
fof(f5453,plain,
( $false
| ~ spl0_665 ),
inference(forward_subsumption_resolution,[],[f5452,f9]) ).
fof(f5454,plain,
~ spl0_665,
inference(avatar_contradiction_clause,[],[f5453]) ).
fof(f5455,plain,
( ! [X0] :
( ~ sum(X0,s(n0),s(s(s(s(n0)))))
| same(X0,s(s(s(s(s(s(n0))))))) )
| ~ spl0_666 ),
inference(resolution,[],[f5433,f6]) ).
fof(f5456,plain,
( ! [X0] :
( ~ sum(X0,n0,s(s(s(n0))))
| same(X0,s(s(s(s(s(s(n0))))))) )
| ~ spl0_666 ),
inference(resolution,[],[f5455,f6]) ).
fof(f5460,plain,
( same(s(s(s(n0))),s(s(s(s(s(s(n0)))))))
| ~ spl0_666 ),
inference(resolution,[],[f5456,f5]) ).
fof(f5461,plain,
( same(s(s(n0)),s(s(s(s(s(n0))))))
| ~ spl0_666 ),
inference(resolution,[],[f5460,f11]) ).
fof(f5462,plain,
( same(s(n0),s(s(s(s(n0)))))
| ~ spl0_666 ),
inference(resolution,[],[f5461,f11]) ).
fof(f5469,plain,
( same(n0,s(s(s(n0))))
| ~ spl0_666 ),
inference(resolution,[],[f5462,f11]) ).
fof(f5470,plain,
( $false
| ~ spl0_666 ),
inference(forward_subsumption_resolution,[],[f5469,f10]) ).
fof(f5471,plain,
~ spl0_666,
inference(avatar_contradiction_clause,[],[f5470]) ).
fof(f6106,plain,
! [X0,X1] :
( ~ sum(s(s(X0)),X0,s(s(s(s(X0)))))
| ~ less(s(s(s(X0))),s(s(s(s(X0)))))
| ~ do_queens(cons(s(s(s(X0))),cons(s(s(s(s(X0)))),cons(s(s(s(s(s(X0))))),cons(s(s(s(s(s(s(X0)))))),empty_list)))),empty_list,X1)
| queens(s(s(X0)),X1)
| ~ less(s(s(s(X0))),s(s(s(s(s(X0))))))
| ~ less(s(X0),s(s(s(s(X0))))) ),
inference(resolution,[],[f5340,f4]) ).
fof(f6779,plain,
! [X0,X1] :
( ~ less(s(s(s(s(X0)))),s(s(s(s(s(s(X0)))))))
| ~ do_queens(cons(s(s(s(s(X0)))),cons(s(s(s(s(s(X0))))),cons(s(s(s(s(s(s(X0)))))),cons(s(s(s(s(s(s(s(X0))))))),empty_list)))),empty_list,X1)
| queens(s(s(s(X0))),X1)
| ~ less(s(s(s(s(X0)))),s(s(s(s(s(X0))))))
| ~ less(s(s(X0)),s(s(s(s(s(X0))))))
| ~ sum(s(s(s(X0))),X0,s(s(s(s(X0))))) ),
inference(resolution,[],[f6106,f6]) ).
fof(f7008,plain,
! [X0,X1] :
( ~ less(s(s(X0)),s(s(s(s(s(X0))))))
| queens(s(s(s(X0))),X1)
| ~ less(s(s(s(s(X0)))),s(s(s(s(s(X0))))))
| ~ do_queens(cons(s(s(s(s(X0)))),cons(s(s(s(s(s(X0))))),cons(s(s(s(s(s(s(X0)))))),cons(s(s(s(s(s(s(s(X0))))))),empty_list)))),empty_list,X1)
| ~ sum(s(s(s(X0))),X0,s(s(s(s(X0)))))
| ~ less(s(s(s(X0))),s(s(s(s(s(X0)))))) ),
inference(resolution,[],[f6779,f4]) ).
fof(f7009,plain,
! [X0,X1] :
( ~ sum(s(s(s(X0))),X0,s(s(s(s(X0)))))
| ~ less(s(s(s(s(X0)))),s(s(s(s(s(X0))))))
| ~ do_queens(cons(s(s(s(s(X0)))),cons(s(s(s(s(s(X0))))),cons(s(s(s(s(s(s(X0)))))),cons(s(s(s(s(s(s(s(X0))))))),empty_list)))),empty_list,X1)
| queens(s(s(s(X0))),X1)
| ~ less(s(s(s(X0))),s(s(s(s(s(X0))))))
| ~ less(s(X0),s(s(s(s(X0))))) ),
inference(resolution,[],[f7008,f4]) ).
fof(f7016,plain,
! [X0,X1] :
( ~ less(s(s(s(s(s(X0))))),s(s(s(s(s(s(X0)))))))
| ~ do_queens(cons(s(s(s(s(s(X0))))),cons(s(s(s(s(s(s(X0)))))),cons(s(s(s(s(s(s(s(X0))))))),cons(s(s(s(s(s(s(s(s(X0)))))))),empty_list)))),empty_list,X1)
| queens(s(s(s(s(X0)))),X1)
| ~ less(s(s(s(s(X0)))),s(s(s(s(s(s(X0)))))))
| ~ less(s(s(X0)),s(s(s(s(s(X0))))))
| ~ sum(s(s(s(s(X0)))),X0,s(s(s(s(X0))))) ),
inference(resolution,[],[f7009,f6]) ).
fof(f7045,plain,
! [X0,X1] :
( ~ less(s(s(s(s(X0)))),s(s(s(s(s(s(X0)))))))
| queens(s(s(s(s(X0)))),X1)
| ~ do_queens(cons(s(s(s(s(s(X0))))),cons(s(s(s(s(s(s(X0)))))),cons(s(s(s(s(s(s(s(X0))))))),cons(s(s(s(s(s(s(s(s(X0)))))))),empty_list)))),empty_list,X1)
| ~ less(s(s(X0)),s(s(s(s(s(X0))))))
| ~ sum(s(s(s(s(X0)))),X0,s(s(s(s(X0)))))
| ~ less(s(s(s(s(X0)))),s(s(s(s(s(X0)))))) ),
inference(resolution,[],[f7016,f4]) ).
fof(f7053,plain,
! [X0,X1] :
( ~ less(s(s(X0)),s(s(s(s(s(X0))))))
| ~ do_queens(cons(s(s(s(s(s(X0))))),cons(s(s(s(s(s(s(X0)))))),cons(s(s(s(s(s(s(s(X0))))))),cons(s(s(s(s(s(s(s(s(X0)))))))),empty_list)))),empty_list,X1)
| queens(s(s(s(s(X0)))),X1)
| ~ sum(s(s(s(s(X0)))),X0,s(s(s(s(X0)))))
| ~ less(s(s(s(s(X0)))),s(s(s(s(s(X0))))))
| ~ less(s(s(s(X0))),s(s(s(s(s(X0)))))) ),
inference(resolution,[],[f7045,f4]) ).
fof(f7054,plain,
! [X0,X1] :
( ~ less(s(s(s(s(X0)))),s(s(s(s(s(X0))))))
| queens(s(s(s(s(X0)))),X1)
| ~ sum(s(s(s(s(X0)))),X0,s(s(s(s(X0)))))
| ~ do_queens(cons(s(s(s(s(s(X0))))),cons(s(s(s(s(s(s(X0)))))),cons(s(s(s(s(s(s(s(X0))))))),cons(s(s(s(s(s(s(s(s(X0)))))))),empty_list)))),empty_list,X1)
| ~ less(s(s(s(X0))),s(s(s(s(s(X0))))))
| ~ less(s(X0),s(s(s(s(X0))))) ),
inference(resolution,[],[f7053,f4]) ).
fof(f7055,plain,
( ! [X0] :
( queens(s(s(s(s(n0)))),X0)
| ~ sum(s(s(s(s(n0)))),n0,s(s(s(s(n0)))))
| ~ do_queens(cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(n0)))))),cons(s(s(s(s(s(s(s(n0))))))),cons(s(s(s(s(s(s(s(s(n0)))))))),empty_list)))),empty_list,X0)
| ~ less(s(s(s(n0))),s(s(s(s(s(n0))))))
| ~ less(s(n0),s(s(s(s(n0))))) )
| ~ spl0_1 ),
inference(resolution,[],[f7054,f93]) ).
fof(f7057,plain,
( ! [X0] :
( queens(s(s(s(s(n0)))),X0)
| ~ do_queens(cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(n0)))))),cons(s(s(s(s(s(s(s(n0))))))),cons(s(s(s(s(s(s(s(s(n0)))))))),empty_list)))),empty_list,X0)
| ~ less(s(s(s(n0))),s(s(s(s(s(n0))))))
| ~ less(s(n0),s(s(s(s(n0))))) )
| ~ spl0_1 ),
inference(forward_subsumption_resolution,[],[f7055,f5]) ).
fof(f7058,plain,
( ! [X0] :
( queens(s(s(s(s(n0)))),X0)
| ~ do_queens(cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(n0)))))),cons(s(s(s(s(s(s(s(n0))))))),cons(s(s(s(s(s(s(s(s(n0)))))))),empty_list)))),empty_list,X0)
| ~ less(s(n0),s(s(s(s(n0))))) )
| ~ spl0_1
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f7057,f123]) ).
fof(f7059,plain,
( ! [X0] :
( queens(s(s(s(s(n0)))),X0)
| ~ do_queens(cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(n0)))))),cons(s(s(s(s(s(s(s(n0))))))),cons(s(s(s(s(s(s(s(s(n0)))))))),empty_list)))),empty_list,X0) )
| ~ spl0_1
| ~ spl0_4
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f7058,f250]) ).
fof(f7060,plain,
( ! [X0] : ~ do_queens(cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(n0)))))),cons(s(s(s(s(s(s(s(n0))))))),cons(s(s(s(s(s(s(s(s(n0)))))))),empty_list)))),empty_list,X0)
| ~ spl0_1
| ~ spl0_4
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f7059,f18]) ).
fof(f7079,plain,
( attack(s(s(s(s(s(s(s(n0))))))),empty_list)
| attack(s(s(s(s(s(s(n0)))))),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list))))
| attack(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| attack(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| ~ spl0_1
| ~ spl0_4
| ~ spl0_20 ),
inference(resolution,[],[f7060,f501]) ).
fof(f7098,plain,
( attack(s(s(s(s(s(s(n0)))))),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list))))
| attack(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| attack(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| ~ spl0_1
| ~ spl0_4
| ~ spl0_20 ),
inference(forward_subsumption_resolution,[],[f7079,f19]) ).
fof(f7204,definition,
( spl0_850
<=> attack(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list))) ),
introduced(definition,[new_symbols(definition,[spl0_850])],[avatar_definition]) ).
fof(f7206,plain,
( attack(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| ~ spl0_850 ),
inference(avatar_component_clause,[],[f7204]) ).
fof(f7208,definition,
( spl0_851
<=> attack(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)) ),
introduced(definition,[new_symbols(definition,[spl0_851])],[avatar_definition]) ).
fof(f7210,plain,
( attack(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| ~ spl0_851 ),
inference(avatar_component_clause,[],[f7208]) ).
fof(f7212,definition,
( spl0_852
<=> attack(s(s(s(s(s(s(n0)))))),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))) ),
introduced(definition,[new_symbols(definition,[spl0_852])],[avatar_definition]) ).
fof(f7214,plain,
( attack(s(s(s(s(s(s(n0)))))),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list))))
| ~ spl0_852 ),
inference(avatar_component_clause,[],[f7212]) ).
fof(f7215,plain,
( spl0_850
| spl0_851
| spl0_852
| ~ spl0_1
| ~ spl0_4
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f7098,f249,f122,f92,f7212,f7208,f7204]) ).
fof(f7347,definition,
( spl0_881
<=> ! [X1] :
( ~ sum(X1,s(n0),s(s(s(s(s(n0))))))
| same(X1,s(s(s(s(s(s(s(s(n0))))))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_881])],[avatar_definition]) ).
fof(f7348,plain,
( ! [X1] :
( ~ sum(X1,s(n0),s(s(s(s(s(n0))))))
| same(X1,s(s(s(s(s(s(s(s(n0))))))))) )
| ~ spl0_881 ),
inference(avatar_component_clause,[],[f7347]) ).
fof(f7350,definition,
( spl0_882
<=> ! [X0] :
( ~ sum(s(s(s(s(s(n0))))),s(n0),X0)
| same(X0,s(s(s(s(s(s(s(s(n0))))))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_882])],[avatar_definition]) ).
fof(f7351,plain,
( ! [X0] :
( ~ sum(s(s(s(s(s(n0))))),s(n0),X0)
| same(X0,s(s(s(s(s(s(s(s(n0))))))))) )
| ~ spl0_882 ),
inference(avatar_component_clause,[],[f7350]) ).
fof(f7356,definition,
( spl0_883
<=> ! [X1] :
( ~ sum(X1,s(n0),s(s(s(s(s(s(s(s(n0)))))))))
| same(X1,s(s(s(s(s(s(n0))))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_883])],[avatar_definition]) ).
fof(f7357,plain,
( ! [X1] :
( ~ sum(X1,s(n0),s(s(s(s(s(s(s(s(n0)))))))))
| same(X1,s(s(s(s(s(s(n0))))))) )
| ~ spl0_883 ),
inference(avatar_component_clause,[],[f7356]) ).
fof(f7359,definition,
( spl0_884
<=> ! [X0] :
( ~ sum(s(s(s(s(s(s(s(s(n0)))))))),s(n0),X0)
| same(X0,s(s(s(s(s(s(n0))))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_884])],[avatar_definition]) ).
fof(f7360,plain,
( ! [X0] :
( ~ sum(s(s(s(s(s(s(s(s(n0)))))))),s(n0),X0)
| same(X0,s(s(s(s(s(s(n0))))))) )
| ~ spl0_884 ),
inference(avatar_component_clause,[],[f7359]) ).
fof(f7466,plain,
( ! [X0] :
( ~ sum(X0,n0,s(s(s(s(n0)))))
| same(X0,s(s(s(s(s(s(s(s(n0))))))))) )
| ~ spl0_881 ),
inference(resolution,[],[f7348,f6]) ).
fof(f7467,plain,
( same(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(n0)))))))))
| ~ spl0_881 ),
inference(resolution,[],[f7466,f5]) ).
fof(f7468,plain,
( same(s(s(s(n0))),s(s(s(s(s(s(s(n0))))))))
| ~ spl0_881 ),
inference(resolution,[],[f7467,f11]) ).
fof(f7469,plain,
( same(s(s(n0)),s(s(s(s(s(s(n0)))))))
| ~ spl0_881 ),
inference(resolution,[],[f7468,f11]) ).
fof(f7470,plain,
( same(s(n0),s(s(s(s(s(n0))))))
| ~ spl0_881 ),
inference(resolution,[],[f7469,f11]) ).
fof(f7494,plain,
( same(n0,s(s(s(s(n0)))))
| ~ spl0_881 ),
inference(resolution,[],[f7470,f11]) ).
fof(f7495,plain,
( $false
| ~ spl0_881 ),
inference(forward_subsumption_resolution,[],[f7494,f10]) ).
fof(f7496,plain,
~ spl0_881,
inference(avatar_contradiction_clause,[],[f7495]) ).
fof(f7567,plain,
( ! [X0] :
( same(s(X0),s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(s(n0))))),n0,X0) )
| ~ spl0_882 ),
inference(resolution,[],[f7351,f6]) ).
fof(f7612,plain,
( ! [X0] :
( ~ sum(s(s(s(s(s(n0))))),n0,X0)
| same(X0,s(s(s(s(s(s(s(n0)))))))) )
| ~ spl0_882 ),
inference(resolution,[],[f7567,f11]) ).
fof(f7615,plain,
( same(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(n0))))))))
| ~ spl0_882 ),
inference(resolution,[],[f7612,f5]) ).
fof(f7616,plain,
( same(s(s(s(s(n0)))),s(s(s(s(s(s(n0)))))))
| ~ spl0_882 ),
inference(resolution,[],[f7615,f11]) ).
fof(f7617,plain,
( same(s(s(s(n0))),s(s(s(s(s(n0))))))
| ~ spl0_882 ),
inference(resolution,[],[f7616,f11]) ).
fof(f7622,plain,
( same(s(s(n0)),s(s(s(s(n0)))))
| ~ spl0_882 ),
inference(resolution,[],[f7617,f11]) ).
fof(f7625,plain,
( same(s(n0),s(s(s(n0))))
| ~ spl0_882 ),
inference(resolution,[],[f7622,f11]) ).
fof(f7626,plain,
( same(n0,s(s(n0)))
| ~ spl0_882 ),
inference(resolution,[],[f7625,f11]) ).
fof(f7627,plain,
( $false
| ~ spl0_882 ),
inference(forward_subsumption_resolution,[],[f7626,f10]) ).
fof(f7628,plain,
~ spl0_882,
inference(avatar_contradiction_clause,[],[f7627]) ).
fof(f7631,plain,
( ! [X0] :
( ~ sum(X0,n0,s(s(s(s(s(s(s(n0))))))))
| same(X0,s(s(s(s(s(s(n0))))))) )
| ~ spl0_883 ),
inference(resolution,[],[f7357,f6]) ).
fof(f7632,plain,
( same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(n0)))))))
| ~ spl0_883 ),
inference(resolution,[],[f7631,f5]) ).
fof(f7673,plain,
( same(s(s(s(s(s(s(n0)))))),s(s(s(s(s(n0))))))
| ~ spl0_883 ),
inference(resolution,[],[f7632,f11]) ).
fof(f7674,plain,
( same(s(s(s(s(s(n0))))),s(s(s(s(n0)))))
| ~ spl0_883 ),
inference(resolution,[],[f7673,f11]) ).
fof(f7675,plain,
( same(s(s(s(s(n0)))),s(s(s(n0))))
| ~ spl0_883 ),
inference(resolution,[],[f7674,f11]) ).
fof(f7676,plain,
( same(s(s(s(n0))),s(s(n0)))
| ~ spl0_883 ),
inference(resolution,[],[f7675,f11]) ).
fof(f7679,plain,
( same(s(s(n0)),s(n0))
| ~ spl0_883 ),
inference(resolution,[],[f7676,f11]) ).
fof(f7680,plain,
( same(s(n0),n0)
| ~ spl0_883 ),
inference(resolution,[],[f7679,f11]) ).
fof(f7681,plain,
( $false
| ~ spl0_883 ),
inference(forward_subsumption_resolution,[],[f7680,f9]) ).
fof(f7682,plain,
~ spl0_883,
inference(avatar_contradiction_clause,[],[f7681]) ).
fof(f7690,plain,
( ! [X0] :
( ~ sum(s(s(s(s(s(s(s(s(n0)))))))),n0,X0)
| same(s(X0),s(s(s(s(s(s(n0))))))) )
| ~ spl0_884 ),
inference(resolution,[],[f7360,f6]) ).
fof(f7713,plain,
( same(s(s(s(s(s(s(s(s(s(n0))))))))),s(s(s(s(s(s(n0)))))))
| ~ spl0_884 ),
inference(resolution,[],[f7690,f5]) ).
fof(f7714,plain,
( same(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(n0))))))
| ~ spl0_884 ),
inference(resolution,[],[f7713,f11]) ).
fof(f7715,plain,
( same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(n0)))))
| ~ spl0_884 ),
inference(resolution,[],[f7714,f11]) ).
fof(f7716,plain,
( same(s(s(s(s(s(s(n0)))))),s(s(s(n0))))
| ~ spl0_884 ),
inference(resolution,[],[f7715,f11]) ).
fof(f7717,plain,
( same(s(s(s(s(s(n0))))),s(s(n0)))
| ~ spl0_884 ),
inference(resolution,[],[f7716,f11]) ).
fof(f7718,plain,
( same(s(s(s(s(n0)))),s(n0))
| ~ spl0_884 ),
inference(resolution,[],[f7717,f11]) ).
fof(f7719,plain,
( same(s(s(s(n0))),n0)
| ~ spl0_884 ),
inference(resolution,[],[f7718,f11]) ).
fof(f7720,plain,
( $false
| ~ spl0_884 ),
inference(forward_subsumption_resolution,[],[f7719,f9]) ).
fof(f7721,plain,
~ spl0_884,
inference(avatar_contradiction_clause,[],[f7720]) ).
fof(f7816,plain,
( ! [X2,X0,X1] :
( ~ sum(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(n0))))))
| diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(X2),cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| same(X1,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(n0),n0,X2) )
| ~ spl0_850 ),
inference(resolution,[],[f7206,f73]) ).
fof(f7818,definition,
( spl0_927
<=> ! [X2] :
( diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(X2),cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| ~ sum(s(n0),n0,X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_927])],[avatar_definition]) ).
fof(f7819,plain,
( ! [X2] :
( diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(X2),cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| ~ sum(s(n0),n0,X2) )
| ~ spl0_927 ),
inference(avatar_component_clause,[],[f7818]) ).
fof(f7820,plain,
( spl0_927
| spl0_881
| spl0_882
| ~ spl0_850 ),
inference(avatar_split_clause,[],[f7816,f7204,f7350,f7347,f7818]) ).
fof(f7826,plain,
( ! [X2,X3,X0,X1] :
( ~ sum(s(n0),n0,X0)
| ~ sum(X1,s(X0),s(s(s(s(s(s(s(n0))))))))
| same(X1,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(X0),X2)
| same(X2,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(X0),s(n0),X3)
| diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),X3,empty_list) )
| ~ spl0_927 ),
inference(resolution,[],[f7819,f13]) ).
fof(f7827,plain,
( ! [X2,X3,X0,X1] :
( ~ sum(s(n0),n0,X0)
| ~ sum(X1,s(X0),s(s(s(s(s(s(s(n0))))))))
| same(X1,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(X0),X2)
| same(X2,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(X0),s(n0),X3) )
| ~ spl0_927 ),
inference(forward_subsumption_resolution,[],[f7826,f14]) ).
fof(f7969,plain,
( ! [X2,X0,X1] :
( ~ sum(X0,s(s(n0)),s(s(s(s(s(s(s(n0))))))))
| same(X0,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(s(n0)),X1)
| same(X1,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(n0)),s(n0),X2) )
| ~ spl0_927 ),
inference(resolution,[],[f7827,f5]) ).
fof(f7971,definition,
( spl0_946
<=> ! [X1] :
( ~ sum(s(s(s(s(s(s(s(n0))))))),s(s(n0)),X1)
| same(X1,s(s(s(s(s(s(s(s(n0))))))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_946])],[avatar_definition]) ).
fof(f7972,plain,
( ! [X1] :
( ~ sum(s(s(s(s(s(s(s(n0))))))),s(s(n0)),X1)
| same(X1,s(s(s(s(s(s(s(s(n0))))))))) )
| ~ spl0_946 ),
inference(avatar_component_clause,[],[f7971]) ).
fof(f7974,definition,
( spl0_947
<=> ! [X0] :
( ~ sum(X0,s(s(n0)),s(s(s(s(s(s(s(n0))))))))
| same(X0,s(s(s(s(s(s(s(s(n0))))))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_947])],[avatar_definition]) ).
fof(f7975,plain,
( ! [X0] :
( ~ sum(X0,s(s(n0)),s(s(s(s(s(s(s(n0))))))))
| same(X0,s(s(s(s(s(s(s(s(n0))))))))) )
| ~ spl0_947 ),
inference(avatar_component_clause,[],[f7974]) ).
fof(f7976,plain,
( spl0_167
| spl0_946
| spl0_947
| ~ spl0_927 ),
inference(avatar_split_clause,[],[f7969,f7818,f7974,f7971,f1341]) ).
fof(f7977,plain,
( ! [X0] :
( same(s(X0),s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(n0),X0) )
| ~ spl0_946 ),
inference(resolution,[],[f7972,f6]) ).
fof(f7978,plain,
( ! [X0] :
( ~ sum(s(s(s(s(s(s(s(n0))))))),s(n0),X0)
| same(X0,s(s(s(s(s(s(s(n0)))))))) )
| ~ spl0_946 ),
inference(resolution,[],[f7977,f11]) ).
fof(f7979,plain,
( ! [X0] :
( same(s(X0),s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),n0,X0) )
| ~ spl0_946 ),
inference(resolution,[],[f7978,f6]) ).
fof(f7980,plain,
( ! [X0] :
( ~ sum(s(s(s(s(s(s(s(n0))))))),n0,X0)
| same(X0,s(s(s(s(s(s(n0))))))) )
| ~ spl0_946 ),
inference(resolution,[],[f7979,f11]) ).
fof(f7981,plain,
( same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(n0)))))))
| ~ spl0_946 ),
inference(resolution,[],[f7980,f5]) ).
fof(f7982,plain,
( same(s(s(s(s(s(s(n0)))))),s(s(s(s(s(n0))))))
| ~ spl0_946 ),
inference(resolution,[],[f7981,f11]) ).
fof(f7983,plain,
( same(s(s(s(s(s(n0))))),s(s(s(s(n0)))))
| ~ spl0_946 ),
inference(resolution,[],[f7982,f11]) ).
fof(f7984,plain,
( same(s(s(s(s(n0)))),s(s(s(n0))))
| ~ spl0_946 ),
inference(resolution,[],[f7983,f11]) ).
fof(f7985,plain,
( same(s(s(s(n0))),s(s(n0)))
| ~ spl0_946 ),
inference(resolution,[],[f7984,f11]) ).
fof(f7986,plain,
( same(s(s(n0)),s(n0))
| ~ spl0_946 ),
inference(resolution,[],[f7985,f11]) ).
fof(f7987,plain,
( same(s(n0),n0)
| ~ spl0_946 ),
inference(resolution,[],[f7986,f11]) ).
fof(f7988,plain,
( $false
| ~ spl0_946 ),
inference(forward_subsumption_resolution,[],[f7987,f9]) ).
fof(f7989,plain,
~ spl0_946,
inference(avatar_contradiction_clause,[],[f7988]) ).
fof(f8027,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_947 ),
inference(resolution,[],[f7975,f6]) ).
fof(f8028,plain,
( ! [X0] :
( ~ sum(X0,n0,s(s(s(s(s(n0))))))
| same(X0,s(s(s(s(s(s(s(s(n0))))))))) )
| ~ spl0_947 ),
inference(resolution,[],[f8027,f6]) ).
fof(f8029,plain,
( same(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(s(n0)))))))))
| ~ spl0_947 ),
inference(resolution,[],[f8028,f5]) ).
fof(f8030,plain,
( same(s(s(s(s(n0)))),s(s(s(s(s(s(s(n0))))))))
| ~ spl0_947 ),
inference(resolution,[],[f8029,f11]) ).
fof(f8031,plain,
( same(s(s(s(n0))),s(s(s(s(s(s(n0)))))))
| ~ spl0_947 ),
inference(resolution,[],[f8030,f11]) ).
fof(f8032,plain,
( same(s(s(n0)),s(s(s(s(s(n0))))))
| ~ spl0_947 ),
inference(resolution,[],[f8031,f11]) ).
fof(f8033,plain,
( same(s(n0),s(s(s(s(n0)))))
| ~ spl0_947 ),
inference(resolution,[],[f8032,f11]) ).
fof(f8034,plain,
( same(n0,s(s(s(n0))))
| ~ spl0_947 ),
inference(resolution,[],[f8033,f11]) ).
fof(f8035,plain,
( $false
| ~ spl0_947 ),
inference(forward_subsumption_resolution,[],[f8034,f10]) ).
fof(f8036,plain,
~ spl0_947,
inference(avatar_contradiction_clause,[],[f8035]) ).
fof(f8037,plain,
( ! [X2,X0,X1] :
( ~ sum(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(n0))))))))
| diagonal_attack(s(s(s(s(s(n0))))),s(X2),empty_list)
| same(X1,s(s(s(s(s(n0))))))
| ~ sum(s(n0),n0,X2) )
| ~ spl0_851 ),
inference(resolution,[],[f7210,f73]) ).
fof(f8038,plain,
( ! [X2,X0,X1] :
( ~ sum(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(n0))))))))
| same(X1,s(s(s(s(s(n0))))))
| ~ sum(s(n0),n0,X2) )
| ~ spl0_851 ),
inference(forward_subsumption_resolution,[],[f8037,f14]) ).
fof(f8040,definition,
( spl0_952
<=> ! [X1] :
( ~ sum(X1,s(n0),s(s(s(s(s(s(s(n0))))))))
| same(X1,s(s(s(s(s(n0)))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_952])],[avatar_definition]) ).
fof(f8041,plain,
( ! [X1] :
( ~ sum(X1,s(n0),s(s(s(s(s(s(s(n0))))))))
| same(X1,s(s(s(s(s(n0)))))) )
| ~ spl0_952 ),
inference(avatar_component_clause,[],[f8040]) ).
fof(f8043,definition,
( spl0_953
<=> ! [X0] :
( ~ sum(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_953])],[avatar_definition]) ).
fof(f8044,plain,
( ! [X0] :
( ~ sum(s(s(s(s(s(s(s(n0))))))),s(n0),X0)
| same(X0,s(s(s(s(s(n0)))))) )
| ~ spl0_953 ),
inference(avatar_component_clause,[],[f8043]) ).
fof(f8045,plain,
( spl0_32
| spl0_952
| spl0_953
| ~ spl0_851 ),
inference(avatar_split_clause,[],[f8038,f7208,f8043,f8040,f329]) ).
fof(f8047,plain,
( ! [X0] :
( ~ sum(X0,n0,s(s(s(s(s(s(n0)))))))
| same(X0,s(s(s(s(s(n0)))))) )
| ~ spl0_952 ),
inference(resolution,[],[f8041,f6]) ).
fof(f8048,plain,
( same(s(s(s(s(s(s(n0)))))),s(s(s(s(s(n0))))))
| ~ spl0_952 ),
inference(resolution,[],[f8047,f5]) ).
fof(f8053,plain,
( same(s(s(s(s(s(n0))))),s(s(s(s(n0)))))
| ~ spl0_952 ),
inference(resolution,[],[f8048,f11]) ).
fof(f8054,plain,
( same(s(s(s(s(n0)))),s(s(s(n0))))
| ~ spl0_952 ),
inference(resolution,[],[f8053,f11]) ).
fof(f8055,plain,
( same(s(s(s(n0))),s(s(n0)))
| ~ spl0_952 ),
inference(resolution,[],[f8054,f11]) ).
fof(f8056,plain,
( same(s(s(n0)),s(n0))
| ~ spl0_952 ),
inference(resolution,[],[f8055,f11]) ).
fof(f8061,plain,
( same(s(n0),n0)
| ~ spl0_952 ),
inference(resolution,[],[f8056,f11]) ).
fof(f8062,plain,
( $false
| ~ spl0_952 ),
inference(forward_subsumption_resolution,[],[f8061,f9]) ).
fof(f8063,plain,
~ spl0_952,
inference(avatar_contradiction_clause,[],[f8062]) ).
fof(f8064,plain,
( ! [X0] :
( ~ sum(s(s(s(s(s(s(s(n0))))))),n0,X0)
| same(s(X0),s(s(s(s(s(n0)))))) )
| ~ spl0_953 ),
inference(resolution,[],[f8044,f6]) ).
fof(f8067,plain,
( same(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(n0))))))
| ~ spl0_953 ),
inference(resolution,[],[f8064,f5]) ).
fof(f8071,plain,
( same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(n0)))))
| ~ spl0_953 ),
inference(resolution,[],[f8067,f11]) ).
fof(f8076,plain,
( same(s(s(s(s(s(s(n0)))))),s(s(s(n0))))
| ~ spl0_953 ),
inference(resolution,[],[f8071,f11]) ).
fof(f8077,plain,
( same(s(s(s(s(s(n0))))),s(s(n0)))
| ~ spl0_953 ),
inference(resolution,[],[f8076,f11]) ).
fof(f8078,plain,
( same(s(s(s(s(n0)))),s(n0))
| ~ spl0_953 ),
inference(resolution,[],[f8077,f11]) ).
fof(f8081,plain,
( same(s(s(s(n0))),n0)
| ~ spl0_953 ),
inference(resolution,[],[f8078,f11]) ).
fof(f8082,plain,
( $false
| ~ spl0_953 ),
inference(forward_subsumption_resolution,[],[f8081,f9]) ).
fof(f8083,plain,
~ spl0_953,
inference(avatar_contradiction_clause,[],[f8082]) ).
fof(f8139,plain,
( ! [X2,X0,X1] :
( ~ sum(s(s(s(s(s(s(s(s(n0)))))))),s(n0),X0)
| same(X0,s(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(s(n0)))))),s(X2),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| same(X1,s(s(s(s(s(s(n0)))))))
| ~ sum(s(n0),n0,X2) )
| ~ spl0_852 ),
inference(resolution,[],[f7214,f73]) ).
fof(f8141,definition,
( spl0_962
<=> ! [X2] :
( diagonal_attack(s(s(s(s(s(s(n0)))))),s(X2),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| ~ sum(s(n0),n0,X2) ) ),
introduced(definition,[new_symbols(definition,[spl0_962])],[avatar_definition]) ).
fof(f8142,plain,
( ! [X2] :
( diagonal_attack(s(s(s(s(s(s(n0)))))),s(X2),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| ~ sum(s(n0),n0,X2) )
| ~ spl0_962 ),
inference(avatar_component_clause,[],[f8141]) ).
fof(f8143,plain,
( spl0_962
| spl0_883
| spl0_884
| ~ spl0_852 ),
inference(avatar_split_clause,[],[f8139,f7212,f7359,f7356,f8141]) ).
fof(f8146,plain,
( ! [X2,X3,X0,X1] :
( ~ sum(s(n0),n0,X0)
| ~ sum(X1,s(X0),s(s(s(s(s(n0))))))
| same(X1,s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(n0))))),s(X0),X2)
| same(X2,s(s(s(s(s(s(n0)))))))
| ~ sum(s(X0),s(n0),X3)
| diagonal_attack(s(s(s(s(s(s(n0)))))),X3,cons(s(s(s(s(s(s(s(n0))))))),empty_list)) )
| ~ spl0_962 ),
inference(resolution,[],[f8142,f13]) ).
fof(f8147,plain,
( ! [X2,X0,X1] :
( ~ sum(X0,s(s(n0)),s(s(s(s(s(n0))))))
| same(X0,s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(n0))))),s(s(n0)),X1)
| same(X1,s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(n0)),s(n0),X2)
| diagonal_attack(s(s(s(s(s(s(n0)))))),X2,cons(s(s(s(s(s(s(s(n0))))))),empty_list)) )
| ~ spl0_962 ),
inference(resolution,[],[f8146,f5]) ).
fof(f8149,definition,
( spl0_963
<=> ! [X2] :
( ~ sum(s(s(n0)),s(n0),X2)
| diagonal_attack(s(s(s(s(s(s(n0)))))),X2,cons(s(s(s(s(s(s(s(n0))))))),empty_list)) ) ),
introduced(definition,[new_symbols(definition,[spl0_963])],[avatar_definition]) ).
fof(f8150,plain,
( ! [X2] :
( diagonal_attack(s(s(s(s(s(s(n0)))))),X2,cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| ~ sum(s(s(n0)),s(n0),X2) )
| ~ spl0_963 ),
inference(avatar_component_clause,[],[f8149]) ).
fof(f8151,plain,
( spl0_963
| spl0_665
| spl0_666
| ~ spl0_962 ),
inference(avatar_split_clause,[],[f8147,f8141,f5432,f5429,f8149]) ).
fof(f8152,plain,
( ! [X2,X3,X0,X1] :
( ~ sum(s(s(n0)),s(n0),X0)
| ~ sum(X1,X0,s(s(s(s(s(s(s(n0))))))))
| same(X1,s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),X0,X2)
| same(X2,s(s(s(s(s(s(n0)))))))
| ~ sum(X0,s(n0),X3)
| diagonal_attack(s(s(s(s(s(s(n0)))))),X3,empty_list) )
| ~ spl0_963 ),
inference(resolution,[],[f8150,f13]) ).
fof(f8153,plain,
( ! [X2,X3,X0,X1] :
( ~ sum(s(s(n0)),s(n0),X0)
| ~ sum(X1,X0,s(s(s(s(s(s(s(n0))))))))
| same(X1,s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),X0,X2)
| same(X2,s(s(s(s(s(s(n0)))))))
| ~ sum(X0,s(n0),X3) )
| ~ spl0_963 ),
inference(forward_subsumption_resolution,[],[f8152,f14]) ).
fof(f8156,plain,
( ! [X2,X3,X0,X1] :
( ~ sum(s(s(n0)),n0,X1)
| same(X0,s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(X1),X2)
| same(X2,s(s(s(s(s(s(n0)))))))
| ~ sum(s(X1),s(n0),X3)
| ~ sum(X0,s(X1),s(s(s(s(s(s(s(n0)))))))) )
| ~ spl0_963 ),
inference(resolution,[],[f8153,f6]) ).
fof(f8157,plain,
( ! [X2,X0,X1] :
( same(X0,s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(s(s(n0))),X1)
| same(X1,s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(n0))),s(n0),X2)
| ~ sum(X0,s(s(s(n0))),s(s(s(s(s(s(s(n0)))))))) )
| ~ spl0_963 ),
inference(resolution,[],[f8156,f5]) ).
fof(f8159,definition,
( spl0_964
<=> ! [X1] :
( ~ sum(s(s(s(s(s(s(s(n0))))))),s(s(s(n0))),X1)
| same(X1,s(s(s(s(s(s(n0))))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_964])],[avatar_definition]) ).
fof(f8160,plain,
( ! [X1] :
( ~ sum(s(s(s(s(s(s(s(n0))))))),s(s(s(n0))),X1)
| same(X1,s(s(s(s(s(s(n0))))))) )
| ~ spl0_964 ),
inference(avatar_component_clause,[],[f8159]) ).
fof(f8162,definition,
( spl0_965
<=> ! [X0] :
( same(X0,s(s(s(s(s(s(n0)))))))
| ~ sum(X0,s(s(s(n0))),s(s(s(s(s(s(s(n0)))))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_965])],[avatar_definition]) ).
fof(f8163,plain,
( ! [X0] :
( ~ sum(X0,s(s(s(n0))),s(s(s(s(s(s(s(n0))))))))
| same(X0,s(s(s(s(s(s(n0))))))) )
| ~ spl0_965 ),
inference(avatar_component_clause,[],[f8162]) ).
fof(f8164,plain,
( spl0_469
| spl0_964
| spl0_965
| ~ spl0_963 ),
inference(avatar_split_clause,[],[f8157,f8149,f8162,f8159,f3811]) ).
fof(f8167,plain,
( ! [X0] :
( ~ sum(s(s(s(s(s(s(s(n0))))))),s(s(n0)),X0)
| same(s(X0),s(s(s(s(s(s(n0))))))) )
| ~ spl0_964 ),
inference(resolution,[],[f8160,f6]) ).
fof(f8168,plain,
( ! [X0] :
( ~ sum(s(s(s(s(s(s(s(n0))))))),s(n0),X0)
| same(s(s(X0)),s(s(s(s(s(s(n0))))))) )
| ~ spl0_964 ),
inference(resolution,[],[f8167,f6]) ).
fof(f8169,plain,
( ! [X0] :
( same(s(s(s(X0))),s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),n0,X0) )
| ~ spl0_964 ),
inference(resolution,[],[f8168,f6]) ).
fof(f8170,plain,
( ! [X0] :
( ~ sum(s(s(s(s(s(s(s(n0))))))),n0,X0)
| same(s(s(X0)),s(s(s(s(s(n0)))))) )
| ~ spl0_964 ),
inference(resolution,[],[f8169,f11]) ).
fof(f8171,plain,
( same(s(s(s(s(s(s(s(s(s(n0))))))))),s(s(s(s(s(n0))))))
| ~ spl0_964 ),
inference(resolution,[],[f8170,f5]) ).
fof(f8172,plain,
( same(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(n0)))))
| ~ spl0_964 ),
inference(resolution,[],[f8171,f11]) ).
fof(f8175,plain,
( same(s(s(s(s(s(s(s(n0))))))),s(s(s(n0))))
| ~ spl0_964 ),
inference(resolution,[],[f8172,f11]) ).
fof(f8178,plain,
( same(s(s(s(s(s(s(n0)))))),s(s(n0)))
| ~ spl0_964 ),
inference(resolution,[],[f8175,f11]) ).
fof(f8181,plain,
( same(s(s(s(s(s(n0))))),s(n0))
| ~ spl0_964 ),
inference(resolution,[],[f8178,f11]) ).
fof(f8188,plain,
( same(s(s(s(s(n0)))),n0)
| ~ spl0_964 ),
inference(resolution,[],[f8181,f11]) ).
fof(f8189,plain,
( $false
| ~ spl0_964 ),
inference(forward_subsumption_resolution,[],[f8188,f9]) ).
fof(f8190,plain,
~ spl0_964,
inference(avatar_contradiction_clause,[],[f8189]) ).
fof(f8191,plain,
( ! [X0] :
( ~ sum(X0,s(s(n0)),s(s(s(s(s(s(n0)))))))
| same(X0,s(s(s(s(s(s(n0))))))) )
| ~ spl0_965 ),
inference(resolution,[],[f8163,f6]) ).
fof(f8194,plain,
( ! [X0] :
( ~ sum(X0,s(n0),s(s(s(s(s(n0))))))
| same(X0,s(s(s(s(s(s(n0))))))) )
| ~ spl0_965 ),
inference(resolution,[],[f8191,f6]) ).
fof(f8199,plain,
( ! [X0] :
( ~ sum(X0,n0,s(s(s(s(n0)))))
| same(X0,s(s(s(s(s(s(n0))))))) )
| ~ spl0_965 ),
inference(resolution,[],[f8194,f6]) ).
fof(f8200,plain,
( same(s(s(s(s(n0)))),s(s(s(s(s(s(n0)))))))
| ~ spl0_965 ),
inference(resolution,[],[f8199,f5]) ).
fof(f8201,plain,
( same(s(s(s(n0))),s(s(s(s(s(n0))))))
| ~ spl0_965 ),
inference(resolution,[],[f8200,f11]) ).
fof(f8204,plain,
( same(s(s(n0)),s(s(s(s(n0)))))
| ~ spl0_965 ),
inference(resolution,[],[f8201,f11]) ).
fof(f8205,plain,
( same(s(n0),s(s(s(n0))))
| ~ spl0_965 ),
inference(resolution,[],[f8204,f11]) ).
fof(f8206,plain,
( same(n0,s(s(n0)))
| ~ spl0_965 ),
inference(resolution,[],[f8205,f11]) ).
fof(f8207,plain,
( $false
| ~ spl0_965 ),
inference(forward_subsumption_resolution,[],[f8206,f10]) ).
fof(f8208,plain,
~ spl0_965,
inference(avatar_contradiction_clause,[],[f8207]) ).
cnf(s2,plain,
spl0_1,
inference(sat_conversion,[],[f114]) ).
cnf(s4,plain,
spl0_4,
inference(sat_conversion,[],[f135]) ).
cnf(s17,plain,
spl0_20,
inference(sat_conversion,[],[f255]) ).
cnf(s25,plain,
~ spl0_32,
inference(sat_conversion,[],[f344]) ).
cnf(s103,plain,
~ spl0_167,
inference(sat_conversion,[],[f1355]) ).
cnf(s283,plain,
~ spl0_469,
inference(sat_conversion,[],[f3822]) ).
cnf(s410,plain,
~ spl0_665,
inference(sat_conversion,[],[f5454]) ).
cnf(s411,plain,
~ spl0_666,
inference(sat_conversion,[],[f5471]) ).
cnf(s520,plain,
( ~ spl0_1
| ~ spl0_4
| ~ spl0_20
| spl0_850
| spl0_851
| spl0_852 ),
inference(sat_conversion,[],[f7215]) ).
cnf(s543,plain,
~ spl0_881,
inference(sat_conversion,[],[f7496]) ).
cnf(s552,plain,
~ spl0_882,
inference(sat_conversion,[],[f7628]) ).
cnf(s555,plain,
~ spl0_883,
inference(sat_conversion,[],[f7682]) ).
cnf(s558,plain,
~ spl0_884,
inference(sat_conversion,[],[f7721]) ).
cnf(s566,plain,
( ~ spl0_850
| spl0_881
| spl0_882
| spl0_927 ),
inference(sat_conversion,[],[f7820]) ).
cnf(s577,plain,
( spl0_167
| ~ spl0_927
| spl0_946
| spl0_947 ),
inference(sat_conversion,[],[f7976]) ).
cnf(s578,plain,
~ spl0_946,
inference(sat_conversion,[],[f7989]) ).
cnf(s581,plain,
~ spl0_947,
inference(sat_conversion,[],[f8036]) ).
cnf(s582,plain,
( spl0_32
| ~ spl0_851
| spl0_952
| spl0_953 ),
inference(sat_conversion,[],[f8045]) ).
cnf(s583,plain,
~ spl0_952,
inference(sat_conversion,[],[f8063]) ).
cnf(s584,plain,
~ spl0_953,
inference(sat_conversion,[],[f8083]) ).
cnf(s588,plain,
( ~ spl0_852
| spl0_883
| spl0_884
| spl0_962 ),
inference(sat_conversion,[],[f8143]) ).
cnf(s589,plain,
( spl0_665
| spl0_666
| ~ spl0_962
| spl0_963 ),
inference(sat_conversion,[],[f8151]) ).
cnf(s590,plain,
( spl0_469
| ~ spl0_963
| spl0_964
| spl0_965 ),
inference(sat_conversion,[],[f8164]) ).
cnf(s591,plain,
~ spl0_964,
inference(sat_conversion,[],[f8190]) ).
cnf(s592,plain,
~ spl0_965,
inference(sat_conversion,[],[f8208]) ).
cnf(s593,plain,
( spl0_469
| ~ spl0_963 ),
inference(rat,[],[s590,s592,s591]) ).
cnf(s594,plain,
( spl0_32
| ~ spl0_851 ),
inference(rat,[],[s582,s584,s583]) ).
cnf(s595,plain,
( spl0_167
| ~ spl0_927 ),
inference(rat,[],[s577,s581,s578]) ).
cnf(s635,plain,
~ spl0_963,
inference(rat,[],[s593,s283]) ).
cnf(s644,plain,
~ spl0_962,
inference(rat,[],[s589,s410,s411,s635]) ).
cnf(s647,plain,
~ spl0_852,
inference(rat,[],[s588,s555,s558,s644]) ).
cnf(s688,plain,
~ spl0_927,
inference(rat,[],[s595,s103]) ).
cnf(s701,plain,
~ spl0_850,
inference(rat,[],[s566,s543,s552,s688]) ).
cnf(s753,plain,
~ spl0_851,
inference(rat,[],[s594,s25]) ).
cnf(s784,plain,
~ spl0_1,
inference(rat,[],[s520,s647,s753,s701,s17,s4]) ).
cnf(s785,plain,
$false,
inference(rat,[],[s2,s784]) ).
fof(f8209,plain,
$false,
inference(avatar_sat_refutation,[],[s785]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ034-1.004 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.37 % Computer : n007.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 22:29:40 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.40 Running first-order model finding
% 0.10/0.40 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.21/0.92 % (1837851)Will run a generic schedule for satisfiability detection.
% 3.21/0.92 % (1837857)% WARNING: option uhcvi not known.
% 3.21/0.92 % (1837857)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2445849152:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.21/0.92 % (1837860)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3003433206:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.21/0.92 % (1837856)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=8764053_2999 on theBenchmark for (2999ds/0Mi)
% 3.21/0.92 % (1837858)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2796430251:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.21/0.92 % (1837859)dis+10_1_sil=32000:sp=arity:random_seed=3873569092:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.21/0.92 % (1837861)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3027758688:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.21/0.92 % (1837862)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2669771313:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.21/0.92 % TRYING [1]
% 3.21/0.92 % TRYING [2]
% 3.21/0.92 % TRYING [3]
% 3.21/0.92 % TRYING [4]
% 3.21/0.92 % (1837860)Instruction limit reached!
% 3.21/0.92 % (1837860)------------------------------
% 3.21/0.92 % (1837860)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.21/0.92 % (1837860)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/0.92 % (1837860)CaDiCaL version: 2.1.3
% 3.21/0.92 % (1837860)Termination reason: Instruction limit
% 3.21/0.92 % (1837860)Termination phase: Saturation
% 3.21/0.92 % (1837860)Time elapsed: 0.048 s
% 3.21/0.92 % (1837860)Peak memory usage: 12 MB
% 3.21/0.92 % (1837860)Instructions burned: 118 (million)
% 3.21/0.92 % (1837859)Instruction limit reached!
% 3.21/0.92 % (1837859)------------------------------
% 3.21/0.92 % (1837859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.21/0.92 % (1837859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/0.92 % (1837859)CaDiCaL version: 2.1.3
% 3.21/0.92 % (1837859)Termination reason: Instruction limit
% 3.21/0.92 % (1837859)Termination phase: Saturation
% 3.21/0.92 % (1837859)Time elapsed: 0.053 s
% 3.21/0.92 % (1837859)Peak memory usage: 11 MB
% 3.21/0.92 % (1837859)Instructions burned: 105 (million)
% 3.21/0.92 % (1837870)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1893245876:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.21/0.92 % TRYING [1]
% 3.21/0.92 % TRYING [2]
% 3.21/0.92 % TRYING [3]
% 3.21/0.92 % (1837861)Instruction limit reached!
% 3.21/0.92 % (1837861)------------------------------
% 3.21/0.92 % (1837861)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.21/0.92 % (1837861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/0.92 % (1837861)CaDiCaL version: 2.1.3
% 3.21/0.92 % (1837861)Termination reason: Instruction limit
% 3.21/0.92 % (1837861)Termination phase: Saturation
% 3.21/0.92 % (1837861)Time elapsed: 0.072 s
% 3.21/0.92 % (1837861)Peak memory usage: 13 MB
% 3.21/0.92 % (1837861)Instructions burned: 133 (million)
% 3.21/0.92 % (1837871)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1594157387:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.21/0.92 % TRYING [4]
% 3.21/0.92 % (1837862)Instruction limit reached!
% 3.21/0.92 % (1837862)------------------------------
% 3.21/0.92 % (1837862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.21/0.92 % (1837862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/0.92 % (1837862)CaDiCaL version: 2.1.3
% 3.21/0.92 % (1837862)Termination reason: Instruction limit
% 3.21/0.92 % (1837862)Termination phase: Saturation
% 3.21/0.92 % (1837862)Time elapsed: 0.087 s
% 3.21/0.92 % (1837862)Peak memory usage: 13 MB
% 3.21/0.92 % (1837862)Instructions burned: 161 (million)
% 3.21/0.92 % (1837874)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=409041686:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 3.21/0.92 % TRYING [5]
% 3.21/0.92 % (1837875)ott-21_1_sil=16000:fs=off:random_seed=4029438079:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 3.21/0.92 % (1837871)Instruction limit reached!
% 3.21/0.92 % (1837871)------------------------------
% 3.21/0.92 % (1837871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.21/0.92 % (1837871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/0.92 % (1837871)CaDiCaL version: 2.1.3
% 3.21/0.92 % (1837871)Termination reason: Instruction limit
% 3.21/0.92 % (1837871)Termination phase: Saturation
% 3.21/0.92 % (1837871)Time elapsed: 0.069 s
% 3.21/0.92 % (1837871)Peak memory usage: 13 MB
% 3.21/0.92 % (1837871)Instructions burned: 133 (million)
% 3.21/0.92 % TRYING [5]
% 3.21/0.92 % (1837878)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3323972551:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 3.21/0.92 % (1837875)Instruction limit reached!
% 3.21/0.92 % (1837875)------------------------------
% 3.21/0.92 % (1837875)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.21/0.92 % (1837875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/0.92 % (1837875)CaDiCaL version: 2.1.3
% 3.21/0.92 % (1837875)Termination reason: Instruction limit
% 3.21/0.92 % (1837875)Termination phase: Saturation
% 3.21/0.92 % (1837875)Time elapsed: 0.099 s
% 3.21/0.92 % (1837875)Peak memory usage: 11 MB
% 3.21/0.92 % (1837875)Instructions burned: 181 (million)
% 3.21/0.92 % (1837880)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1625472305:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 3.21/0.92 % TRYING [1]
% 3.21/0.92 % TRYING [2]
% 3.21/0.92 % TRYING [3]
% 3.21/0.92 % TRYING [4]
% 3.21/0.92 % TRYING [5]
% 3.21/0.92 % (1837878)Instruction limit reached!
% 3.21/0.92 % (1837878)------------------------------
% 3.21/0.92 % (1837878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.21/0.92 % (1837878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/0.92 % (1837878)CaDiCaL version: 2.1.3
% 3.21/0.92 % (1837878)Termination reason: Instruction limit
% 3.21/0.92 % (1837878)Termination phase: Saturation
% 3.21/0.92 % (1837878)Time elapsed: 0.292 s
% 3.21/0.92 % (1837878)Peak memory usage: 14 MB
% 3.21/0.92 % (1837878)Instructions burned: 478 (million)
% 3.21/0.92 % (1837874) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1837851-1837874"...
% 3.21/0.92 % (1837874)...printing done.
% 3.21/0.92 % (1837882)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2234564648:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 3.21/0.92 % (1837874)Refutation found. Thanks to Tanya!
% 3.21/0.92 % SZS status Unsatisfiable for theBenchmark
% 3.21/0.92 % SZS output start Proof for theBenchmark
% See solution above
% 3.21/0.92 % (1837874)------------------------------
% 3.21/0.92 % (1837874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.21/0.92 % (1837874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.21/0.92 % (1837874)CaDiCaL version: 2.1.3
% 3.21/0.92 % (1837874)Termination reason: Refutation
% 3.21/0.92 % (1837874)Time elapsed: 0.381 s
% 3.21/0.92 % (1837874)Peak memory usage: 19 MB
% 3.21/0.92 % (1837874)Instructions burned: 614 (million)
% 3.21/0.92 % (1837851)Success in time 0.514 s
% 3.21/0.92 % Vampire exiting
%------------------------------------------------------------------------------