%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : PUZ034-1.004 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:59:56 PM UTC 2026
% Result : Unsatisfiable 4.74s 1.06s
% Output : CNFRefutation 4.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 52
% Syntax : Number of formulae : 328 ( 39 unt; 34 def)
% Number of atoms : 870 ( 0 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 1057 ( 515 ~; 508 |; 0 &)
% ( 34 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 13 ( 4 avg)
% Number of predicates : 44 ( 43 usr; 35 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 351 ( 351 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [Low,High,RestOfNumbers,NewLow] :
( ~ range(NewLow,High,RestOfNumbers)
| ~ sum(Low,s(n0),NewLow)
| ~ less(Low,High)
| range(Low,High,cons(Low,RestOfNumbers)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [Same] : range(Same,Same,cons(Same,empty_list)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [X] : less(n0,s(X)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y] :
( ~ less(X,Y)
| less(s(X),s(Y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
! [X] : sum(X,n0,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X,Y,Z] :
( sum(X,s(Y),s(Z))
| ~ sum(X,Y,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [Head,Tail] : select(Head,cons(Head,Tail),Tail),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [Element,Head,Tail,NewTail] :
( ~ select(Element,Tail,NewTail)
| select(Element,cons(Head,Tail),cons(Head,NewTail)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X] : ~ same(s(X),n0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X] : ~ same(n0,s(X)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X,Y] :
( same(X,Y)
| ~ same(s(X),s(Y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [Queen,PlacedQueens] :
( ~ attack(Queen,PlacedQueens)
| diagonal_attack(Queen,s(n0),PlacedQueens) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [Queen,QueenNumber,PlacedQueen,OtherPlacedQueens,Diagonal1,Diagonal2,NextQueenNumber] :
( diagonal_attack(Queen,NextQueenNumber,OtherPlacedQueens)
| ~ sum(QueenNumber,s(n0),NextQueenNumber)
| same(Diagonal2,Queen)
| ~ sum(PlacedQueen,QueenNumber,Diagonal2)
| same(Diagonal1,Queen)
| ~ sum(Diagonal1,QueenNumber,PlacedQueen)
| ~ diagonal_attack(Queen,QueenNumber,cons(PlacedQueen,OtherPlacedQueens)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [Queen,LastQueen] : ~ diagonal_attack(Queen,LastQueen,empty_list),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [UnplacedQueens,SafeQueens,Placement,AQueen,RestOfUnplacedQueens] :
( ~ do_queens(RestOfUnplacedQueens,cons(AQueen,SafeQueens),Placement)
| attack(AQueen,SafeQueens)
| ~ select(AQueen,UnplacedQueens,RestOfUnplacedQueens)
| do_queens(UnplacedQueens,SafeQueens,Placement) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,axiom,
! [Placement] : do_queens(empty_list,Placement,Placement),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
! [NumberOfQueens,Placement,Low,High,Positions] :
( ~ do_queens(Positions,empty_list,Placement)
| ~ range(Low,High,Positions)
| ~ sum(NumberOfQueens,NumberOfQueens,High)
| ~ sum(NumberOfQueens,s(n0),Low)
| queens(NumberOfQueens,Placement) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,negated_conjecture,
! [Placement] : ~ queens(s(s(s(s(n0)))),Placement),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f19,plain,
! [High,RestOfNumbers,NewLow] :
( ~ range(NewLow,High,RestOfNumbers)
| ! [Low] :
( ~ sum(Low,s(n0),NewLow)
| ~ less(Low,High)
| range(Low,High,cons(Low,RestOfNumbers)) ) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f20,plain,
! [X0,X1,X2,X3] :
( ~ range(X3,X1,X2)
| ~ sum(X0,s(n0),X3)
| ~ less(X0,X1)
| range(X0,X1,cons(X0,X2)) ),
inference(cnf_transformation,[status(thm)],[f19]) ).
fof(f21,plain,
! [X0] : range(X0,X0,cons(X0,empty_list)),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f22,plain,
! [X0] : less(n0,s(X0)),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f23,plain,
! [X0,X1] :
( ~ less(X0,X1)
| less(s(X0),s(X1)) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f24,plain,
! [X0] : sum(X0,n0,X0),
inference(cnf_transformation,[status(thm)],[f5]) ).
fof(f25,plain,
! [X0,X1,X2] :
( sum(X0,s(X1),s(X2))
| ~ sum(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f26,plain,
! [X0,X1] : select(X0,cons(X0,X1),X1),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f27,plain,
! [Element,Tail,NewTail] :
( ~ select(Element,Tail,NewTail)
| ! [Head] : select(Element,cons(Head,Tail),cons(Head,NewTail)) ),
inference(miniscoping,[status(thm)],[f8]) ).
fof(f28,plain,
! [X0,X1,X2,X3] :
( ~ select(X0,X2,X3)
| select(X0,cons(X1,X2),cons(X1,X3)) ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f29,plain,
! [X0] : ~ same(s(X0),n0),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f30,plain,
! [X0] : ~ same(n0,s(X0)),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f31,plain,
! [X0,X1] :
( same(X0,X1)
| ~ same(s(X0),s(X1)) ),
inference(cnf_transformation,[status(thm)],[f11]) ).
fof(f32,plain,
! [X0,X1] :
( ~ attack(X0,X1)
| diagonal_attack(X0,s(n0),X1) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f33,plain,
! [Queen,OtherPlacedQueens,NextQueenNumber] :
( diagonal_attack(Queen,NextQueenNumber,OtherPlacedQueens)
| ! [QueenNumber] :
( ~ sum(QueenNumber,s(n0),NextQueenNumber)
| ! [Diagonal2] :
( same(Diagonal2,Queen)
| ! [PlacedQueen] :
( ~ sum(PlacedQueen,QueenNumber,Diagonal2)
| ! [Diagonal1] :
( same(Diagonal1,Queen)
| ~ sum(Diagonal1,QueenNumber,PlacedQueen)
| ~ diagonal_attack(Queen,QueenNumber,cons(PlacedQueen,OtherPlacedQueens)) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f13]) ).
fof(f34,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( diagonal_attack(X0,X6,X3)
| ~ sum(X1,s(n0),X6)
| same(X5,X0)
| ~ sum(X2,X1,X5)
| same(X4,X0)
| ~ sum(X4,X1,X2)
| ~ diagonal_attack(X0,X1,cons(X2,X3)) ),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f35,plain,
! [X0,X1] : ~ diagonal_attack(X0,X1,empty_list),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f36,plain,
! [SafeQueens,Placement,AQueen,RestOfUnplacedQueens] :
( ~ do_queens(RestOfUnplacedQueens,cons(AQueen,SafeQueens),Placement)
| attack(AQueen,SafeQueens)
| ! [UnplacedQueens] :
( ~ select(AQueen,UnplacedQueens,RestOfUnplacedQueens)
| do_queens(UnplacedQueens,SafeQueens,Placement) ) ),
inference(miniscoping,[status(thm)],[f15]) ).
fof(f37,plain,
! [X0,X1,X2,X3,X4] :
( ~ do_queens(X4,cons(X3,X1),X2)
| attack(X3,X1)
| ~ select(X3,X0,X4)
| do_queens(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f38,plain,
! [X0] : do_queens(empty_list,X0,X0),
inference(cnf_transformation,[status(thm)],[f16]) ).
fof(f39,plain,
! [Placement,Positions] :
( ~ do_queens(Positions,empty_list,Placement)
| ! [Low,High] :
( ~ range(Low,High,Positions)
| ! [NumberOfQueens] :
( ~ sum(NumberOfQueens,NumberOfQueens,High)
| ~ sum(NumberOfQueens,s(n0),Low)
| queens(NumberOfQueens,Placement) ) ) ),
inference(miniscoping,[status(thm)],[f17]) ).
fof(f40,plain,
! [X0,X1,X2,X3,X4] :
( ~ do_queens(X4,empty_list,X1)
| ~ range(X2,X3,X4)
| ~ sum(X0,X0,X3)
| ~ sum(X0,s(n0),X2)
| queens(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f41,plain,
! [X0] : ~ queens(s(s(s(s(n0)))),X0),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f43,plain,
! [X0,X1,X2,X3] :
( ~ range(X3,s(X1),X2)
| ~ sum(s(X0),s(n0),X3)
| range(s(X0),s(X1),cons(s(X0),X2))
| ~ less(X0,X1) ),
inference(resolution,[status(thm)],[f23,f20]) ).
fof(f44,plain,
! [X0,X1,X2,X3,X4] :
( ~ do_queens(X4,empty_list,X2)
| ~ range(s(X1),X3,X4)
| ~ sum(X0,X0,X3)
| queens(X0,X2)
| ~ sum(X0,n0,X1) ),
inference(resolution,[status(thm)],[f25,f40]) ).
fof(f45,plain,
! [X0,X1,X2,X3] :
( ~ do_queens(X3,empty_list,X1)
| ~ range(s(X0),X2,X3)
| ~ sum(X0,X0,X2)
| queens(X0,X1) ),
inference(resolution,[status(thm)],[f44,f24]) ).
fof(f46,plain,
! [X0,X1,X2] :
( ~ do_queens(X1,empty_list,X2)
| ~ range(s(s(s(s(s(n0))))),X0,X1)
| ~ sum(s(s(s(s(n0)))),s(s(s(s(n0)))),X0) ),
inference(resolution,[status(thm)],[f45,f41]) ).
fof(f47,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(n0)))),s(s(s(n0))),X0)
| ~ do_queens(X1,empty_list,X2)
| ~ range(s(s(s(s(s(n0))))),s(X0),X1) ),
inference(resolution,[status(thm)],[f46,f25]) ).
fof(f48,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(n0)))),s(s(n0)),X0)
| ~ do_queens(X1,empty_list,X2)
| ~ range(s(s(s(s(s(n0))))),s(s(X0)),X1) ),
inference(resolution,[status(thm)],[f47,f25]) ).
fof(f49,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(n0)))),s(n0),X0)
| ~ do_queens(X1,empty_list,X2)
| ~ range(s(s(s(s(s(n0))))),s(s(s(X0))),X1) ),
inference(resolution,[status(thm)],[f48,f25]) ).
fof(f50,plain,
! [X0,X1,X2] :
( ~ sum(s(s(s(s(n0)))),n0,X0)
| ~ do_queens(X1,empty_list,X2)
| ~ range(s(s(s(s(s(n0))))),s(s(s(s(X0)))),X1) ),
inference(resolution,[status(thm)],[f49,f25]) ).
fof(f51,plain,
! [X0,X1] :
( ~ do_queens(X0,empty_list,X1)
| ~ range(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(s(n0)))))))),X0) ),
inference(resolution,[status(thm)],[f50,f24]) ).
fof(f52,plain,
! [X0,X1,X2] :
( ~ range(X2,s(s(s(s(s(s(s(s(n0)))))))),X0)
| ~ sum(s(s(s(s(s(n0))))),s(n0),X2)
| ~ less(s(s(s(s(n0)))),s(s(s(s(s(s(s(n0))))))))
| ~ do_queens(cons(s(s(s(s(s(n0))))),X0),empty_list,X1) ),
inference(resolution,[status(thm)],[f51,f43]) ).
fof(f53,definition,
! [X0,X1,X2] :
( sQ0_spl
<=> ( ~ range(X2,s(s(s(s(s(s(s(s(n0)))))))),X0)
| ~ sum(s(s(s(s(s(n0))))),s(n0),X2)
| ~ do_queens(cons(s(s(s(s(s(n0))))),X0),empty_list,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f54,plain,
! [X0,X1,X2] :
( ~ sQ0_spl
| ~ range(X2,s(s(s(s(s(s(s(s(n0)))))))),X0)
| ~ sum(s(s(s(s(s(n0))))),s(n0),X2)
| ~ do_queens(cons(s(s(s(s(s(n0))))),X0),empty_list,X1) ),
inference(component_clause,[status(thm)],[f53]) ).
fof(f56,definition,
( sQ1_spl
<=> less(s(s(s(s(n0)))),s(s(s(s(s(s(s(n0)))))))) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f58,plain,
( sQ1_spl
| ~ less(s(s(s(s(n0)))),s(s(s(s(s(s(s(n0)))))))) ),
inference(component_clause,[status(thm)],[f56]) ).
fof(f59,plain,
( ~ sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f52,f53,f56]) ).
fof(f60,plain,
! [X0,X1,X2] :
( ~ sQ0_spl
| ~ sum(s(s(s(s(s(n0))))),n0,X2)
| ~ range(s(X2),s(s(s(s(s(s(s(s(n0)))))))),X0)
| ~ do_queens(cons(s(s(s(s(s(n0))))),X0),empty_list,X1) ),
inference(resolution,[status(thm)],[f54,f25]) ).
fof(f61,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ range(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(n0)))))))),X0)
| ~ do_queens(cons(s(s(s(s(s(n0))))),X0),empty_list,X1) ),
inference(resolution,[status(thm)],[f60,f24]) ).
fof(f62,plain,
! [X0,X1,X2] :
( ~ sQ0_spl
| ~ range(X2,s(s(s(s(s(s(s(s(n0)))))))),X0)
| ~ sum(s(s(s(s(s(s(n0)))))),s(n0),X2)
| ~ less(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(n0))))))))
| ~ do_queens(cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(n0)))))),X0)),empty_list,X1) ),
inference(resolution,[status(thm)],[f61,f43]) ).
fof(f63,definition,
! [X0,X1,X2] :
( sQ2_spl
<=> ( ~ range(X2,s(s(s(s(s(s(s(s(n0)))))))),X0)
| ~ sum(s(s(s(s(s(s(n0)))))),s(n0),X2)
| ~ do_queens(cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(n0)))))),X0)),empty_list,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f64,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| ~ range(X2,s(s(s(s(s(s(s(s(n0)))))))),X0)
| ~ sum(s(s(s(s(s(s(n0)))))),s(n0),X2)
| ~ do_queens(cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(n0)))))),X0)),empty_list,X1) ),
inference(component_clause,[status(thm)],[f63]) ).
fof(f66,definition,
( sQ3_spl
<=> less(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(n0)))))))) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f68,plain,
( sQ3_spl
| ~ less(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(n0)))))))) ),
inference(component_clause,[status(thm)],[f66]) ).
fof(f69,plain,
( ~ sQ0_spl
| ~ sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f62,f63,f66,f53]) ).
fof(f70,plain,
( sQ1_spl
| ~ less(s(s(s(n0))),s(s(s(s(s(s(n0))))))) ),
inference(resolution,[status(thm)],[f58,f23]) ).
fof(f71,plain,
( sQ1_spl
| ~ less(s(s(n0)),s(s(s(s(s(n0)))))) ),
inference(resolution,[status(thm)],[f70,f23]) ).
fof(f72,plain,
( sQ1_spl
| ~ less(s(n0),s(s(s(s(n0))))) ),
inference(resolution,[status(thm)],[f71,f23]) ).
fof(f73,plain,
( sQ3_spl
| ~ less(s(s(s(s(n0)))),s(s(s(s(s(s(n0))))))) ),
inference(resolution,[status(thm)],[f68,f23]) ).
fof(f74,plain,
( sQ1_spl
| ~ less(n0,s(s(s(n0)))) ),
inference(resolution,[status(thm)],[f72,f23]) ).
fof(f75,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f74,f22]) ).
fof(f76,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f75]) ).
fof(f82,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| ~ sum(s(s(s(s(s(s(n0)))))),n0,X2)
| ~ range(s(X2),s(s(s(s(s(s(s(s(n0)))))))),X0)
| ~ do_queens(cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(n0)))))),X0)),empty_list,X1) ),
inference(resolution,[status(thm)],[f64,f25]) ).
fof(f83,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ range(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(s(n0)))))))),X0)
| ~ do_queens(cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(n0)))))),X0)),empty_list,X1) ),
inference(resolution,[status(thm)],[f82,f24]) ).
fof(f84,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| ~ range(X2,s(s(s(s(s(s(s(s(n0)))))))),X0)
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(n0),X2)
| ~ less(s(s(s(s(s(s(n0)))))),s(s(s(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))))))),X0))),empty_list,X1) ),
inference(resolution,[status(thm)],[f83,f43]) ).
fof(f85,definition,
! [X0,X1,X2] :
( sQ4_spl
<=> ( ~ range(X2,s(s(s(s(s(s(s(s(n0)))))))),X0)
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(n0),X2)
| ~ 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))))))),X0))),empty_list,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f86,plain,
! [X0,X1,X2] :
( ~ sQ4_spl
| ~ range(X2,s(s(s(s(s(s(s(s(n0)))))))),X0)
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(n0),X2)
| ~ 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))))))),X0))),empty_list,X1) ),
inference(component_clause,[status(thm)],[f85]) ).
fof(f88,definition,
( sQ5_spl
<=> less(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(n0)))))))) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f90,plain,
( sQ5_spl
| ~ less(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(n0)))))))) ),
inference(component_clause,[status(thm)],[f88]) ).
fof(f91,plain,
( ~ sQ2_spl
| ~ sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f84,f85,f88,f63]) ).
fof(f92,plain,
( sQ3_spl
| ~ less(s(s(s(n0))),s(s(s(s(s(n0)))))) ),
inference(resolution,[status(thm)],[f73,f23]) ).
fof(f94,plain,
( sQ3_spl
| ~ less(s(s(n0)),s(s(s(s(n0))))) ),
inference(resolution,[status(thm)],[f92,f23]) ).
fof(f95,plain,
( sQ5_spl
| ~ less(s(s(s(s(s(n0))))),s(s(s(s(s(s(n0))))))) ),
inference(resolution,[status(thm)],[f90,f23]) ).
fof(f96,plain,
( sQ3_spl
| ~ less(s(n0),s(s(s(n0)))) ),
inference(resolution,[status(thm)],[f94,f23]) ).
fof(f97,plain,
( sQ3_spl
| ~ less(n0,s(s(n0))) ),
inference(resolution,[status(thm)],[f96,f23]) ).
fof(f98,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f97,f22]) ).
fof(f99,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f98]) ).
fof(f105,plain,
! [X0,X1,X2] :
( ~ sQ4_spl
| ~ sum(s(s(s(s(s(s(s(n0))))))),n0,X2)
| ~ range(s(X2),s(s(s(s(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))))))),X0))),empty_list,X1) ),
inference(resolution,[status(thm)],[f86,f25]) ).
fof(f106,plain,
! [X0,X1] :
( ~ sQ4_spl
| ~ range(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(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))))))),X0))),empty_list,X1) ),
inference(resolution,[status(thm)],[f105,f24]) ).
fof(f107,plain,
! [X0,X1,X2,X3] :
( ~ sQ4_spl
| ~ do_queens(X2,cons(X1,empty_list),X3)
| attack(X1,empty_list)
| ~ select(X1,cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(n0)))))),cons(s(s(s(s(s(s(s(n0))))))),X0))),X2)
| ~ range(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(n0)))))))),X0) ),
inference(resolution,[status(thm)],[f106,f37]) ).
fof(f109,plain,
! [X0,X1,X2] :
( ~ sQ4_spl
| ~ do_queens(X1,cons(X0,empty_list),X2)
| attack(X0,empty_list)
| ~ select(X0,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)))),X1) ),
inference(resolution,[status(thm)],[f107,f21]) ).
fof(f118,plain,
( sQ5_spl
| ~ less(s(s(s(s(n0)))),s(s(s(s(s(n0)))))) ),
inference(resolution,[status(thm)],[f95,f23]) ).
fof(f119,plain,
( sQ5_spl
| ~ less(s(s(s(n0))),s(s(s(s(n0))))) ),
inference(resolution,[status(thm)],[f118,f23]) ).
fof(f120,plain,
( sQ5_spl
| ~ less(s(s(n0)),s(s(s(n0)))) ),
inference(resolution,[status(thm)],[f119,f23]) ).
fof(f121,plain,
( sQ5_spl
| ~ less(s(n0),s(s(n0))) ),
inference(resolution,[status(thm)],[f120,f23]) ).
fof(f122,plain,
( sQ5_spl
| ~ less(n0,s(n0)) ),
inference(resolution,[status(thm)],[f121,f23]) ).
fof(f123,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f122,f22]) ).
fof(f124,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f123]) ).
fof(f126,plain,
! [X0,X1,X2] :
( ~ sQ4_spl
| ~ select(X0,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))),X1)
| ~ do_queens(cons(s(s(s(s(s(n0))))),X1),cons(X0,empty_list),X2)
| attack(X0,empty_list) ),
inference(resolution,[status(thm)],[f109,f28]) ).
fof(f141,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ4_spl
| ~ do_queens(X3,cons(X2,cons(X0,empty_list)),X4)
| attack(X2,cons(X0,empty_list))
| ~ select(X2,cons(s(s(s(s(s(n0))))),X1),X3)
| ~ select(X0,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))),X1)
| attack(X0,empty_list) ),
inference(resolution,[status(thm)],[f126,f37]) ).
fof(f157,definition,
! [X0] :
( sQ12_spl
<=> ( same(X0,s(s(s(s(s(s(n0)))))))
| ~ sum(X0,s(n0),s(s(s(s(s(n0)))))) ) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f158,plain,
! [X0] :
( ~ sQ12_spl
| same(X0,s(s(s(s(s(s(n0)))))))
| ~ sum(X0,s(n0),s(s(s(s(s(n0)))))) ),
inference(component_clause,[status(thm)],[f157]) ).
fof(f182,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ4_spl
| ~ select(X0,cons(s(s(s(s(s(s(s(n0))))))),cons(s(s(s(s(s(s(s(s(n0)))))))),empty_list)),X2)
| ~ do_queens(X3,cons(X1,cons(X0,empty_list)),X4)
| attack(X1,cons(X0,empty_list))
| ~ select(X1,cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(n0)))))),X2)),X3)
| attack(X0,empty_list) ),
inference(resolution,[status(thm)],[f141,f28]) ).
fof(f212,plain,
! [X0,X1,X2] :
( ~ sQ4_spl
| ~ do_queens(X1,cons(X0,cons(s(s(s(s(s(s(s(n0))))))),empty_list)),X2)
| attack(X0,cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| ~ select(X0,cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(n0)))))),cons(s(s(s(s(s(s(s(s(n0)))))))),empty_list))),X1)
| attack(s(s(s(s(s(s(s(n0))))))),empty_list) ),
inference(resolution,[status(thm)],[f182,f26]) ).
fof(f213,definition,
( sQ19_spl
<=> attack(s(s(s(s(s(s(s(n0))))))),empty_list) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f214,plain,
( ~ sQ19_spl
| attack(s(s(s(s(s(s(s(n0))))))),empty_list) ),
inference(component_clause,[status(thm)],[f213]) ).
fof(f216,definition,
! [X0,X1,X2] :
( sQ20_spl
<=> ( ~ do_queens(X1,cons(X0,cons(s(s(s(s(s(s(s(n0))))))),empty_list)),X2)
| attack(X0,cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| ~ select(X0,cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(n0)))))),cons(s(s(s(s(s(s(s(s(n0)))))))),empty_list))),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f217,plain,
! [X0,X1,X2] :
( ~ sQ20_spl
| ~ do_queens(X1,cons(X0,cons(s(s(s(s(s(s(s(n0))))))),empty_list)),X2)
| attack(X0,cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| ~ select(X0,cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(n0)))))),cons(s(s(s(s(s(s(s(s(n0)))))))),empty_list))),X1) ),
inference(component_clause,[status(thm)],[f216]) ).
fof(f219,plain,
( ~ sQ4_spl
| sQ20_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f212,f213,f216,f85]) ).
fof(f220,plain,
( ~ sQ19_spl
| diagonal_attack(s(s(s(s(s(s(s(n0))))))),s(n0),empty_list) ),
inference(resolution,[status(thm)],[f214,f32]) ).
fof(f221,plain,
( ~ sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f220,f35]) ).
fof(f222,plain,
~ sQ19_spl,
inference(contradiction_clause,[status(thm)],[f221]) ).
fof(f250,plain,
! [X0] :
( ~ sQ12_spl
| ~ sum(X0,n0,s(s(s(s(n0)))))
| same(X0,s(s(s(s(s(s(n0))))))) ),
inference(resolution,[status(thm)],[f158,f25]) ).
fof(f260,plain,
( ~ sQ12_spl
| same(s(s(s(s(n0)))),s(s(s(s(s(s(n0))))))) ),
inference(resolution,[status(thm)],[f250,f24]) ).
fof(f261,plain,
( ~ sQ12_spl
| same(s(s(s(n0))),s(s(s(s(s(n0)))))) ),
inference(resolution,[status(thm)],[f260,f31]) ).
fof(f262,plain,
( ~ sQ12_spl
| same(s(s(n0)),s(s(s(s(n0))))) ),
inference(resolution,[status(thm)],[f261,f31]) ).
fof(f263,plain,
( ~ sQ12_spl
| same(s(n0),s(s(s(n0)))) ),
inference(resolution,[status(thm)],[f262,f31]) ).
fof(f264,plain,
( ~ sQ12_spl
| same(n0,s(s(n0))) ),
inference(resolution,[status(thm)],[f263,f31]) ).
fof(f265,plain,
( ~ sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f264,f30]) ).
fof(f266,plain,
~ sQ12_spl,
inference(contradiction_clause,[status(thm)],[f265]) ).
fof(f277,plain,
! [X0] :
( ~ sQ20_spl
| ~ do_queens(cons(s(s(s(s(s(s(n0)))))),cons(s(s(s(s(s(s(s(s(n0)))))))),empty_list)),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)),X0)
| attack(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)) ),
inference(resolution,[status(thm)],[f217,f26]) ).
fof(f278,definition,
( sQ29_spl
<=> attack(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f279,plain,
( ~ sQ29_spl
| attack(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)) ),
inference(component_clause,[status(thm)],[f278]) ).
fof(f281,definition,
! [X0] :
( sQ30_spl
<=> ~ do_queens(cons(s(s(s(s(s(s(n0)))))),cons(s(s(s(s(s(s(s(s(n0)))))))),empty_list)),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)),X0) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f282,plain,
! [X0] :
( ~ sQ30_spl
| ~ do_queens(cons(s(s(s(s(s(s(n0)))))),cons(s(s(s(s(s(s(s(s(n0)))))))),empty_list)),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)),X0) ),
inference(component_clause,[status(thm)],[f281]) ).
fof(f284,plain,
( ~ sQ20_spl
| sQ30_spl
| sQ29_spl ),
inference(split_clause,[status(thm)],[f277,f278,f281,f216]) ).
fof(f299,plain,
( ~ sQ29_spl
| diagonal_attack(s(s(s(s(s(n0))))),s(n0),cons(s(s(s(s(s(s(s(n0))))))),empty_list)) ),
inference(resolution,[status(thm)],[f279,f32]) ).
fof(f307,definition,
! [X2] :
( sQ33_spl
<=> ( diagonal_attack(s(s(s(s(s(n0))))),X2,empty_list)
| ~ sum(s(n0),s(n0),X2) ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f308,plain,
! [X0] :
( ~ sQ33_spl
| diagonal_attack(s(s(s(s(s(n0))))),X0,empty_list)
| ~ sum(s(n0),s(n0),X0) ),
inference(component_clause,[status(thm)],[f307]) ).
fof(f311,plain,
! [X0] :
( ~ sQ33_spl
| ~ sum(s(n0),s(n0),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f308,f35]) ).
fof(f312,plain,
! [X0] :
( ~ sQ33_spl
| ~ sum(s(n0),n0,X0) ),
inference(resolution,[status(thm)],[f311,f25]) ).
fof(f314,plain,
( ~ sQ33_spl
| $false ),
inference(resolution,[status(thm)],[f312,f24]) ).
fof(f315,plain,
~ sQ33_spl,
inference(contradiction_clause,[status(thm)],[f314]) ).
fof(f376,plain,
! [X0,X1,X2] :
( ~ sQ29_spl
| diagonal_attack(s(s(s(s(s(n0))))),X2,empty_list)
| ~ sum(s(n0),s(n0),X2)
| same(X1,s(s(s(s(s(n0))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(n0),X1)
| same(X0,s(s(s(s(s(n0))))))
| ~ sum(X0,s(n0),s(s(s(s(s(s(s(n0)))))))) ),
inference(resolution,[status(thm)],[f299,f34]) ).
fof(f377,definition,
! [X0] :
( sQ43_spl
<=> ( same(X0,s(s(s(s(s(n0))))))
| ~ sum(X0,s(n0),s(s(s(s(s(s(s(n0)))))))) ) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f378,plain,
! [X0] :
( ~ sQ43_spl
| same(X0,s(s(s(s(s(n0))))))
| ~ sum(X0,s(n0),s(s(s(s(s(s(s(n0)))))))) ),
inference(component_clause,[status(thm)],[f377]) ).
fof(f380,definition,
! [X1] :
( sQ44_spl
<=> ( same(X1,s(s(s(s(s(n0))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(n0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f381,plain,
! [X0] :
( ~ sQ44_spl
| same(X0,s(s(s(s(s(n0))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(n0),X0) ),
inference(component_clause,[status(thm)],[f380]) ).
fof(f383,plain,
( ~ sQ29_spl
| sQ33_spl
| sQ44_spl
| sQ43_spl ),
inference(split_clause,[status(thm)],[f376,f377,f380,f307,f278]) ).
fof(f389,plain,
! [X0,X1,X2] :
( ~ sQ30_spl
| ~ do_queens(X1,cons(X0,cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list))),X2)
| attack(X0,cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| ~ select(X0,cons(s(s(s(s(s(s(n0)))))),cons(s(s(s(s(s(s(s(s(n0)))))))),empty_list)),X1) ),
inference(resolution,[status(thm)],[f282,f37]) ).
fof(f406,plain,
! [X0] :
( ~ sQ44_spl
| ~ sum(s(s(s(s(s(s(s(n0))))))),n0,X0)
| same(s(X0),s(s(s(s(s(n0)))))) ),
inference(resolution,[status(thm)],[f381,f25]) ).
fof(f407,plain,
! [X0] :
( ~ sQ43_spl
| ~ sum(X0,n0,s(s(s(s(s(s(n0)))))))
| same(X0,s(s(s(s(s(n0)))))) ),
inference(resolution,[status(thm)],[f378,f25]) ).
fof(f408,plain,
( ~ sQ43_spl
| same(s(s(s(s(s(s(n0)))))),s(s(s(s(s(n0)))))) ),
inference(resolution,[status(thm)],[f407,f24]) ).
fof(f409,plain,
( ~ sQ43_spl
| same(s(s(s(s(s(n0))))),s(s(s(s(n0))))) ),
inference(resolution,[status(thm)],[f408,f31]) ).
fof(f410,plain,
( ~ sQ43_spl
| same(s(s(s(s(n0)))),s(s(s(n0)))) ),
inference(resolution,[status(thm)],[f409,f31]) ).
fof(f423,plain,
( ~ sQ43_spl
| same(s(s(s(n0))),s(s(n0))) ),
inference(resolution,[status(thm)],[f410,f31]) ).
fof(f424,plain,
( ~ sQ43_spl
| same(s(s(n0)),s(n0)) ),
inference(resolution,[status(thm)],[f423,f31]) ).
fof(f425,plain,
( ~ sQ43_spl
| same(s(n0),n0) ),
inference(resolution,[status(thm)],[f424,f31]) ).
fof(f426,plain,
( ~ sQ43_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f425,f29]) ).
fof(f427,plain,
~ sQ43_spl,
inference(contradiction_clause,[status(thm)],[f426]) ).
fof(f458,plain,
( ~ sQ44_spl
| same(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(n0)))))) ),
inference(resolution,[status(thm)],[f406,f24]) ).
fof(f459,plain,
( ~ sQ44_spl
| same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(n0))))) ),
inference(resolution,[status(thm)],[f458,f31]) ).
fof(f460,plain,
( ~ sQ44_spl
| same(s(s(s(s(s(s(n0)))))),s(s(s(n0)))) ),
inference(resolution,[status(thm)],[f459,f31]) ).
fof(f461,plain,
( ~ sQ44_spl
| same(s(s(s(s(s(n0))))),s(s(n0))) ),
inference(resolution,[status(thm)],[f460,f31]) ).
fof(f462,plain,
( ~ sQ44_spl
| same(s(s(s(s(n0)))),s(n0)) ),
inference(resolution,[status(thm)],[f461,f31]) ).
fof(f463,plain,
( ~ sQ44_spl
| same(s(s(s(n0))),n0) ),
inference(resolution,[status(thm)],[f462,f31]) ).
fof(f464,plain,
( ~ sQ44_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f463,f29]) ).
fof(f465,plain,
~ sQ44_spl,
inference(contradiction_clause,[status(thm)],[f464]) ).
fof(f486,definition,
! [X0] :
( sQ56_spl
<=> ( same(X0,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(X0,s(n0),s(s(s(s(s(n0)))))) ) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f487,plain,
! [X0] :
( ~ sQ56_spl
| same(X0,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(X0,s(n0),s(s(s(s(s(n0)))))) ),
inference(component_clause,[status(thm)],[f486]) ).
fof(f489,definition,
! [X1] :
( sQ57_spl
<=> ( same(X1,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(s(n0))))),s(n0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f490,plain,
! [X0] :
( ~ sQ57_spl
| same(X0,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(s(n0))))),s(n0),X0) ),
inference(component_clause,[status(thm)],[f489]) ).
fof(f543,plain,
! [X0] :
( ~ sQ57_spl
| ~ sum(s(s(s(s(s(n0))))),n0,X0)
| same(s(X0),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(resolution,[status(thm)],[f490,f25]) ).
fof(f544,plain,
! [X0] :
( ~ sQ56_spl
| ~ sum(X0,n0,s(s(s(s(n0)))))
| same(X0,s(s(s(s(s(s(s(s(n0))))))))) ),
inference(resolution,[status(thm)],[f487,f25]) ).
fof(f545,plain,
( ~ sQ56_spl
| same(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(resolution,[status(thm)],[f544,f24]) ).
fof(f546,plain,
( ~ sQ56_spl
| same(s(s(s(n0))),s(s(s(s(s(s(s(n0)))))))) ),
inference(resolution,[status(thm)],[f545,f31]) ).
fof(f547,plain,
( ~ sQ56_spl
| same(s(s(n0)),s(s(s(s(s(s(n0))))))) ),
inference(resolution,[status(thm)],[f546,f31]) ).
fof(f548,plain,
! [X0,X1,X2] :
( ~ sQ30_spl
| ~ select(X0,cons(s(s(s(s(s(s(s(s(n0)))))))),empty_list),X1)
| ~ do_queens(cons(s(s(s(s(s(s(n0)))))),X1),cons(X0,cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list))),X2)
| attack(X0,cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list))) ),
inference(resolution,[status(thm)],[f389,f28]) ).
fof(f566,plain,
( ~ sQ56_spl
| same(s(n0),s(s(s(s(s(n0)))))) ),
inference(resolution,[status(thm)],[f547,f31]) ).
fof(f567,plain,
( ~ sQ56_spl
| same(n0,s(s(s(s(n0))))) ),
inference(resolution,[status(thm)],[f566,f31]) ).
fof(f568,plain,
( ~ sQ56_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f567,f30]) ).
fof(f569,plain,
~ sQ56_spl,
inference(contradiction_clause,[status(thm)],[f568]) ).
fof(f604,plain,
! [X0] :
( ~ sQ57_spl
| same(X0,s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(s(s(s(s(n0))))),n0,X0) ),
inference(resolution,[status(thm)],[f543,f31]) ).
fof(f605,plain,
( ~ sQ57_spl
| same(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(n0)))))))) ),
inference(resolution,[status(thm)],[f604,f24]) ).
fof(f606,plain,
( ~ sQ57_spl
| same(s(s(s(s(n0)))),s(s(s(s(s(s(n0))))))) ),
inference(resolution,[status(thm)],[f605,f31]) ).
fof(f611,plain,
( ~ sQ57_spl
| same(s(s(s(n0))),s(s(s(s(s(n0)))))) ),
inference(resolution,[status(thm)],[f606,f31]) ).
fof(f612,plain,
( ~ sQ57_spl
| same(s(s(n0)),s(s(s(s(n0))))) ),
inference(resolution,[status(thm)],[f611,f31]) ).
fof(f613,plain,
( ~ sQ57_spl
| same(s(n0),s(s(s(n0)))) ),
inference(resolution,[status(thm)],[f612,f31]) ).
fof(f614,plain,
( ~ sQ57_spl
| same(n0,s(s(n0))) ),
inference(resolution,[status(thm)],[f613,f31]) ).
fof(f615,plain,
( ~ sQ57_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f614,f30]) ).
fof(f616,plain,
~ sQ57_spl,
inference(contradiction_clause,[status(thm)],[f615]) ).
fof(f652,definition,
! [X0] :
( sQ75_spl
<=> ( 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,[sQ75_spl])],[split_symbol_definition]) ).
fof(f653,plain,
! [X0] :
( ~ sQ75_spl
| same(X0,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(X0,s(n0),s(s(s(s(s(s(n0))))))) ),
inference(component_clause,[status(thm)],[f652]) ).
fof(f660,plain,
! [X0] :
( ~ sQ75_spl
| ~ sum(X0,n0,s(s(s(s(s(n0))))))
| same(X0,s(s(s(s(s(s(s(s(n0))))))))) ),
inference(resolution,[status(thm)],[f653,f25]) ).
fof(f661,plain,
( ~ sQ75_spl
| same(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(resolution,[status(thm)],[f660,f24]) ).
fof(f662,plain,
( ~ sQ75_spl
| same(s(s(s(s(n0)))),s(s(s(s(s(s(s(n0)))))))) ),
inference(resolution,[status(thm)],[f661,f31]) ).
fof(f686,plain,
( ~ sQ75_spl
| same(s(s(s(n0))),s(s(s(s(s(s(n0))))))) ),
inference(resolution,[status(thm)],[f662,f31]) ).
fof(f687,plain,
( ~ sQ75_spl
| same(s(s(n0)),s(s(s(s(s(n0)))))) ),
inference(resolution,[status(thm)],[f686,f31]) ).
fof(f688,plain,
( ~ sQ75_spl
| same(s(n0),s(s(s(s(n0))))) ),
inference(resolution,[status(thm)],[f687,f31]) ).
fof(f698,plain,
( ~ sQ75_spl
| same(n0,s(s(s(n0)))) ),
inference(resolution,[status(thm)],[f688,f31]) ).
fof(f699,plain,
( ~ sQ75_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f698,f30]) ).
fof(f700,plain,
~ sQ75_spl,
inference(contradiction_clause,[status(thm)],[f699]) ).
fof(f715,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ30_spl
| ~ do_queens(X3,cons(X2,cons(X0,cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))),X4)
| attack(X2,cons(X0,cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list))))
| ~ select(X2,cons(s(s(s(s(s(s(n0)))))),X1),X3)
| ~ select(X0,cons(s(s(s(s(s(s(s(s(n0)))))))),empty_list),X1)
| attack(X0,cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list))) ),
inference(resolution,[status(thm)],[f548,f37]) ).
fof(f724,definition,
! [X0] :
( sQ86_spl
<=> ( same(X0,s(s(s(s(s(s(n0)))))))
| ~ sum(X0,s(n0),s(s(s(s(s(s(s(s(n0))))))))) ) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f725,plain,
! [X0] :
( ~ sQ86_spl
| same(X0,s(s(s(s(s(s(n0)))))))
| ~ sum(X0,s(n0),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(component_clause,[status(thm)],[f724]) ).
fof(f727,definition,
! [X1] :
( sQ87_spl
<=> ( same(X1,s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(s(s(s(n0)))))))),s(n0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f728,plain,
! [X0] :
( ~ sQ87_spl
| same(X0,s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(s(s(s(n0)))))))),s(n0),X0) ),
inference(component_clause,[status(thm)],[f727]) ).
fof(f731,plain,
! [X0] :
( ~ sQ87_spl
| ~ sum(s(s(s(s(s(s(s(s(n0)))))))),n0,X0)
| same(s(X0),s(s(s(s(s(s(n0))))))) ),
inference(resolution,[status(thm)],[f728,f25]) ).
fof(f732,plain,
! [X0] :
( ~ sQ86_spl
| ~ sum(X0,n0,s(s(s(s(s(s(s(n0))))))))
| same(X0,s(s(s(s(s(s(n0))))))) ),
inference(resolution,[status(thm)],[f725,f25]) ).
fof(f735,plain,
( ~ sQ86_spl
| same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(n0))))))) ),
inference(resolution,[status(thm)],[f732,f24]) ).
fof(f736,plain,
( ~ sQ86_spl
| same(s(s(s(s(s(s(n0)))))),s(s(s(s(s(n0)))))) ),
inference(resolution,[status(thm)],[f735,f31]) ).
fof(f737,plain,
( ~ sQ86_spl
| same(s(s(s(s(s(n0))))),s(s(s(s(n0))))) ),
inference(resolution,[status(thm)],[f736,f31]) ).
fof(f747,plain,
( ~ sQ86_spl
| same(s(s(s(s(n0)))),s(s(s(n0)))) ),
inference(resolution,[status(thm)],[f737,f31]) ).
fof(f748,plain,
( ~ sQ86_spl
| same(s(s(s(n0))),s(s(n0))) ),
inference(resolution,[status(thm)],[f747,f31]) ).
fof(f749,plain,
( ~ sQ86_spl
| same(s(s(n0)),s(n0)) ),
inference(resolution,[status(thm)],[f748,f31]) ).
fof(f750,plain,
( ~ sQ86_spl
| same(s(n0),n0) ),
inference(resolution,[status(thm)],[f749,f31]) ).
fof(f751,plain,
( ~ sQ86_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f750,f29]) ).
fof(f752,plain,
~ sQ86_spl,
inference(contradiction_clause,[status(thm)],[f751]) ).
fof(f753,plain,
( ~ sQ87_spl
| same(s(s(s(s(s(s(s(s(s(n0))))))))),s(s(s(s(s(s(n0))))))) ),
inference(resolution,[status(thm)],[f731,f24]) ).
fof(f754,plain,
( ~ sQ87_spl
| same(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(n0)))))) ),
inference(resolution,[status(thm)],[f753,f31]) ).
fof(f757,plain,
( ~ sQ87_spl
| same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(n0))))) ),
inference(resolution,[status(thm)],[f754,f31]) ).
fof(f758,plain,
( ~ sQ87_spl
| same(s(s(s(s(s(s(n0)))))),s(s(s(n0)))) ),
inference(resolution,[status(thm)],[f757,f31]) ).
fof(f759,plain,
( ~ sQ87_spl
| same(s(s(s(s(s(n0))))),s(s(n0))) ),
inference(resolution,[status(thm)],[f758,f31]) ).
fof(f760,plain,
( ~ sQ87_spl
| same(s(s(s(s(n0)))),s(n0)) ),
inference(resolution,[status(thm)],[f759,f31]) ).
fof(f761,plain,
( ~ sQ87_spl
| same(s(s(s(n0))),n0) ),
inference(resolution,[status(thm)],[f760,f31]) ).
fof(f762,plain,
( ~ sQ87_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f761,f29]) ).
fof(f763,plain,
~ sQ87_spl,
inference(contradiction_clause,[status(thm)],[f762]) ).
fof(f959,plain,
! [X0,X1,X2] :
( ~ sQ30_spl
| ~ do_queens(X1,cons(X0,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)))),X2)
| attack(X0,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))))
| ~ select(X0,cons(s(s(s(s(s(s(n0)))))),empty_list),X1)
| 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))) ),
inference(resolution,[status(thm)],[f715,f26]) ).
fof(f960,definition,
( sQ116_spl
<=> 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,[sQ116_spl])],[split_symbol_definition]) ).
fof(f961,plain,
( ~ sQ116_spl
| 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))) ),
inference(component_clause,[status(thm)],[f960]) ).
fof(f963,definition,
! [X0,X1,X2] :
( sQ117_spl
<=> ( ~ do_queens(X1,cons(X0,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)))),X2)
| attack(X0,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))))
| ~ select(X0,cons(s(s(s(s(s(s(n0)))))),empty_list),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f964,plain,
! [X0,X1,X2] :
( ~ sQ117_spl
| ~ do_queens(X1,cons(X0,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)))),X2)
| attack(X0,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))))
| ~ select(X0,cons(s(s(s(s(s(s(n0)))))),empty_list),X1) ),
inference(component_clause,[status(thm)],[f963]) ).
fof(f966,plain,
( ~ sQ30_spl
| sQ117_spl
| sQ116_spl ),
inference(split_clause,[status(thm)],[f959,f960,f963,f281]) ).
fof(f967,plain,
( ~ sQ116_spl
| diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(n0),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list))) ),
inference(resolution,[status(thm)],[f961,f32]) ).
fof(f981,plain,
! [X0,X1,X2] :
( ~ sQ116_spl
| diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),X2,cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| ~ sum(s(n0),s(n0),X2)
| same(X1,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(s(n0))))),s(n0),X1)
| same(X0,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(X0,s(n0),s(s(s(s(s(n0)))))) ),
inference(resolution,[status(thm)],[f967,f34]) ).
fof(f982,definition,
! [X2] :
( sQ120_spl
<=> ( diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),X2,cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| ~ sum(s(n0),s(n0),X2) ) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f983,plain,
! [X0] :
( ~ sQ120_spl
| diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),X0,cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| ~ sum(s(n0),s(n0),X0) ),
inference(component_clause,[status(thm)],[f982]) ).
fof(f985,plain,
( ~ sQ116_spl
| sQ120_spl
| sQ57_spl
| sQ56_spl ),
inference(split_clause,[status(thm)],[f981,f486,f489,f982,f960]) ).
fof(f986,plain,
! [X0] :
( ~ sQ120_spl
| ~ sum(s(n0),n0,X0)
| diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(X0),cons(s(s(s(s(s(s(s(n0))))))),empty_list)) ),
inference(resolution,[status(thm)],[f983,f25]) ).
fof(f987,plain,
! [X0,X1,X2,X3] :
( ~ sQ120_spl
| diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),X3,empty_list)
| ~ sum(s(X0),s(n0),X3)
| same(X2,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(X0),X2)
| same(X1,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(X1,s(X0),s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(n0),n0,X0) ),
inference(resolution,[status(thm)],[f986,f34]) ).
fof(f988,plain,
! [X0,X1,X2,X3] :
( ~ sQ120_spl
| ~ sum(s(X0),s(n0),X3)
| same(X2,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(X0),X2)
| same(X1,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(X1,s(X0),s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(n0),n0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f987,f35]) ).
fof(f1097,definition,
! [X2] :
( sQ138_spl
<=> ~ sum(s(s(n0)),s(n0),X2) ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f1098,plain,
! [X0] :
( ~ sQ138_spl
| ~ sum(s(s(n0)),s(n0),X0) ),
inference(component_clause,[status(thm)],[f1097]) ).
fof(f1101,plain,
! [X0] :
( ~ sQ138_spl
| ~ sum(s(s(n0)),n0,X0) ),
inference(resolution,[status(thm)],[f1098,f25]) ).
fof(f1102,plain,
( ~ sQ138_spl
| $false ),
inference(resolution,[status(thm)],[f1101,f24]) ).
fof(f1103,plain,
~ sQ138_spl,
inference(contradiction_clause,[status(thm)],[f1102]) ).
fof(f1221,plain,
! [X0] :
( ~ sQ117_spl
| ~ do_queens(empty_list,cons(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)))),X0)
| 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)))) ),
inference(resolution,[status(thm)],[f964,f26]) ).
fof(f1222,definition,
( sQ154_spl
<=> 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,[sQ154_spl])],[split_symbol_definition]) ).
fof(f1223,plain,
( ~ sQ154_spl
| 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)))) ),
inference(component_clause,[status(thm)],[f1222]) ).
fof(f1225,definition,
! [X0] :
( sQ155_spl
<=> ~ do_queens(empty_list,cons(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)))),X0) ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f1226,plain,
! [X0] :
( ~ sQ155_spl
| ~ do_queens(empty_list,cons(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)))),X0) ),
inference(component_clause,[status(thm)],[f1225]) ).
fof(f1228,plain,
( ~ sQ117_spl
| sQ155_spl
| sQ154_spl ),
inference(split_clause,[status(thm)],[f1221,f1222,f1225,f963]) ).
fof(f1229,plain,
( ~ sQ154_spl
| diagonal_attack(s(s(s(s(s(s(n0)))))),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)))) ),
inference(resolution,[status(thm)],[f1223,f32]) ).
fof(f1237,plain,
! [X0,X1,X2] :
( ~ sQ154_spl
| diagonal_attack(s(s(s(s(s(s(n0)))))),X2,cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| ~ sum(s(n0),s(n0),X2)
| same(X1,s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(s(s(s(n0)))))))),s(n0),X1)
| same(X0,s(s(s(s(s(s(n0)))))))
| ~ sum(X0,s(n0),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(resolution,[status(thm)],[f1229,f34]) ).
fof(f1238,definition,
! [X2] :
( sQ157_spl
<=> ( diagonal_attack(s(s(s(s(s(s(n0)))))),X2,cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| ~ sum(s(n0),s(n0),X2) ) ),
introduced(definition,[new_symbols(definition,[sQ157_spl])],[split_symbol_definition]) ).
fof(f1239,plain,
! [X0] :
( ~ sQ157_spl
| diagonal_attack(s(s(s(s(s(s(n0)))))),X0,cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| ~ sum(s(n0),s(n0),X0) ),
inference(component_clause,[status(thm)],[f1238]) ).
fof(f1241,plain,
( ~ sQ154_spl
| sQ157_spl
| sQ87_spl
| sQ86_spl ),
inference(split_clause,[status(thm)],[f1237,f724,f727,f1238,f1222]) ).
fof(f1242,plain,
! [X0] :
( ~ sQ157_spl
| ~ sum(s(n0),n0,X0)
| diagonal_attack(s(s(s(s(s(s(n0)))))),s(X0),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list))) ),
inference(resolution,[status(thm)],[f1239,f25]) ).
fof(f1255,plain,
! [X0,X1,X2,X3] :
( ~ sQ157_spl
| diagonal_attack(s(s(s(s(s(s(n0)))))),X3,cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| ~ sum(s(X0),s(n0),X3)
| same(X2,s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(n0))))),s(X0),X2)
| same(X1,s(s(s(s(s(s(n0)))))))
| ~ sum(X1,s(X0),s(s(s(s(s(n0))))))
| ~ sum(s(n0),n0,X0) ),
inference(resolution,[status(thm)],[f1242,f34]) ).
fof(f1266,plain,
( ~ sQ155_spl
| $false ),
inference(resolution,[status(thm)],[f1226,f38]) ).
fof(f1268,plain,
~ sQ155_spl,
inference(contradiction_clause,[status(thm)],[f1266]) ).
fof(f1270,definition,
! [X0] :
( sQ160_spl
<=> ( same(X0,s(s(s(s(s(s(n0)))))))
| ~ sum(X0,s(s(n0)),s(s(s(s(s(n0)))))) ) ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f1271,plain,
! [X0] :
( ~ sQ160_spl
| same(X0,s(s(s(s(s(s(n0)))))))
| ~ sum(X0,s(s(n0)),s(s(s(s(s(n0)))))) ),
inference(component_clause,[status(thm)],[f1270]) ).
fof(f1273,definition,
! [X1] :
( sQ161_spl
<=> ( same(X1,s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(n0))))),s(s(n0)),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition]) ).
fof(f1274,plain,
! [X0] :
( ~ sQ161_spl
| same(X0,s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(n0))))),s(s(n0)),X0) ),
inference(component_clause,[status(thm)],[f1273]) ).
fof(f1295,plain,
! [X0] :
( ~ sQ160_spl
| ~ sum(X0,s(n0),s(s(s(s(n0)))))
| same(X0,s(s(s(s(s(s(n0))))))) ),
inference(resolution,[status(thm)],[f1271,f25]) ).
fof(f1296,plain,
! [X0] :
( ~ sQ160_spl
| ~ sum(X0,n0,s(s(s(n0))))
| same(X0,s(s(s(s(s(s(n0))))))) ),
inference(resolution,[status(thm)],[f1295,f25]) ).
fof(f1297,plain,
( ~ sQ160_spl
| same(s(s(s(n0))),s(s(s(s(s(s(n0))))))) ),
inference(resolution,[status(thm)],[f1296,f24]) ).
fof(f1298,plain,
( ~ sQ160_spl
| same(s(s(n0)),s(s(s(s(s(n0)))))) ),
inference(resolution,[status(thm)],[f1297,f31]) ).
fof(f1299,plain,
( ~ sQ160_spl
| same(s(n0),s(s(s(s(n0))))) ),
inference(resolution,[status(thm)],[f1298,f31]) ).
fof(f1300,plain,
( ~ sQ160_spl
| same(n0,s(s(s(n0)))) ),
inference(resolution,[status(thm)],[f1299,f31]) ).
fof(f1301,plain,
( ~ sQ160_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1300,f30]) ).
fof(f1302,plain,
~ sQ160_spl,
inference(contradiction_clause,[status(thm)],[f1301]) ).
fof(f1303,plain,
! [X0] :
( ~ sQ161_spl
| ~ sum(s(s(s(s(s(n0))))),s(n0),X0)
| same(s(X0),s(s(s(s(s(s(n0))))))) ),
inference(resolution,[status(thm)],[f1274,f25]) ).
fof(f1304,plain,
! [X0] :
( ~ sQ161_spl
| ~ sum(s(s(s(s(s(n0))))),n0,X0)
| same(s(s(X0)),s(s(s(s(s(s(n0))))))) ),
inference(resolution,[status(thm)],[f1303,f25]) ).
fof(f1305,plain,
! [X0] :
( ~ sQ161_spl
| same(s(X0),s(s(s(s(s(n0))))))
| ~ sum(s(s(s(s(s(n0))))),n0,X0) ),
inference(resolution,[status(thm)],[f1304,f31]) ).
fof(f1307,plain,
( ~ sQ161_spl
| same(s(s(s(s(s(s(n0)))))),s(s(s(s(s(n0)))))) ),
inference(resolution,[status(thm)],[f1305,f24]) ).
fof(f1308,plain,
( ~ sQ161_spl
| same(s(s(s(s(s(n0))))),s(s(s(s(n0))))) ),
inference(resolution,[status(thm)],[f1307,f31]) ).
fof(f1309,plain,
( ~ sQ161_spl
| same(s(s(s(s(n0)))),s(s(s(n0)))) ),
inference(resolution,[status(thm)],[f1308,f31]) ).
fof(f1310,plain,
( ~ sQ161_spl
| same(s(s(s(n0))),s(s(n0))) ),
inference(resolution,[status(thm)],[f1309,f31]) ).
fof(f1311,plain,
( ~ sQ161_spl
| same(s(s(n0)),s(n0)) ),
inference(resolution,[status(thm)],[f1310,f31]) ).
fof(f1312,plain,
( ~ sQ161_spl
| same(s(n0),n0) ),
inference(resolution,[status(thm)],[f1311,f31]) ).
fof(f1313,plain,
( ~ sQ161_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1312,f29]) ).
fof(f1314,plain,
~ sQ161_spl,
inference(contradiction_clause,[status(thm)],[f1313]) ).
fof(f1728,plain,
! [X0,X1,X2] :
( ~ sQ120_spl
| ~ sum(s(s(n0)),s(n0),X2)
| same(X1,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(s(n0)),X1)
| same(X0,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(X0,s(s(n0)),s(s(s(s(s(s(s(n0)))))))) ),
inference(resolution,[status(thm)],[f988,f24]) ).
fof(f1729,definition,
! [X0] :
( sQ218_spl
<=> ( same(X0,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(X0,s(s(n0)),s(s(s(s(s(s(s(n0)))))))) ) ),
introduced(definition,[new_symbols(definition,[sQ218_spl])],[split_symbol_definition]) ).
fof(f1730,plain,
! [X0] :
( ~ sQ218_spl
| same(X0,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(X0,s(s(n0)),s(s(s(s(s(s(s(n0)))))))) ),
inference(component_clause,[status(thm)],[f1729]) ).
fof(f1732,definition,
! [X1] :
( sQ219_spl
<=> ( same(X1,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(s(n0)),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ219_spl])],[split_symbol_definition]) ).
fof(f1733,plain,
! [X0] :
( ~ sQ219_spl
| same(X0,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(s(n0)),X0) ),
inference(component_clause,[status(thm)],[f1732]) ).
fof(f1735,plain,
( ~ sQ120_spl
| sQ138_spl
| sQ219_spl
| sQ218_spl ),
inference(split_clause,[status(thm)],[f1728,f1729,f1732,f1097,f982]) ).
fof(f1753,plain,
! [X0] :
( ~ sQ218_spl
| ~ sum(X0,s(n0),s(s(s(s(s(s(n0)))))))
| same(X0,s(s(s(s(s(s(s(s(n0))))))))) ),
inference(resolution,[status(thm)],[f1730,f25]) ).
fof(f1754,plain,
( ~ sQ218_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f1753,f652,f1729]) ).
fof(f1755,plain,
! [X0] :
( ~ sQ219_spl
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(n0),X0)
| same(s(X0),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(resolution,[status(thm)],[f1733,f25]) ).
fof(f1757,plain,
! [X0] :
( ~ sQ219_spl
| ~ sum(s(s(s(s(s(s(s(n0))))))),n0,X0)
| same(s(s(X0)),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(resolution,[status(thm)],[f1755,f25]) ).
fof(f1760,plain,
! [X0] :
( ~ sQ219_spl
| same(s(X0),s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),n0,X0) ),
inference(resolution,[status(thm)],[f1757,f31]) ).
fof(f1764,plain,
( ~ sQ219_spl
| same(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(n0)))))))) ),
inference(resolution,[status(thm)],[f1760,f24]) ).
fof(f1765,plain,
( ~ sQ219_spl
| same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(n0))))))) ),
inference(resolution,[status(thm)],[f1764,f31]) ).
fof(f1766,plain,
( ~ sQ219_spl
| same(s(s(s(s(s(s(n0)))))),s(s(s(s(s(n0)))))) ),
inference(resolution,[status(thm)],[f1765,f31]) ).
fof(f1767,plain,
( ~ sQ219_spl
| same(s(s(s(s(s(n0))))),s(s(s(s(n0))))) ),
inference(resolution,[status(thm)],[f1766,f31]) ).
fof(f1768,plain,
( ~ sQ219_spl
| same(s(s(s(s(n0)))),s(s(s(n0)))) ),
inference(resolution,[status(thm)],[f1767,f31]) ).
fof(f1769,plain,
( ~ sQ219_spl
| same(s(s(s(n0))),s(s(n0))) ),
inference(resolution,[status(thm)],[f1768,f31]) ).
fof(f1770,plain,
( ~ sQ219_spl
| same(s(s(n0)),s(n0)) ),
inference(resolution,[status(thm)],[f1769,f31]) ).
fof(f1771,plain,
( ~ sQ219_spl
| same(s(n0),n0) ),
inference(resolution,[status(thm)],[f1770,f31]) ).
fof(f1772,plain,
( ~ sQ219_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1771,f29]) ).
fof(f1773,plain,
~ sQ219_spl,
inference(contradiction_clause,[status(thm)],[f1772]) ).
fof(f1801,definition,
! [X2] :
( sQ227_spl
<=> ~ sum(s(s(s(n0))),s(n0),X2) ),
introduced(definition,[new_symbols(definition,[sQ227_spl])],[split_symbol_definition]) ).
fof(f1802,plain,
! [X0] :
( ~ sQ227_spl
| ~ sum(s(s(s(n0))),s(n0),X0) ),
inference(component_clause,[status(thm)],[f1801]) ).
fof(f1805,plain,
! [X0] :
( ~ sQ227_spl
| ~ sum(s(s(s(n0))),n0,X0) ),
inference(resolution,[status(thm)],[f1802,f25]) ).
fof(f1806,plain,
( ~ sQ227_spl
| $false ),
inference(resolution,[status(thm)],[f1805,f24]) ).
fof(f1807,plain,
~ sQ227_spl,
inference(contradiction_clause,[status(thm)],[f1806]) ).
fof(f1830,plain,
! [X0,X1,X2] :
( ~ sQ157_spl
| 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)
| same(X1,s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(n0))))),s(s(n0)),X1)
| same(X0,s(s(s(s(s(s(n0)))))))
| ~ sum(X0,s(s(n0)),s(s(s(s(s(n0)))))) ),
inference(resolution,[status(thm)],[f1255,f24]) ).
fof(f1831,definition,
! [X2] :
( sQ230_spl
<=> ( 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) ) ),
introduced(definition,[new_symbols(definition,[sQ230_spl])],[split_symbol_definition]) ).
fof(f1832,plain,
! [X0] :
( ~ sQ230_spl
| diagonal_attack(s(s(s(s(s(s(n0)))))),X0,cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| ~ sum(s(s(n0)),s(n0),X0) ),
inference(component_clause,[status(thm)],[f1831]) ).
fof(f1834,plain,
( ~ sQ157_spl
| sQ230_spl
| sQ161_spl
| sQ160_spl ),
inference(split_clause,[status(thm)],[f1830,f1270,f1273,f1831,f1238]) ).
fof(f1910,plain,
! [X0] :
( ~ sQ230_spl
| ~ sum(s(s(n0)),n0,X0)
| diagonal_attack(s(s(s(s(s(s(n0)))))),s(X0),cons(s(s(s(s(s(s(s(n0))))))),empty_list)) ),
inference(resolution,[status(thm)],[f1832,f25]) ).
fof(f1998,plain,
! [X0,X1,X2,X3] :
( ~ sQ230_spl
| diagonal_attack(s(s(s(s(s(s(n0)))))),X3,empty_list)
| ~ sum(s(X0),s(n0),X3)
| same(X2,s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(X0),X2)
| same(X1,s(s(s(s(s(s(n0)))))))
| ~ sum(X1,s(X0),s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(s(n0)),n0,X0) ),
inference(resolution,[status(thm)],[f1910,f34]) ).
fof(f1999,plain,
! [X0,X1,X2,X3] :
( ~ sQ230_spl
| ~ sum(s(X0),s(n0),X3)
| same(X2,s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(X0),X2)
| same(X1,s(s(s(s(s(s(n0)))))))
| ~ sum(X1,s(X0),s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(s(n0)),n0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1998,f35]) ).
fof(f2040,plain,
! [X0,X1,X2] :
( ~ sQ230_spl
| ~ sum(s(s(s(n0))),s(n0),X2)
| same(X1,s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(s(s(n0))),X1)
| same(X0,s(s(s(s(s(s(n0)))))))
| ~ sum(X0,s(s(s(n0))),s(s(s(s(s(s(s(n0)))))))) ),
inference(resolution,[status(thm)],[f1999,f24]) ).
fof(f2041,definition,
! [X0] :
( sQ248_spl
<=> ( 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,[sQ248_spl])],[split_symbol_definition]) ).
fof(f2042,plain,
! [X0] :
( ~ sQ248_spl
| same(X0,s(s(s(s(s(s(n0)))))))
| ~ sum(X0,s(s(s(n0))),s(s(s(s(s(s(s(n0)))))))) ),
inference(component_clause,[status(thm)],[f2041]) ).
fof(f2044,definition,
! [X1] :
( sQ249_spl
<=> ( same(X1,s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(s(s(n0))),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ249_spl])],[split_symbol_definition]) ).
fof(f2045,plain,
! [X0] :
( ~ sQ249_spl
| same(X0,s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(s(s(n0))),X0) ),
inference(component_clause,[status(thm)],[f2044]) ).
fof(f2047,plain,
( ~ sQ230_spl
| sQ227_spl
| sQ249_spl
| sQ248_spl ),
inference(split_clause,[status(thm)],[f2040,f2041,f2044,f1801,f1831]) ).
fof(f2048,plain,
! [X0] :
( ~ sQ248_spl
| ~ sum(X0,s(s(n0)),s(s(s(s(s(s(n0)))))))
| same(X0,s(s(s(s(s(s(n0))))))) ),
inference(resolution,[status(thm)],[f2042,f25]) ).
fof(f2049,plain,
! [X0] :
( ~ sQ248_spl
| ~ sum(X0,s(n0),s(s(s(s(s(n0))))))
| same(X0,s(s(s(s(s(s(n0))))))) ),
inference(resolution,[status(thm)],[f2048,f25]) ).
fof(f2050,plain,
( ~ sQ248_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f2049,f157,f2041]) ).
fof(f2051,plain,
! [X0] :
( ~ sQ249_spl
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(s(n0)),X0)
| same(s(X0),s(s(s(s(s(s(n0))))))) ),
inference(resolution,[status(thm)],[f2045,f25]) ).
fof(f2060,plain,
! [X0] :
( ~ sQ249_spl
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(n0),X0)
| same(s(s(X0)),s(s(s(s(s(s(n0))))))) ),
inference(resolution,[status(thm)],[f2051,f25]) ).
fof(f2061,plain,
! [X0] :
( ~ sQ249_spl
| ~ sum(s(s(s(s(s(s(s(n0))))))),n0,X0)
| same(s(s(s(X0))),s(s(s(s(s(s(n0))))))) ),
inference(resolution,[status(thm)],[f2060,f25]) ).
fof(f2062,plain,
! [X0] :
( ~ sQ249_spl
| same(s(s(X0)),s(s(s(s(s(n0))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),n0,X0) ),
inference(resolution,[status(thm)],[f2061,f31]) ).
fof(f2063,plain,
( ~ sQ249_spl
| same(s(s(s(s(s(s(s(s(s(n0))))))))),s(s(s(s(s(n0)))))) ),
inference(resolution,[status(thm)],[f2062,f24]) ).
fof(f2064,plain,
( ~ sQ249_spl
| same(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(n0))))) ),
inference(resolution,[status(thm)],[f2063,f31]) ).
fof(f2065,plain,
( ~ sQ249_spl
| same(s(s(s(s(s(s(s(n0))))))),s(s(s(n0)))) ),
inference(resolution,[status(thm)],[f2064,f31]) ).
fof(f2082,plain,
( ~ sQ249_spl
| same(s(s(s(s(s(s(n0)))))),s(s(n0))) ),
inference(resolution,[status(thm)],[f2065,f31]) ).
fof(f2083,plain,
( ~ sQ249_spl
| same(s(s(s(s(s(n0))))),s(n0)) ),
inference(resolution,[status(thm)],[f2082,f31]) ).
fof(f2084,plain,
( ~ sQ249_spl
| same(s(s(s(s(n0)))),n0) ),
inference(resolution,[status(thm)],[f2083,f31]) ).
fof(f2085,plain,
( ~ sQ249_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2084,f29]) ).
fof(f2086,plain,
~ sQ249_spl,
inference(contradiction_clause,[status(thm)],[f2085]) ).
fof(f2087,plain,
$false,
inference(sat_refutation,[status(thm)],[f59,f69,f76,f91,f99,f124,f219,f222,f266,f284,f315,f383,f427,f465,f569,f616,f700,f752,f763,f966,f985,f1103,f1228,f1241,f1268,f1302,f1314,f1735,f1754,f1773,f1807,f1834,f2047,f2050,f2086]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ034-1.004 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n015.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 03:50:06 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Drodi V4.1.1
% 4.74/1.06 % Refutation found
% 4.74/1.06 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 4.74/1.06 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.74/1.08 % Elapsed time: 0.706325 seconds
% 4.74/1.08 % CPU time: 5.335744 seconds
% 4.74/1.08 % Total memory used: 77.960 MB
% 4.74/1.08 % Net memory used: 64.459 MB
%------------------------------------------------------------------------------