%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : PUZ034-1.004 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n012.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 : Fri Sep 25 02:32:47 PM UTC 2026
% Result : Unsatisfiable 104.65s 27.27s
% Output : CNFRefutation 104.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 18
% Syntax : Number of formulae : 322 ( 68 unt; 0 def)
% Number of atoms : 960 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 1138 ( 500 ~; 638 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 13 ( 3 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 10 ( 9 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 561 ( 0 sgn 561 !; 0 ?; 516 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1] :
( ~ range(X3,X1,X2)
| ~ sum(X0,s(n0),X3)
| ~ less(X0,X1)
| range(X0,X1,cons(X0,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(X0,X1)
| less(s(X0),s(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,X2,X3)
| select(X0,cons(X1,X2),cons(X1,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(X0,X1)
| ~ same(s(X0),s(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',same_definition3) ).
fof(f12,axiom,
! [X0,X1] :
( ~ attack(X0,X1)
| diagonal_attack(X0,s(n0),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',attack) ).
fof(f13,axiom,
! [X2,X3,X0,X1,X6,X4,X5] :
( 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)) ),
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)
| attack(X3,X1)
| ~ select(X3,X0,X4)
| 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] :
( ~ do_queens(X4,empty_list,X1)
| ~ range(X2,X3,X4)
| ~ sum(X0,X0,X3)
| ~ sum(X0,s(n0),X2)
| queens(X0,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) ).
tcf(c_67,negated_conjecture,
! [X0: $i] : ~ queens(s(s(s(s(n0)))),X0),
inference(cnf_transformation,[],[f18]) ).
tcf(c_68,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( queens(X0,X4)
| ~ do_queens(X3,empty_list,X4)
| ~ sum(X0,X0,X2)
| ~ range(X1,X2,X3)
| ~ sum(X0,s(n0),X1) ),
inference(cnf_transformation,[],[f17]) ).
tcf(c_69,plain,
! [X0: $i] : range(X0,X0,cons(X0,empty_list)),
inference(cnf_transformation,[],[f2]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( range(X0,X2,cons(X0,X3))
| ~ less(X0,X2)
| ~ range(X1,X2,X3)
| ~ sum(X0,s(n0),X1) ),
inference(cnf_transformation,[],[f1]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i,X2: $i] :
( sum(X0,s(X1),s(X2))
| ~ sum(X0,X1,X2) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_72,plain,
! [X0: $i] : sum(X0,n0,X0),
inference(cnf_transformation,[],[f5]) ).
tcf(c_73,plain,
! [X0: $i] : do_queens(empty_list,X0,X0),
inference(cnf_transformation,[],[f16]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i] : ~ diagonal_attack(X0,X1,empty_list),
inference(cnf_transformation,[],[f14]) ).
tcf(c_75,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( attack(X1,X2)
| do_queens(X4,X2,X3)
| ~ select(X1,X4,X0)
| ~ do_queens(X0,cons(X1,X2),X3) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_76,plain,
! [X0: $i,X1: $i] :
( less(s(X0),s(X1))
| ~ less(X0,X1) ),
inference(cnf_transformation,[],[f4]) ).
tcf(c_77,plain,
! [X0: $i] : less(n0,s(X0)),
inference(cnf_transformation,[],[f3]) ).
tcf(c_78,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( same(X6,X0)
| same(X5,X0)
| diagonal_attack(X0,X4,X3)
| ~ sum(X6,X1,X2)
| ~ sum(X2,X1,X5)
| ~ sum(X1,s(n0),X4)
| ~ diagonal_attack(X0,X1,cons(X2,X3)) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_79,plain,
! [X0: $i,X1: $i] :
( diagonal_attack(X0,s(n0),X1)
| ~ attack(X0,X1) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_80,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( select(X0,cons(X3,X1),cons(X3,X2))
| ~ select(X0,X1,X2) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_81,plain,
! [X0: $i,X1: $i] : select(X0,cons(X0,X1),X1),
inference(cnf_transformation,[],[f7]) ).
tcf(c_82,plain,
! [X0: $i,X1: $i] :
( same(X0,X1)
| ~ same(s(X0),s(X1)) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_83,plain,
! [X0: $i] : ~ same(n0,s(X0)),
inference(cnf_transformation,[],[f10]) ).
tcf(c_84,plain,
! [X0: $i] : ~ same(s(X0),n0),
inference(cnf_transformation,[],[f9]) ).
tcf(c_85,plain,
less(n0,s(n0)),
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_89,plain,
~ same(n0,s(n0)),
inference(instantiation,[status(thm)],[c_83]) ).
tcf(c_181,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( do_queens(X4,X2,X3)
| diagonal_attack(X1,s(n0),X2)
| ~ select(X1,X4,X0)
| ~ do_queens(X0,cons(X1,X2),X3) ),
inference(resolution,[status(thm)],[c_79,c_75]) ).
tcf(c_199,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ do_queens(X2,empty_list,X3)
| ~ range(X1,X0,X2)
| ~ sum(s(s(s(s(n0)))),s(n0),X1)
| ~ sum(s(s(s(s(n0)))),s(s(s(s(n0)))),X0) ),
inference(resolution,[status(thm)],[c_68,c_67]) ).
tcf(c_287,plain,
! [X0: $i] :
( less(s(n0),s(s(X0)))
| ~ less(n0,s(X0)) ),
inference(instantiation,[status(thm)],[c_76]) ).
tcf(c_288,plain,
( less(s(n0),s(s(n0)))
| ~ less(n0,s(n0)) ),
inference(instantiation,[status(thm)],[c_287]) ).
tcf(c_289,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ do_queens(X2,empty_list,X3)
| ~ range(s(X1),X0,X2)
| ~ sum(s(s(s(s(n0)))),s(n0),s(X1))
| ~ sum(s(s(s(s(n0)))),s(s(s(s(n0)))),X0) ),
inference(instantiation,[status(thm)],[c_199]) ).
tcf(c_290,plain,
! [X0: $i] :
( sum(s(s(s(s(n0)))),s(n0),s(X0))
| ~ sum(s(s(s(s(n0)))),n0,X0) ),
inference(instantiation,[status(thm)],[c_71]) ).
tcf(c_300,plain,
! [X0: $i,X1: $i] :
( sum(X0,s(n0),s(X1))
| ~ sum(X0,n0,X1) ),
inference(instantiation,[status(thm)],[c_71]) ).
tcf(c_302,plain,
! [X0: $i] :
( less(s(s(n0)),s(s(s(X0))))
| ~ less(s(n0),s(s(X0))) ),
inference(instantiation,[status(thm)],[c_76]) ).
tcf(c_303,plain,
( less(s(s(n0)),s(s(s(n0))))
| ~ less(s(n0),s(s(n0))) ),
inference(instantiation,[status(thm)],[c_302]) ).
tcf(c_310,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ do_queens(X2,empty_list,X3)
| ~ range(s(X1),s(X0),X2)
| ~ sum(s(s(s(s(n0)))),s(n0),s(X1))
| ~ sum(s(s(s(s(n0)))),s(s(s(s(n0)))),s(X0)) ),
inference(instantiation,[status(thm)],[c_289]) ).
tcf(c_311,plain,
! [X0: $i] :
( sum(s(s(s(s(n0)))),s(s(s(s(n0)))),s(X0))
| ~ sum(s(s(s(s(n0)))),s(s(s(n0))),X0) ),
inference(instantiation,[status(thm)],[c_71]) ).
tcf(c_318,plain,
! [X0: $i] :
( less(s(s(s(n0))),s(s(s(s(X0)))))
| ~ less(s(s(n0)),s(s(s(X0)))) ),
inference(instantiation,[status(thm)],[c_76]) ).
tcf(c_319,plain,
( less(s(s(s(n0))),s(s(s(s(n0)))))
| ~ less(s(s(n0)),s(s(s(n0)))) ),
inference(instantiation,[status(thm)],[c_318]) ).
tcf(c_329,plain,
! [X0: $i] :
( sum(s(n0),s(n0),s(X0))
| ~ sum(s(n0),n0,X0) ),
inference(instantiation,[status(thm)],[c_300]) ).
tcf(c_332,plain,
! [X0: $i] :
( sum(s(s(s(s(n0)))),s(s(s(s(n0)))),s(s(X0)))
| ~ sum(s(s(s(s(n0)))),s(s(s(n0))),s(X0)) ),
inference(instantiation,[status(thm)],[c_311]) ).
tcf(c_333,plain,
! [X0: $i] :
( sum(s(s(s(s(n0)))),s(s(s(n0))),s(X0))
| ~ sum(s(s(s(s(n0)))),s(s(n0)),X0) ),
inference(instantiation,[status(thm)],[c_71]) ).
tcf(c_338,plain,
( sum(s(s(s(s(n0)))),s(n0),s(s(s(s(s(n0))))))
| ~ sum(s(s(s(s(n0)))),n0,s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[c_290]) ).
tcf(c_339,plain,
sum(s(s(s(s(n0)))),n0,s(s(s(s(n0))))),
inference(instantiation,[status(thm)],[c_72]) ).
tcf(c_346,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ do_queens(X1,empty_list,X2)
| ~ range(s(s(s(s(s(n0))))),s(X0),X1)
| ~ sum(s(s(s(s(n0)))),s(s(s(s(n0)))),s(X0))
| ~ sum(s(s(s(s(n0)))),s(n0),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[c_310]) ).
tcf(c_349,plain,
! [X0: $i] :
( less(s(s(s(s(n0)))),s(s(s(s(s(X0))))))
| ~ less(s(s(s(n0))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_76]) ).
tcf(c_350,plain,
( less(s(s(s(s(n0)))),s(s(s(s(s(n0))))))
| ~ less(s(s(s(n0))),s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[c_349]) ).
tcf(c_361,plain,
! [X0: $i] :
( sum(s(s(n0)),s(n0),s(X0))
| ~ sum(s(s(n0)),n0,X0) ),
inference(instantiation,[status(thm)],[c_300]) ).
tcf(c_366,plain,
( sum(s(n0),s(n0),s(s(n0)))
| ~ sum(s(n0),n0,s(n0)) ),
inference(instantiation,[status(thm)],[c_329]) ).
tcf(c_367,plain,
sum(s(n0),n0,s(n0)),
inference(instantiation,[status(thm)],[c_72]) ).
tcf(c_379,plain,
! [X0: $i] :
( less(s(s(s(s(s(n0))))),s(s(s(s(s(s(X0)))))))
| ~ less(s(s(s(s(n0)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_76]) ).
tcf(c_380,plain,
( less(s(s(s(s(s(n0))))),s(s(s(s(s(s(n0)))))))
| ~ less(s(s(s(s(n0)))),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[c_379]) ).
tcf(c_383,plain,
( sum(s(s(n0)),s(n0),s(s(s(n0))))
| ~ sum(s(s(n0)),n0,s(s(n0))) ),
inference(instantiation,[status(thm)],[c_361]) ).
tcf(c_384,plain,
sum(s(s(n0)),n0,s(s(n0))),
inference(instantiation,[status(thm)],[c_72]) ).
tcf(c_394,plain,
! [X0: $i] : ~ diagonal_attack(X0,s(n0),empty_list),
inference(instantiation,[status(thm)],[c_74]) ).
tcf(c_397,plain,
! [X0: $i] :
( sum(s(s(s(s(n0)))),s(s(s(n0))),s(s(X0)))
| ~ sum(s(s(s(s(n0)))),s(s(n0)),s(X0)) ),
inference(instantiation,[status(thm)],[c_333]) ).
tcf(c_398,plain,
! [X0: $i] :
( sum(s(s(s(s(n0)))),s(s(n0)),s(X0))
| ~ sum(s(s(s(s(n0)))),s(n0),X0) ),
inference(instantiation,[status(thm)],[c_71]) ).
tcf(c_404,plain,
! [X0: $i] :
( sum(s(s(s(n0))),s(n0),s(X0))
| ~ sum(s(s(s(n0))),n0,X0) ),
inference(instantiation,[status(thm)],[c_300]) ).
tcf(c_425,plain,
! [X0: $i] :
( less(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(X0))))))))
| ~ less(s(s(s(s(s(n0))))),s(s(s(s(s(s(X0))))))) ),
inference(instantiation,[status(thm)],[c_76]) ).
tcf(c_426,plain,
( less(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(n0))))))))
| ~ less(s(s(s(s(s(n0))))),s(s(s(s(s(s(n0))))))) ),
inference(instantiation,[status(thm)],[c_425]) ).
tcf(c_427,plain,
! [X0: $i,X1: $i,X2: $i] :
( range(s(s(s(s(s(n0))))),s(s(s(s(s(s(X0)))))),cons(s(s(s(s(s(n0))))),X2))
| ~ sum(s(s(s(s(s(n0))))),s(n0),X1)
| ~ range(X1,s(s(s(s(s(s(X0)))))),X2)
| ~ less(s(s(s(s(s(n0))))),s(s(s(s(s(s(X0))))))) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_434,plain,
( sum(s(s(s(s(n0)))),s(s(n0)),s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(n0)))),s(n0),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[c_398]) ).
tcf(c_435,plain,
( sum(s(s(s(n0))),s(n0),s(s(s(s(n0)))))
| ~ sum(s(s(s(n0))),n0,s(s(s(n0)))) ),
inference(instantiation,[status(thm)],[c_404]) ).
tcf(c_436,plain,
sum(s(s(s(n0))),n0,s(s(s(n0)))),
inference(instantiation,[status(thm)],[c_72]) ).
tcf(c_541,plain,
( sum(s(s(s(s(n0)))),s(s(s(n0))),s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(s(s(s(n0)))),s(s(n0)),s(s(s(s(s(s(n0))))))) ),
inference(instantiation,[status(thm)],[c_397]) ).
tcf(c_548,plain,
! [X0: $i] :
( less(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(s(X0)))))))))
| ~ less(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(X0)))))))) ),
inference(instantiation,[status(thm)],[c_76]) ).
tcf(c_549,plain,
( less(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(s(n0)))))))))
| ~ less(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(n0)))))))) ),
inference(instantiation,[status(thm)],[c_548]) ).
tcf(c_550,plain,
! [X0: $i,X1: $i,X2: $i] :
( range(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(X0))))))),cons(s(s(s(s(s(s(n0)))))),X2))
| ~ sum(s(s(s(s(s(s(n0)))))),s(n0),X1)
| ~ range(X1,s(s(s(s(s(s(s(X0))))))),X2)
| ~ less(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(X0)))))))) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_597,plain,
! [X0: $i,X1: $i,X2: $i] :
( range(s(s(s(s(s(n0))))),s(s(s(s(s(s(X0)))))),cons(s(s(s(s(s(n0))))),X2))
| ~ sum(s(s(s(s(s(n0))))),s(n0),s(X1))
| ~ range(s(X1),s(s(s(s(s(s(X0)))))),X2)
| ~ less(s(s(s(s(s(n0))))),s(s(s(s(s(s(X0))))))) ),
inference(instantiation,[status(thm)],[c_427]) ).
tcf(c_598,plain,
! [X0: $i] :
( sum(s(s(s(s(s(n0))))),s(n0),s(X0))
| ~ sum(s(s(s(s(s(n0))))),n0,X0) ),
inference(instantiation,[status(thm)],[c_300]) ).
tcf(c_707,plain,
( sum(s(s(s(s(n0)))),s(s(s(s(n0)))),s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(n0)))),s(s(s(n0))),s(s(s(s(s(s(s(n0)))))))) ),
inference(instantiation,[status(thm)],[c_332]) ).
tcf(c_713,plain,
! [X0: $i,X1: $i,X2: $i] :
( range(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(s(X0)))))))),cons(s(s(s(s(s(s(s(n0))))))),X2))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(n0),X1)
| ~ range(X1,s(s(s(s(s(s(s(s(X0)))))))),X2)
| ~ less(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(s(X0))))))))) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_749,plain,
! [X0: $i,X1: $i,X2: $i] :
( range(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(X0))))))),cons(s(s(s(s(s(s(n0)))))),X2))
| ~ sum(s(s(s(s(s(s(n0)))))),s(n0),s(X1))
| ~ range(s(X1),s(s(s(s(s(s(s(X0))))))),X2)
| ~ less(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(X0)))))))) ),
inference(instantiation,[status(thm)],[c_550]) ).
tcf(c_750,plain,
! [X0: $i] :
( sum(s(s(s(s(s(s(n0)))))),s(n0),s(X0))
| ~ sum(s(s(s(s(s(s(n0)))))),n0,X0) ),
inference(instantiation,[status(thm)],[c_300]) ).
tcf(c_755,plain,
( sum(s(s(s(s(s(n0))))),s(n0),s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(n0))))),n0,s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[c_598]) ).
tcf(c_756,plain,
sum(s(s(s(s(s(n0))))),n0,s(s(s(s(s(n0)))))),
inference(instantiation,[status(thm)],[c_72]) ).
tcf(c_843,plain,
! [X0: $i,X1: $i] :
( sum(s(X0),s(n0),s(X1))
| ~ sum(s(X0),n0,X1) ),
inference(instantiation,[status(thm)],[c_300]) ).
tcf(c_888,plain,
! [X0: $i,X1: $i] :
( ~ do_queens(X0,empty_list,X1)
| ~ sum(s(s(s(s(n0)))),s(n0),s(s(s(s(s(n0))))))
| ~ range(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(s(n0)))))))),X0)
| ~ sum(s(s(s(s(n0)))),s(s(s(s(n0)))),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(instantiation,[status(thm)],[c_346]) ).
tcf(c_890,plain,
( less(s(n0),s(s(s(n0))))
| ~ less(n0,s(s(n0))) ),
inference(instantiation,[status(thm)],[c_287]) ).
tcf(c_912,plain,
( less(s(s(s(n0))),s(s(s(s(s(n0))))))
| ~ less(s(s(n0)),s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[c_318]) ).
tcf(c_917,plain,
! [X0: $i,X1: $i] :
( range(s(s(s(s(s(n0))))),s(s(s(s(s(s(X0)))))),cons(s(s(s(s(s(n0))))),X1))
| ~ less(s(s(s(s(s(n0))))),s(s(s(s(s(s(X0)))))))
| ~ sum(s(s(s(s(s(n0))))),s(n0),s(s(s(s(s(s(n0)))))))
| ~ range(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(X0)))))),X1) ),
inference(instantiation,[status(thm)],[c_597]) ).
tcf(c_943,plain,
( sum(s(s(s(s(s(s(n0)))))),s(n0),s(s(s(s(s(s(s(n0))))))))
| ~ sum(s(s(s(s(s(s(n0)))))),n0,s(s(s(s(s(s(n0))))))) ),
inference(instantiation,[status(thm)],[c_750]) ).
tcf(c_944,plain,
sum(s(s(s(s(s(s(n0)))))),n0,s(s(s(s(s(s(n0))))))),
inference(instantiation,[status(thm)],[c_72]) ).
tcf(c_945,plain,
! [X0: $i] :
( sum(s(X0),s(n0),s(s(X0)))
| ~ sum(s(X0),n0,s(X0)) ),
inference(instantiation,[status(thm)],[c_843]) ).
tcf(c_946,plain,
! [X0: $i] : sum(s(X0),n0,s(X0)),
inference(instantiation,[status(thm)],[c_72]) ).
tcf(c_1118,plain,
less(n0,s(s(n0))),
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_1119,plain,
( less(s(s(n0)),s(s(s(s(n0)))))
| ~ less(s(n0),s(s(s(n0)))) ),
inference(instantiation,[status(thm)],[c_302]) ).
tcf(c_1129,plain,
! [X0: $i,X1: $i] :
( range(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(X0))))))),cons(s(s(s(s(s(s(n0)))))),X1))
| ~ less(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(X0))))))))
| ~ sum(s(s(s(s(s(s(n0)))))),s(n0),s(s(s(s(s(s(s(n0))))))))
| ~ range(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(X0))))))),X1) ),
inference(instantiation,[status(thm)],[c_749]) ).
tcf(c_1186,plain,
( sum(s(s(s(s(s(s(s(n0))))))),s(n0),s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),n0,s(s(s(s(s(s(s(n0)))))))) ),
inference(instantiation,[status(thm)],[c_945]) ).
tcf(c_1187,plain,
! [X0: $i,X1: $i] :
( range(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(s(X0)))))))),cons(s(s(s(s(s(s(s(n0))))))),X1))
| ~ less(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(s(X0)))))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(n0),s(s(s(s(s(s(s(s(n0)))))))))
| ~ range(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(X0)))))))),X1) ),
inference(instantiation,[status(thm)],[c_713]) ).
tcf(c_1233,plain,
( sum(s(s(s(s(s(s(s(s(n0)))))))),s(n0),s(s(s(s(s(s(s(s(s(n0))))))))))
| ~ sum(s(s(s(s(s(s(s(s(n0)))))))),n0,s(s(s(s(s(s(s(s(n0))))))))) ),
inference(instantiation,[status(thm)],[c_945]) ).
tcf(c_1270,plain,
! [X0: $i,X1: $i] :
( sum(X0,s(s(n0)),s(X1))
| ~ sum(X0,s(n0),X1) ),
inference(instantiation,[status(thm)],[c_71]) ).
tcf(c_1274,plain,
! [X0: $i,X1: $i] :
( sum(X0,s(s(s(n0))),s(X1))
| ~ sum(X0,s(s(n0)),X1) ),
inference(instantiation,[status(thm)],[c_71]) ).
tcf(c_1492,plain,
sum(s(s(s(s(s(s(s(n0))))))),n0,s(s(s(s(s(s(s(n0)))))))),
inference(instantiation,[status(thm)],[c_946]) ).
tcf(c_1546,plain,
sum(s(s(s(s(s(s(s(s(n0)))))))),n0,s(s(s(s(s(s(s(s(n0))))))))),
inference(instantiation,[status(thm)],[c_946]) ).
tcf(c_1694,plain,
! [X0: $i,X1: $i] :
( sum(X0,s(s(n0)),s(s(X1)))
| ~ sum(X0,s(n0),s(X1)) ),
inference(instantiation,[status(thm)],[c_1270]) ).
tcf(c_2333,plain,
( less(s(n0),s(s(s(s(n0)))))
| ~ less(n0,s(s(s(n0)))) ),
inference(instantiation,[status(thm)],[c_287]) ).
tcf(c_2334,plain,
( less(s(s(n0)),s(s(s(s(s(n0))))))
| ~ less(s(n0),s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[c_302]) ).
tcf(c_2347,plain,
( less(s(s(s(s(n0)))),s(s(s(s(s(s(n0)))))))
| ~ less(s(s(s(n0))),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[c_349]) ).
tcf(c_2428,plain,
! [X0: $i,X1: $i] :
( sum(X0,s(s(s(n0))),s(s(s(X1))))
| ~ sum(X0,s(s(n0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_1274]) ).
tcf(c_2513,plain,
( range(s(s(s(s(s(s(s(n0))))))),s(s(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)))
| ~ less(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(n0),s(s(s(s(s(s(s(s(n0)))))))))
| ~ range(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(s(s(n0)))))))),empty_list)) ),
inference(instantiation,[status(thm)],[c_1187]) ).
tcf(c_2514,plain,
range(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(s(s(n0)))))))),empty_list)),
inference(instantiation,[status(thm)],[c_69]) ).
tcf(c_2535,plain,
! [X0: $i] :
( sum(s(s(s(s(s(s(n0)))))),s(s(n0)),s(s(X0)))
| ~ sum(s(s(s(s(s(s(n0)))))),s(n0),s(X0)) ),
inference(instantiation,[status(thm)],[c_1694]) ).
tcf(c_2933,plain,
less(n0,s(s(s(n0)))),
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_2938,plain,
( less(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(n0))))))))
| ~ less(s(s(s(s(n0)))),s(s(s(s(s(s(n0))))))) ),
inference(instantiation,[status(thm)],[c_379]) ).
tcf(c_3017,plain,
( range(s(s(s(s(s(s(n0)))))),s(s(s(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))))
| ~ less(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(s(s(n0)))))),s(n0),s(s(s(s(s(s(s(n0))))))))
| ~ range(s(s(s(s(s(s(s(n0))))))),s(s(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))) ),
inference(instantiation,[status(thm)],[c_1129]) ).
tcf(c_3065,plain,
( sum(s(s(s(s(s(s(n0)))))),s(s(n0)),s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(s(s(n0)))))),s(n0),s(s(s(s(s(s(s(n0)))))))) ),
inference(instantiation,[status(thm)],[c_2535]) ).
tcf(c_3222,plain,
! [X0: $i,X1: $i] :
( sum(s(s(X0)),s(s(n0)),s(s(X1)))
| ~ sum(s(s(X0)),s(n0),s(X1)) ),
inference(instantiation,[status(thm)],[c_1694]) ).
tcf(c_3274,plain,
! [X0: $i,X1: $i] :
( sum(s(X0),s(s(s(n0))),s(s(s(X1))))
| ~ sum(s(X0),s(s(n0)),s(s(X1))) ),
inference(instantiation,[status(thm)],[c_2428]) ).
tcf(c_3638,plain,
( less(s(s(s(n0))),s(s(s(s(s(s(n0)))))))
| ~ less(s(s(n0)),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[c_318]) ).
tcf(c_3642,plain,
( less(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(n0)))))))))
| ~ less(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(n0)))))))) ),
inference(instantiation,[status(thm)],[c_425]) ).
tcf(c_3806,plain,
( sum(s(s(s(n0))),s(s(n0)),s(s(s(s(s(n0))))))
| ~ sum(s(s(s(n0))),s(n0),s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[c_3222]) ).
tcf(c_3809,plain,
! [X0: $i] :
( sum(s(s(X0)),s(s(n0)),s(s(s(s(X0)))))
| ~ sum(s(s(X0)),s(n0),s(s(s(X0)))) ),
inference(instantiation,[status(thm)],[c_3222]) ).
tcf(c_3883,plain,
( sum(s(s(s(s(s(s(n0)))))),s(s(s(n0))),s(s(s(s(s(s(s(s(s(n0))))))))))
| ~ sum(s(s(s(s(s(s(n0)))))),s(s(n0)),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(instantiation,[status(thm)],[c_3274]) ).
tcf(c_5220,plain,
( less(s(s(s(s(n0)))),s(s(s(s(s(s(s(n0))))))))
| ~ less(s(s(s(n0))),s(s(s(s(s(s(n0))))))) ),
inference(instantiation,[status(thm)],[c_349]) ).
tcf(c_5226,plain,
( range(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(s(n0)))))))),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)))))
| ~ sum(s(s(s(s(s(n0))))),s(n0),s(s(s(s(s(s(n0)))))))
| ~ less(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(s(n0)))))))))
| ~ range(s(s(s(s(s(s(n0)))))),s(s(s(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)))) ),
inference(instantiation,[status(thm)],[c_917]) ).
tcf(c_5331,plain,
( sum(s(s(s(n0))),s(s(s(n0))),s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(n0))),s(s(n0)),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[c_3274]) ).
tcf(c_9383,plain,
( less(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(s(n0)))))))))
| ~ less(s(s(s(s(n0)))),s(s(s(s(s(s(s(n0)))))))) ),
inference(instantiation,[status(thm)],[c_379]) ).
tcf(c_9751,plain,
~ same(s(s(s(n0))),n0),
inference(instantiation,[status(thm)],[c_84]) ).
tcf(c_9752,plain,
~ same(s(s(n0)),n0),
inference(instantiation,[status(thm)],[c_84]) ).
tcf(c_10210,plain,
! [X0: $i,X1: $i] :
( same(s(s(s(s(X0)))),X1)
| ~ same(s(s(s(s(s(X0))))),s(X1)) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_10212,plain,
( same(s(s(s(s(n0)))),n0)
| ~ same(s(s(s(s(s(n0))))),s(n0)) ),
inference(instantiation,[status(thm)],[c_10210]) ).
tcf(c_10396,plain,
( sum(s(s(s(s(s(s(s(s(n0)))))))),s(s(n0)),s(s(s(s(s(s(s(s(s(s(n0)))))))))))
| ~ sum(s(s(s(s(s(s(s(s(n0)))))))),s(n0),s(s(s(s(s(s(s(s(s(n0)))))))))) ),
inference(instantiation,[status(thm)],[c_3809]) ).
tcf(c_10546,plain,
! [X0: $i] : ~ same(s(s(s(X0))),n0),
inference(instantiation,[status(thm)],[c_84]) ).
tcf(c_11694,plain,
! [X0: $i] :
( ~ sum(s(s(s(s(n0)))),s(n0),s(s(s(s(s(n0))))))
| ~ sum(s(s(s(s(n0)))),s(s(s(s(n0)))),s(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))))))),cons(s(s(s(s(s(s(s(s(n0)))))))),empty_list)))),empty_list,X0)
| ~ range(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(s(n0)))))))),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))))) ),
inference(instantiation,[status(thm)],[c_888]) ).
tcf(c_12304,plain,
~ same(s(s(s(s(n0)))),n0),
inference(instantiation,[status(thm)],[c_10546]) ).
tcf(c_12801,plain,
! [X0: $i,X1: $i] :
( same(s(X0),X1)
| ~ same(s(s(X0)),s(X1)) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_21230,plain,
! [X0: $i] :
( same(s(s(n0)),X0)
| ~ same(s(s(s(n0))),s(X0)) ),
inference(instantiation,[status(thm)],[c_12801]) ).
tcf(c_21231,plain,
( same(s(s(n0)),n0)
| ~ same(s(s(s(n0))),s(n0)) ),
inference(instantiation,[status(thm)],[c_21230]) ).
tcf(c_21432,plain,
! [X0: $i,X1: $i] :
( same(s(s(X0)),X1)
| ~ same(s(s(s(X0))),s(X1)) ),
inference(instantiation,[status(thm)],[c_12801]) ).
tcf(c_21973,plain,
! [X0: $i] :
( same(n0,s(X0))
| ~ same(s(n0),s(s(X0))) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_21974,plain,
( same(n0,s(n0))
| ~ same(s(n0),s(s(n0))) ),
inference(instantiation,[status(thm)],[c_21973]) ).
tcf(c_28361,plain,
! [X0: $i] : ~ diagonal_attack(s(X0),s(n0),empty_list),
inference(instantiation,[status(thm)],[c_394]) ).
tcf(c_30796,plain,
! [X0: $i] :
( same(s(s(s(n0))),X0)
| ~ same(s(s(s(s(n0)))),s(X0)) ),
inference(instantiation,[status(thm)],[c_21432]) ).
tcf(c_30797,plain,
( same(s(s(s(n0))),n0)
| ~ same(s(s(s(s(n0)))),s(n0)) ),
inference(instantiation,[status(thm)],[c_30796]) ).
tcf(c_42664,plain,
! [X0: $i] : ~ diagonal_attack(s(s(X0)),s(n0),empty_list),
inference(instantiation,[status(thm)],[c_28361]) ).
tcf(c_62006,plain,
~ diagonal_attack(s(s(s(s(s(s(n0)))))),s(n0),empty_list),
inference(instantiation,[status(thm)],[c_42664]) ).
tcf(c_70018,plain,
! [X0: $i] :
( same(n0,s(X0))
| ~ same(s(n0),s(s(X0))) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_70033,plain,
! [X0: $i] :
( same(s(s(X0)),s(n0))
| ~ same(s(s(s(X0))),s(s(n0))) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_70037,plain,
! [X0: $i] :
( same(s(n0),s(s(X0)))
| ~ same(s(s(n0)),s(s(s(X0)))) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_70038,plain,
( same(s(n0),s(s(n0)))
| ~ same(s(s(n0)),s(s(s(n0)))) ),
inference(instantiation,[status(thm)],[c_70037]) ).
tcf(c_70064,plain,
! [X0: $i] :
( same(s(s(s(X0))),s(s(n0)))
| ~ same(s(s(s(s(X0)))),s(s(s(n0)))) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_70068,plain,
! [X0: $i] :
( same(s(s(n0)),s(s(s(X0))))
| ~ same(s(s(s(n0))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_70069,plain,
( same(s(s(n0)),s(s(s(n0))))
| ~ same(s(s(s(n0))),s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[c_70068]) ).
tcf(c_70108,plain,
! [X0: $i,X1: $i] : ~ diagonal_attack(s(X0),s(X1),empty_list),
inference(instantiation,[status(thm)],[c_74]) ).
tcf(c_70113,plain,
! [X0: $i] :
( same(s(s(s(s(X0)))),s(s(s(n0))))
| ~ same(s(s(s(s(s(X0))))),s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_70117,plain,
! [X0: $i] :
( same(s(s(s(n0))),s(s(s(s(X0)))))
| ~ same(s(s(s(s(n0)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_70118,plain,
( same(s(s(s(n0))),s(s(s(s(n0)))))
| ~ same(s(s(s(s(n0)))),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[c_70117]) ).
tcf(c_70192,plain,
! [X0: $i] :
( same(s(s(s(s(s(X0))))),s(s(s(s(n0)))))
| ~ same(s(s(s(s(s(s(X0)))))),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_70196,plain,
! [X0: $i] :
( same(s(s(s(s(n0)))),s(s(s(s(s(X0))))))
| ~ same(s(s(s(s(s(n0))))),s(s(s(s(s(s(X0))))))) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_70197,plain,
( same(s(s(s(s(n0)))),s(s(s(s(s(n0))))))
| ~ same(s(s(s(s(s(n0))))),s(s(s(s(s(s(n0))))))) ),
inference(instantiation,[status(thm)],[c_70196]) ).
tcf(c_70333,plain,
! [X0: $i,X1: $i] : ~ diagonal_attack(s(s(s(X0))),s(X1),empty_list),
inference(instantiation,[status(thm)],[c_70108]) ).
tcf(c_70369,plain,
! [X0: $i] :
( same(s(s(s(s(s(s(X0)))))),s(s(s(s(s(n0))))))
| ~ same(s(s(s(s(s(s(s(X0))))))),s(s(s(s(s(s(n0))))))) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_70373,plain,
! [X0: $i] :
( same(s(s(s(s(s(n0))))),s(s(s(s(s(s(X0)))))))
| ~ same(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(X0)))))))) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_70374,plain,
( same(s(s(s(s(s(n0))))),s(s(s(s(s(s(n0)))))))
| ~ same(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(n0)))))))) ),
inference(instantiation,[status(thm)],[c_70373]) ).
tcf(c_70810,plain,
! [X0: $i] :
( same(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(X0))))))))
| ~ same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(s(X0))))))))) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_70811,plain,
( same(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(n0))))))))
| ~ same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(instantiation,[status(thm)],[c_70810]) ).
tcf(c_71499,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( same(X5,s(s(s(s(s(s(s(s(X0)))))))))
| diagonal_attack(s(s(s(s(s(s(s(s(X0)))))))),X4,X3)
| same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(s(X0)))))))))
| ~ sum(X5,X1,X2)
| ~ sum(X1,s(n0),X4)
| ~ sum(X2,X1,s(s(s(s(s(s(s(n0))))))))
| ~ diagonal_attack(s(s(s(s(s(s(s(s(X0)))))))),X1,cons(X2,X3)) ),
inference(instantiation,[status(thm)],[c_78]) ).
tcf(c_72006,plain,
! [X0: $i] : ~ diagonal_attack(s(s(s(X0))),s(s(s(n0))),empty_list),
inference(instantiation,[status(thm)],[c_70333]) ).
tcf(c_73676,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( same(X5,s(s(s(s(s(s(s(s(X0)))))))))
| diagonal_attack(s(s(s(s(s(s(s(s(X0)))))))),s(X4),X3)
| same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(s(X0)))))))))
| ~ sum(X5,X1,X2)
| ~ sum(X1,s(n0),s(X4))
| ~ sum(X2,X1,s(s(s(s(s(s(s(n0))))))))
| ~ diagonal_attack(s(s(s(s(s(s(s(s(X0)))))))),X1,cons(X2,X3)) ),
inference(instantiation,[status(thm)],[c_71499]) ).
tcf(c_77362,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( same(X2,s(s(s(s(s(s(s(s(X0)))))))))
| diagonal_attack(s(s(s(s(s(s(s(s(X0)))))))),s(X3),X1)
| same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(s(X0)))))))))
| ~ sum(s(n0),s(n0),s(X3))
| ~ sum(X2,s(n0),s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(s(n0)))))),s(n0),s(s(s(s(s(s(s(n0))))))))
| ~ diagonal_attack(s(s(s(s(s(s(s(s(X0)))))))),s(n0),cons(s(s(s(s(s(s(n0)))))),X1)) ),
inference(instantiation,[status(thm)],[c_73676]) ).
tcf(c_78033,plain,
( same(s(s(s(s(n0)))),s(s(n0)))
| ~ same(s(s(s(s(s(n0))))),s(s(s(n0)))) ),
inference(instantiation,[status(thm)],[c_70064]) ).
tcf(c_78408,plain,
( same(s(s(s(s(n0)))),s(n0))
| ~ same(s(s(s(s(s(n0))))),s(s(n0))) ),
inference(instantiation,[status(thm)],[c_70033]) ).
tcf(c_81027,plain,
! [X0: $i] :
( same(s(s(s(s(X0)))),s(n0))
| ~ same(s(s(s(s(s(X0))))),s(s(n0))) ),
inference(instantiation,[status(thm)],[c_70033]) ).
tcf(c_81084,plain,
! [X0: $i,X1: $i,X2: $i] :
( same(X2,s(s(s(s(s(s(s(s(X0)))))))))
| diagonal_attack(s(s(s(s(s(s(s(s(X0)))))))),s(s(n0)),X1)
| same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(s(X0)))))))))
| ~ sum(s(n0),s(n0),s(s(n0)))
| ~ sum(X2,s(n0),s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(s(n0)))))),s(n0),s(s(s(s(s(s(s(n0))))))))
| ~ diagonal_attack(s(s(s(s(s(s(s(s(X0)))))))),s(n0),cons(s(s(s(s(s(s(n0)))))),X1)) ),
inference(instantiation,[status(thm)],[c_77362]) ).
tcf(c_82422,plain,
( same(s(s(s(n0))),s(n0))
| ~ same(s(s(s(s(n0)))),s(s(n0))) ),
inference(instantiation,[status(thm)],[c_70033]) ).
tcf(c_84132,plain,
( same(s(s(s(s(s(s(n0)))))),s(s(s(n0))))
| ~ same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[c_70113]) ).
tcf(c_84719,plain,
! [X0: $i] :
( same(n0,s(s(s(X0))))
| ~ same(s(n0),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_70018]) ).
tcf(c_84720,plain,
( same(n0,s(s(s(n0))))
| ~ same(s(n0),s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[c_84719]) ).
tcf(c_84758,plain,
~ same(n0,s(s(s(n0)))),
inference(instantiation,[status(thm)],[c_83]) ).
tcf(c_85394,plain,
( same(s(s(s(s(s(n0))))),s(n0))
| ~ same(s(s(s(s(s(s(n0)))))),s(s(n0))) ),
inference(instantiation,[status(thm)],[c_81027]) ).
tcf(c_85401,plain,
! [X0: $i] : ~ same(n0,s(s(s(X0)))),
inference(instantiation,[status(thm)],[c_83]) ).
tcf(c_85464,plain,
( same(s(s(s(s(s(n0))))),s(s(s(n0))))
| ~ same(s(s(s(s(s(s(n0)))))),s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[c_70113]) ).
tcf(c_86560,plain,
! [X0: $i] :
( same(s(n0),s(s(s(s(X0)))))
| ~ same(s(s(n0)),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_70037]) ).
tcf(c_86561,plain,
( same(s(n0),s(s(s(s(n0)))))
| ~ same(s(s(n0)),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[c_86560]) ).
tcf(c_86577,plain,
! [X0: $i,X1: $i] :
( diagonal_attack(s(s(s(s(s(s(s(s(X0)))))))),s(s(n0)),X1)
| same(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(s(X0)))))))))
| same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(s(X0)))))))))
| ~ sum(s(n0),s(n0),s(s(n0)))
| ~ sum(s(s(s(s(s(n0))))),s(n0),s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(s(n0)))))),s(n0),s(s(s(s(s(s(s(n0))))))))
| ~ diagonal_attack(s(s(s(s(s(s(s(s(X0)))))))),s(n0),cons(s(s(s(s(s(s(n0)))))),X1)) ),
inference(instantiation,[status(thm)],[c_81084]) ).
tcf(c_87171,plain,
! [X0: $i] :
( same(s(s(s(s(s(X0))))),s(s(s(n0))))
| ~ same(s(s(s(s(s(s(X0)))))),s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[c_70113]) ).
tcf(c_89687,plain,
( same(s(s(s(s(s(n0))))),s(s(n0)))
| ~ same(s(s(s(s(s(s(n0)))))),s(s(s(n0)))) ),
inference(instantiation,[status(thm)],[c_70064]) ).
tcf(c_91068,plain,
( same(s(s(s(s(s(s(s(n0))))))),s(s(s(n0))))
| ~ same(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[c_87171]) ).
tcf(c_92268,plain,
( same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(n0)))))
| ~ same(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[c_70192]) ).
tcf(c_94380,plain,
! [X0: $i] :
( diagonal_attack(s(s(s(s(s(s(s(s(X0)))))))),s(s(n0)),empty_list)
| same(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(s(X0)))))))))
| same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(s(X0)))))))))
| ~ sum(s(n0),s(n0),s(s(n0)))
| ~ sum(s(s(s(s(s(n0))))),s(n0),s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(s(n0)))))),s(n0),s(s(s(s(s(s(s(n0))))))))
| ~ diagonal_attack(s(s(s(s(s(s(s(s(X0)))))))),s(n0),cons(s(s(s(s(s(s(n0)))))),empty_list)) ),
inference(instantiation,[status(thm)],[c_86577]) ).
tcf(c_94382,plain,
( diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(s(n0)),empty_list)
| same(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(s(n0)))))))))
| same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(n0),s(n0),s(s(n0)))
| ~ sum(s(s(s(s(s(n0))))),s(n0),s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(s(n0)))))),s(n0),s(s(s(s(s(s(s(n0))))))))
| ~ diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(n0),cons(s(s(s(s(s(s(n0)))))),empty_list)) ),
inference(instantiation,[status(thm)],[c_94380]) ).
tcf(c_94641,plain,
! [X0: $i] :
( same(s(s(s(s(s(s(s(X0))))))),s(s(s(s(n0)))))
| ~ same(s(s(s(s(s(s(s(s(X0)))))))),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[c_70192]) ).
tcf(c_94642,plain,
! [X0: $i] :
( same(s(s(s(s(s(s(X0)))))),s(s(s(s(n0)))))
| ~ same(s(s(s(s(s(s(s(X0))))))),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[c_70192]) ).
tcf(c_94643,plain,
( same(s(s(s(s(s(s(n0)))))),s(s(s(s(n0)))))
| ~ same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[c_94642]) ).
tcf(c_98121,plain,
( same(s(s(s(s(s(s(n0)))))),s(s(n0)))
| ~ same(s(s(s(s(s(s(s(n0))))))),s(s(s(n0)))) ),
inference(instantiation,[status(thm)],[c_70064]) ).
tcf(c_98972,plain,
( same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(n0))))))
| ~ same(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(n0))))))) ),
inference(instantiation,[status(thm)],[c_70369]) ).
tcf(c_98978,plain,
( same(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(n0))))))
| ~ same(s(s(s(s(s(s(s(s(s(n0))))))))),s(s(s(s(s(s(n0))))))) ),
inference(instantiation,[status(thm)],[c_70369]) ).
tcf(c_102967,plain,
( same(s(s(n0)),s(s(s(s(s(n0))))))
| ~ same(s(s(s(n0))),s(s(s(s(s(s(n0))))))) ),
inference(instantiation,[status(thm)],[c_70068]) ).
tcf(c_103060,plain,
( same(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(n0)))))
| ~ same(s(s(s(s(s(s(s(s(s(n0))))))))),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[c_94641]) ).
tcf(c_121551,plain,
( same(s(n0),s(s(s(s(s(n0))))))
| ~ same(s(s(n0)),s(s(s(s(s(s(n0))))))) ),
inference(instantiation,[status(thm)],[c_86560]) ).
tcf(c_134701,plain,
( same(n0,s(s(s(s(n0)))))
| ~ same(s(n0),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[c_84719]) ).
tcf(c_137319,plain,
~ diagonal_attack(s(s(s(s(s(n0))))),s(s(s(n0))),empty_list),
inference(instantiation,[status(thm)],[c_72006]) ).
tcf(c_138952,plain,
~ same(n0,s(s(s(s(n0))))),
inference(instantiation,[status(thm)],[c_85401]) ).
tcf(c_144323,plain,
! [X0: $i] :
( same(s(s(n0)),s(s(s(X0))))
| ~ same(s(s(s(n0))),s(s(s(s(X0))))) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_144332,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( same(X5,X0)
| same(X4,X0)
| diagonal_attack(X0,X3,X2)
| ~ sum(X5,s(n0),X1)
| ~ sum(X1,s(n0),X4)
| ~ sum(s(n0),s(n0),X3)
| ~ diagonal_attack(X0,s(n0),cons(X1,X2)) ),
inference(instantiation,[status(thm)],[c_78]) ).
tcf(c_144342,plain,
! [X0: $i] :
( same(s(s(s(n0))),s(s(s(s(X0)))))
| ~ same(s(s(s(s(n0)))),s(s(s(s(s(X0)))))) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_144356,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( same(X4,X0)
| same(X3,X0)
| diagonal_attack(X0,s(s(n0)),X2)
| ~ sum(X4,s(n0),X1)
| ~ sum(X1,s(n0),X3)
| ~ diagonal_attack(X0,s(n0),cons(X1,X2))
| ~ sum(s(n0),s(n0),s(s(n0))) ),
inference(instantiation,[status(thm)],[c_144332]) ).
tcf(c_144580,plain,
! [X0: $i] :
( same(s(s(s(s(s(s(s(X0))))))),s(s(s(s(s(s(n0)))))))
| ~ same(s(s(s(s(s(s(s(s(X0)))))))),s(s(s(s(s(s(s(n0)))))))) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_145785,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( same(X5,X0)
| same(X4,X0)
| diagonal_attack(X0,X3,X2)
| ~ sum(X5,s(s(n0)),X1)
| ~ sum(X1,s(s(n0)),X4)
| ~ sum(s(s(n0)),s(n0),X3)
| ~ diagonal_attack(X0,s(s(n0)),cons(X1,X2)) ),
inference(instantiation,[status(thm)],[c_78]) ).
tcf(c_146684,plain,
~ diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(s(n0)),empty_list),
inference(instantiation,[status(thm)],[c_74]) ).
tcf(c_146689,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( same(X4,X0)
| same(X3,X0)
| diagonal_attack(X0,X5,X2)
| ~ sum(s(s(n0)),s(n0),X5)
| ~ sum(X4,s(s(n0)),s(X1))
| ~ sum(s(X1),s(s(n0)),X3)
| ~ diagonal_attack(X0,s(s(n0)),cons(s(X1),X2)) ),
inference(instantiation,[status(thm)],[c_145785]) ).
tcf(c_147630,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( same(X2,X0)
| diagonal_attack(X0,X3,X1)
| same(s(s(s(s(n0)))),X0)
| ~ sum(s(s(n0)),s(n0),X3)
| ~ sum(s(s(s(s(s(s(n0)))))),s(s(n0)),X2)
| ~ diagonal_attack(X0,s(s(n0)),cons(s(s(s(s(s(s(n0)))))),X1))
| ~ sum(s(s(s(s(n0)))),s(s(n0)),s(s(s(s(s(s(n0))))))) ),
inference(instantiation,[status(thm)],[c_146689]) ).
tcf(c_148706,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( same(X4,X0)
| same(X3,X0)
| diagonal_attack(X0,X5,X2)
| ~ sum(s(s(n0)),s(n0),X5)
| ~ sum(X4,s(s(n0)),s(s(X1)))
| ~ sum(s(s(X1)),s(s(n0)),X3)
| ~ diagonal_attack(X0,s(s(n0)),cons(s(s(X1)),X2)) ),
inference(instantiation,[status(thm)],[c_146689]) ).
tcf(c_149389,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( diagonal_attack(X0,X3,X1)
| same(s(s(X2)),X0)
| same(s(s(s(s(n0)))),X0)
| ~ sum(s(s(n0)),s(n0),X3)
| ~ sum(s(s(s(s(s(s(n0)))))),s(s(n0)),s(s(X2)))
| ~ diagonal_attack(X0,s(s(n0)),cons(s(s(s(s(s(s(n0)))))),X1))
| ~ sum(s(s(s(s(n0)))),s(s(n0)),s(s(s(s(s(s(n0))))))) ),
inference(instantiation,[status(thm)],[c_147630]) ).
tcf(c_151961,plain,
! [X0: $i] :
( same(s(s(s(s(s(s(s(s(s(X0))))))))),s(s(s(s(s(s(n0)))))))
| ~ same(s(s(s(s(s(s(s(s(s(s(X0)))))))))),s(s(s(s(s(s(s(n0)))))))) ),
inference(instantiation,[status(thm)],[c_144580]) ).
tcf(c_151962,plain,
( same(s(s(s(s(s(s(s(s(s(n0))))))))),s(s(s(s(s(s(n0)))))))
| ~ same(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(n0)))))))) ),
inference(instantiation,[status(thm)],[c_151961]) ).
tcf(c_153262,plain,
! [X0: $i,X1: $i,X2: $i] :
( diagonal_attack(X0,X2,X1)
| same(s(s(s(s(n0)))),X0)
| same(s(s(s(s(s(s(s(s(n0)))))))),X0)
| ~ sum(s(s(n0)),s(n0),X2)
| ~ diagonal_attack(X0,s(s(n0)),cons(s(s(s(s(s(s(n0)))))),X1))
| ~ sum(s(s(s(s(n0)))),s(s(n0)),s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(s(n0)))))),s(s(n0)),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(instantiation,[status(thm)],[c_149389]) ).
tcf(c_164068,plain,
! [X0: $i,X1: $i,X2: $i] :
( diagonal_attack(s(X0),X2,X1)
| same(s(s(s(s(n0)))),s(X0))
| same(s(s(s(s(s(s(s(s(n0)))))))),s(X0))
| ~ sum(s(s(n0)),s(n0),X2)
| ~ diagonal_attack(s(X0),s(s(n0)),cons(s(s(s(s(s(s(n0)))))),X1))
| ~ sum(s(s(s(s(n0)))),s(s(n0)),s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(s(n0)))))),s(s(n0)),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(instantiation,[status(thm)],[c_153262]) ).
tcf(c_166432,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( same(X4,X0)
| same(X3,X0)
| diagonal_attack(X0,s(s(s(n0))),X2)
| ~ sum(X4,s(s(n0)),s(s(X1)))
| ~ sum(s(s(X1)),s(s(n0)),X3)
| ~ sum(s(s(n0)),s(n0),s(s(s(n0))))
| ~ diagonal_attack(X0,s(s(n0)),cons(s(s(X1)),X2)) ),
inference(instantiation,[status(thm)],[c_148706]) ).
tcf(c_166621,plain,
! [X0: $i,X1: $i] :
( same(s(s(s(s(n0)))),s(X0))
| diagonal_attack(s(X0),s(s(s(n0))),X1)
| same(s(s(s(s(s(s(s(s(n0)))))))),s(X0))
| ~ sum(s(s(n0)),s(n0),s(s(s(n0))))
| ~ diagonal_attack(s(X0),s(s(n0)),cons(s(s(s(s(s(s(n0)))))),X1))
| ~ sum(s(s(s(s(n0)))),s(s(n0)),s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(s(n0)))))),s(s(n0)),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(instantiation,[status(thm)],[c_164068]) ).
tcf(c_170673,plain,
( same(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(s(n0)))))))
| ~ same(s(s(s(s(s(s(s(s(s(n0))))))))),s(s(s(s(s(s(s(n0)))))))) ),
inference(instantiation,[status(thm)],[c_144580]) ).
tcf(c_171022,plain,
! [X0: $i] :
( diagonal_attack(s(X0),s(s(s(n0))),empty_list)
| same(s(s(s(s(n0)))),s(X0))
| same(s(s(s(s(s(s(s(s(n0)))))))),s(X0))
| ~ sum(s(s(n0)),s(n0),s(s(s(n0))))
| ~ diagonal_attack(s(X0),s(s(n0)),cons(s(s(s(s(s(s(n0)))))),empty_list))
| ~ sum(s(s(s(s(n0)))),s(s(n0)),s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(s(n0)))))),s(s(n0)),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(instantiation,[status(thm)],[c_166621]) ).
tcf(c_176669,plain,
! [X0: $i] :
( diagonal_attack(s(s(s(X0))),s(s(s(n0))),empty_list)
| same(s(s(s(s(n0)))),s(s(s(X0))))
| same(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(X0))))
| ~ sum(s(s(n0)),s(n0),s(s(s(n0))))
| ~ sum(s(s(s(s(n0)))),s(s(n0)),s(s(s(s(s(s(n0)))))))
| ~ diagonal_attack(s(s(s(X0))),s(s(n0)),cons(s(s(s(s(s(s(n0)))))),empty_list))
| ~ sum(s(s(s(s(s(s(n0)))))),s(s(n0)),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(instantiation,[status(thm)],[c_171022]) ).
tcf(c_189442,plain,
! [X0: $i] :
( diagonal_attack(s(s(s(s(s(X0))))),s(s(s(n0))),empty_list)
| same(s(s(s(s(n0)))),s(s(s(s(s(X0))))))
| same(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(X0))))))
| ~ sum(s(s(n0)),s(n0),s(s(s(n0))))
| ~ sum(s(s(s(s(n0)))),s(s(n0)),s(s(s(s(s(s(n0)))))))
| ~ diagonal_attack(s(s(s(s(s(X0))))),s(s(n0)),cons(s(s(s(s(s(s(n0)))))),empty_list))
| ~ sum(s(s(s(s(s(s(n0)))))),s(s(n0)),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(instantiation,[status(thm)],[c_176669]) ).
tcf(c_189444,plain,
( diagonal_attack(s(s(s(s(s(n0))))),s(s(s(n0))),empty_list)
| same(s(s(s(s(n0)))),s(s(s(s(s(n0))))))
| same(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(s(n0))))))
| ~ sum(s(s(n0)),s(n0),s(s(s(n0))))
| ~ sum(s(s(s(s(n0)))),s(s(n0)),s(s(s(s(s(s(n0)))))))
| ~ diagonal_attack(s(s(s(s(s(n0))))),s(s(n0)),cons(s(s(s(s(s(s(n0)))))),empty_list))
| ~ sum(s(s(s(s(s(s(n0)))))),s(s(n0)),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(instantiation,[status(thm)],[c_189442]) ).
tcf(c_206209,plain,
( same(s(s(n0)),s(s(s(s(s(s(n0)))))))
| ~ same(s(s(s(n0))),s(s(s(s(s(s(s(n0)))))))) ),
inference(instantiation,[status(thm)],[c_144323]) ).
tcf(c_206306,plain,
( same(s(s(s(n0))),s(s(s(s(s(s(n0)))))))
| ~ same(s(s(s(s(n0)))),s(s(s(s(s(s(s(n0)))))))) ),
inference(instantiation,[status(thm)],[c_144342]) ).
tcf(c_209610,plain,
! [X0: $i] :
( same(s(s(s(s(n0)))),s(s(s(s(s(X0))))))
| ~ same(s(s(s(s(s(n0))))),s(s(s(s(s(s(X0))))))) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_210361,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( same(X5,X0)
| same(X4,X0)
| diagonal_attack(X0,X3,X2)
| ~ sum(X5,s(s(s(n0))),X1)
| ~ sum(X1,s(s(s(n0))),X4)
| ~ sum(s(s(s(n0))),s(n0),X3)
| ~ diagonal_attack(X0,s(s(s(n0))),cons(X1,X2)) ),
inference(instantiation,[status(thm)],[c_78]) ).
tcf(c_210756,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( same(X4,X0)
| same(X3,X0)
| diagonal_attack(X0,X5,X2)
| ~ sum(s(s(s(n0))),s(n0),X5)
| ~ sum(X4,s(s(s(n0))),s(X1))
| ~ sum(s(X1),s(s(s(n0))),X3)
| ~ diagonal_attack(X0,s(s(s(n0))),cons(s(X1),X2)) ),
inference(instantiation,[status(thm)],[c_210361]) ).
tcf(c_211121,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( same(X4,X0)
| same(X3,X0)
| diagonal_attack(X0,X5,X2)
| ~ sum(s(s(s(n0))),s(n0),X5)
| ~ sum(X4,s(s(s(n0))),s(s(s(X1))))
| ~ sum(s(s(s(X1))),s(s(s(n0))),X3)
| ~ diagonal_attack(X0,s(s(s(n0))),cons(s(s(s(X1))),X2)) ),
inference(instantiation,[status(thm)],[c_210756]) ).
tcf(c_211583,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( same(X4,X0)
| same(X3,X0)
| diagonal_attack(X0,s(s(s(s(n0)))),X2)
| ~ sum(X4,s(s(s(n0))),s(s(s(X1))))
| ~ sum(s(s(s(X1))),s(s(s(n0))),X3)
| ~ sum(s(s(s(n0))),s(n0),s(s(s(s(n0)))))
| ~ diagonal_attack(X0,s(s(s(n0))),cons(s(s(s(X1))),X2)) ),
inference(instantiation,[status(thm)],[c_211121]) ).
tcf(c_223595,plain,
( same(s(s(s(s(n0)))),s(s(s(s(s(s(s(n0))))))))
| ~ same(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(instantiation,[status(thm)],[c_209610]) ).
tcf(c_297916,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( same(X5,X0)
| same(X4,X0)
| diagonal_attack(X0,X3,X2)
| ~ sum(X5,s(n0),X1)
| ~ sum(X1,s(n0),X4)
| ~ sum(s(n0),s(n0),X3)
| ~ diagonal_attack(X0,s(n0),cons(X1,X2)) ),
inference(instantiation,[status(thm)],[c_78]) ).
tcf(c_297958,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( same(X4,X0)
| same(X3,X0)
| diagonal_attack(X0,s(s(n0)),X2)
| ~ sum(X4,s(n0),X1)
| ~ sum(X1,s(n0),X3)
| ~ diagonal_attack(X0,s(n0),cons(X1,X2))
| ~ sum(s(n0),s(n0),s(s(n0))) ),
inference(instantiation,[status(thm)],[c_297916]) ).
tcf(c_298032,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( same(X4,X0)
| same(X3,X0)
| diagonal_attack(X0,s(s(n0)),X2)
| ~ sum(X4,s(n0),X1)
| ~ sum(X1,s(n0),X3)
| ~ diagonal_attack(X0,s(n0),cons(X1,X2)) ),
inference(global_subsumption_just,[status(thm)],[c_297958,c_366,c_367,c_144356]) ).
tcf(c_298169,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( same(X5,X0)
| same(X4,X0)
| diagonal_attack(X0,s(s(n0)),cons(X2,X3))
| ~ sum(X5,s(n0),X1)
| ~ sum(X1,s(n0),X4)
| ~ diagonal_attack(X0,s(n0),cons(X1,cons(X2,X3))) ),
inference(instantiation,[status(thm)],[c_298032]) ).
tcf(c_298241,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( same(X5,X0)
| same(X4,X0)
| diagonal_attack(X0,X3,X2)
| ~ sum(X5,s(s(n0)),X1)
| ~ sum(X1,s(s(n0)),X4)
| ~ sum(s(s(n0)),s(n0),X3)
| ~ diagonal_attack(X0,s(s(n0)),cons(X1,X2)) ),
inference(instantiation,[status(thm)],[c_78]) ).
tcf(c_298335,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( same(X4,X0)
| same(X3,X0)
| diagonal_attack(X0,X5,X2)
| ~ sum(s(s(n0)),s(n0),X5)
| ~ sum(X4,s(s(n0)),s(X1))
| ~ sum(s(X1),s(s(n0)),X3)
| ~ diagonal_attack(X0,s(s(n0)),cons(s(X1),X2)) ),
inference(instantiation,[status(thm)],[c_298241]) ).
tcf(c_298562,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( same(X4,X0)
| same(X3,X0)
| diagonal_attack(X0,X5,X2)
| ~ sum(s(s(n0)),s(n0),X5)
| ~ sum(X4,s(s(n0)),s(s(X1)))
| ~ sum(s(s(X1)),s(s(n0)),X3)
| ~ diagonal_attack(X0,s(s(n0)),cons(s(s(X1)),X2)) ),
inference(instantiation,[status(thm)],[c_298335]) ).
tcf(c_299032,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( same(X4,X0)
| same(X3,X0)
| diagonal_attack(X0,s(s(s(n0))),X2)
| ~ sum(X4,s(s(n0)),s(s(X1)))
| ~ sum(s(s(X1)),s(s(n0)),X3)
| ~ sum(s(s(n0)),s(n0),s(s(s(n0))))
| ~ diagonal_attack(X0,s(s(n0)),cons(s(s(X1)),X2)) ),
inference(instantiation,[status(thm)],[c_298562]) ).
tcf(c_299387,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( same(X4,X0)
| same(X3,X0)
| diagonal_attack(X0,s(s(s(n0))),X2)
| ~ sum(X4,s(s(n0)),s(s(X1)))
| ~ sum(s(s(X1)),s(s(n0)),X3)
| ~ diagonal_attack(X0,s(s(n0)),cons(s(s(X1)),X2)) ),
inference(global_subsumption_just,[status(thm)],[c_299032,c_383,c_384,c_166432]) ).
tcf(c_299390,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( same(X5,X0)
| same(X4,X0)
| diagonal_attack(X0,s(s(s(n0))),cons(X2,X3))
| ~ sum(X5,s(s(n0)),s(s(X1)))
| ~ sum(s(s(X1)),s(s(n0)),X4)
| ~ diagonal_attack(X0,s(s(n0)),cons(s(s(X1)),cons(X2,X3))) ),
inference(instantiation,[status(thm)],[c_299387]) ).
tcf(c_299391,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( same(X5,X0)
| same(X4,X0)
| diagonal_attack(X0,X3,X2)
| ~ sum(X5,s(s(s(n0))),X1)
| ~ sum(X1,s(s(s(n0))),X4)
| ~ sum(s(s(s(n0))),s(n0),X3)
| ~ diagonal_attack(X0,s(s(s(n0))),cons(X1,X2)) ),
inference(instantiation,[status(thm)],[c_78]) ).
tcf(c_299857,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( same(X4,X0)
| same(X3,X0)
| diagonal_attack(X0,s(s(n0)),cons(s(s(X2)),empty_list))
| ~ sum(X4,s(n0),X1)
| ~ sum(X1,s(n0),X3)
| ~ diagonal_attack(X0,s(n0),cons(X1,cons(s(s(X2)),empty_list))) ),
inference(instantiation,[status(thm)],[c_298169]) ).
tcf(c_299953,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( same(X6,X0)
| same(X5,X0)
| diagonal_attack(X0,s(s(n0)),cons(s(s(X2)),cons(X3,X4)))
| ~ sum(X6,s(n0),X1)
| ~ sum(X1,s(n0),X5)
| ~ diagonal_attack(X0,s(n0),cons(X1,cons(s(s(X2)),cons(X3,X4)))) ),
inference(instantiation,[status(thm)],[c_298169]) ).
tcf(c_299955,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( same(X4,X0)
| same(X3,X0)
| diagonal_attack(X0,X5,X2)
| ~ sum(s(s(s(n0))),s(n0),X5)
| ~ sum(X4,s(s(s(n0))),s(X1))
| ~ sum(s(X1),s(s(s(n0))),X3)
| ~ diagonal_attack(X0,s(s(s(n0))),cons(s(X1),X2)) ),
inference(instantiation,[status(thm)],[c_299391]) ).
tcf(c_300372,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( same(X4,X0)
| same(X3,X0)
| diagonal_attack(X0,s(s(n0)),cons(s(s(X2)),empty_list))
| ~ sum(X4,s(n0),s(X1))
| ~ sum(s(X1),s(n0),X3)
| ~ diagonal_attack(X0,s(n0),cons(s(X1),cons(s(s(X2)),empty_list))) ),
inference(instantiation,[status(thm)],[c_299857]) ).
tcf(c_300770,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( same(X4,X0)
| same(X3,X0)
| diagonal_attack(X0,X5,X2)
| ~ sum(s(s(s(n0))),s(n0),X5)
| ~ sum(X4,s(s(s(n0))),s(s(s(X1))))
| ~ sum(s(s(s(X1))),s(s(s(n0))),X3)
| ~ diagonal_attack(X0,s(s(s(n0))),cons(s(s(s(X1))),X2)) ),
inference(instantiation,[status(thm)],[c_299955]) ).
tcf(c_301278,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( same(X4,X0)
| same(X3,X0)
| diagonal_attack(X0,s(s(s(s(n0)))),X2)
| ~ sum(X4,s(s(s(n0))),s(s(s(X1))))
| ~ sum(s(s(s(X1))),s(s(s(n0))),X3)
| ~ sum(s(s(s(n0))),s(n0),s(s(s(s(n0)))))
| ~ diagonal_attack(X0,s(s(s(n0))),cons(s(s(s(X1))),X2)) ),
inference(instantiation,[status(thm)],[c_300770]) ).
tcf(c_301283,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( same(X4,X0)
| same(X3,X0)
| diagonal_attack(X0,s(s(n0)),cons(s(s(X2)),empty_list))
| ~ sum(X4,s(n0),s(s(X1)))
| ~ sum(s(s(X1)),s(n0),X3)
| ~ diagonal_attack(X0,s(n0),cons(s(s(X1)),cons(s(s(X2)),empty_list))) ),
inference(instantiation,[status(thm)],[c_300372]) ).
tcf(c_301287,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( same(X6,X0)
| same(X5,X0)
| diagonal_attack(X0,s(s(n0)),cons(s(s(X2)),cons(X3,X4)))
| ~ sum(X6,s(n0),s(s(X1)))
| ~ sum(s(s(X1)),s(n0),X5)
| ~ diagonal_attack(X0,s(n0),cons(s(s(X1)),cons(s(s(X2)),cons(X3,X4)))) ),
inference(instantiation,[status(thm)],[c_299953]) ).
tcf(c_301548,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( same(X4,X0)
| same(X3,X0)
| diagonal_attack(X0,s(s(s(s(n0)))),X2)
| ~ sum(X4,s(s(s(n0))),s(s(s(X1))))
| ~ sum(s(s(s(X1))),s(s(s(n0))),X3)
| ~ diagonal_attack(X0,s(s(s(n0))),cons(s(s(s(X1))),X2)) ),
inference(global_subsumption_just,[status(thm)],[c_301278,c_435,c_436,c_211583]) ).
tcf(c_301555,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( same(X4,X2)
| same(s(s(s(X1))),X2)
| diagonal_attack(X2,s(s(s(s(n0)))),X3)
| ~ sum(X4,s(s(s(n0))),s(s(s(X0))))
| ~ diagonal_attack(X2,s(s(s(n0))),cons(s(s(s(X0))),X3))
| ~ sum(s(s(s(X0))),s(s(s(n0))),s(s(s(X1)))) ),
inference(instantiation,[status(thm)],[c_301548]) ).
tcf(c_302044,plain,
! [X0: $i,X1: $i,X2: $i] :
( same(X2,X0)
| diagonal_attack(X0,s(s(s(s(n0)))),X1)
| same(s(s(s(s(s(s(s(s(s(n0))))))))),X0)
| ~ sum(X2,s(s(s(n0))),s(s(s(s(s(s(n0)))))))
| ~ diagonal_attack(X0,s(s(s(n0))),cons(s(s(s(s(s(s(n0)))))),X1))
| ~ sum(s(s(s(s(s(s(n0)))))),s(s(s(n0))),s(s(s(s(s(s(s(s(s(n0)))))))))) ),
inference(instantiation,[status(thm)],[c_301555]) ).
tcf(c_302370,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( same(X3,X0)
| same(X2,X0)
| diagonal_attack(X0,s(s(n0)),cons(s(s(s(s(s(s(n0)))))),empty_list))
| ~ sum(X3,s(n0),s(s(X1)))
| ~ sum(s(s(X1)),s(n0),X2)
| ~ diagonal_attack(X0,s(n0),cons(s(s(X1)),cons(s(s(s(s(s(s(n0)))))),empty_list))) ),
inference(instantiation,[status(thm)],[c_301283]) ).
tcf(c_303247,plain,
! [X0: $i,X1: $i,X2: $i] :
( same(X2,X0)
| diagonal_attack(X0,s(s(s(s(n0)))),X1)
| same(s(s(s(s(s(s(s(s(s(n0))))))))),X0)
| ~ sum(X2,s(s(s(n0))),s(s(s(s(s(s(n0)))))))
| ~ diagonal_attack(X0,s(s(s(n0))),cons(s(s(s(s(s(s(n0)))))),X1)) ),
inference(global_subsumption_just,[status(thm)],[c_302044,c_943,c_944,c_3065,c_3883,c_302044]) ).
tcf(c_303424,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( same(X3,s(s(X0)))
| same(X2,s(s(X0)))
| diagonal_attack(s(s(X0)),s(s(n0)),cons(s(s(s(s(s(s(n0)))))),empty_list))
| ~ sum(X3,s(n0),s(s(X1)))
| ~ sum(s(s(X1)),s(n0),X2)
| ~ diagonal_attack(s(s(X0)),s(n0),cons(s(s(X1)),cons(s(s(s(s(s(s(n0)))))),empty_list))) ),
inference(instantiation,[status(thm)],[c_302370]) ).
tcf(c_303428,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( same(X6,s(s(X0)))
| same(X5,s(s(X0)))
| diagonal_attack(s(s(X0)),s(s(n0)),cons(s(s(X2)),cons(X3,X4)))
| ~ sum(X6,s(n0),s(s(X1)))
| ~ sum(s(s(X1)),s(n0),X5)
| ~ diagonal_attack(s(s(X0)),s(n0),cons(s(s(X1)),cons(s(s(X2)),cons(X3,X4)))) ),
inference(instantiation,[status(thm)],[c_301287]) ).
tcf(c_303700,plain,
! [X0: $i,X1: $i] :
( same(s(s(s(n0))),X0)
| diagonal_attack(X0,s(s(s(s(n0)))),X1)
| same(s(s(s(s(s(s(s(s(s(n0))))))))),X0)
| ~ diagonal_attack(X0,s(s(s(n0))),cons(s(s(s(s(s(s(n0)))))),X1))
| ~ sum(s(s(s(n0))),s(s(s(n0))),s(s(s(s(s(s(n0))))))) ),
inference(instantiation,[status(thm)],[c_303247]) ).
tcf(c_304523,plain,
! [X0: $i,X1: $i] :
( same(X1,s(s(X0)))
| same(s(s(s(s(s(s(s(s(s(n0))))))))),s(s(X0)))
| diagonal_attack(s(s(X0)),s(s(n0)),cons(s(s(s(s(s(s(n0)))))),empty_list))
| ~ sum(X1,s(n0),s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(s(s(s(s(n0)))))))),s(n0),s(s(s(s(s(s(s(s(s(n0))))))))))
| ~ diagonal_attack(s(s(X0)),s(n0),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list))) ),
inference(instantiation,[status(thm)],[c_303424]) ).
tcf(c_305551,plain,
! [X0: $i,X1: $i] :
( same(s(s(s(n0))),X0)
| diagonal_attack(X0,s(s(s(s(n0)))),X1)
| same(s(s(s(s(s(s(s(s(s(n0))))))))),X0)
| ~ diagonal_attack(X0,s(s(s(n0))),cons(s(s(s(s(s(s(n0)))))),X1)) ),
inference(global_subsumption_just,[status(thm)],[c_303700,c_435,c_436,c_3806,c_5331,c_303700]) ).
tcf(c_305759,plain,
! [X0: $i,X1: $i] :
( same(X1,s(s(X0)))
| same(s(s(s(s(s(s(s(s(s(n0))))))))),s(s(X0)))
| diagonal_attack(s(s(X0)),s(s(n0)),cons(s(s(s(s(s(s(n0)))))),empty_list))
| ~ sum(X1,s(n0),s(s(s(s(s(s(s(s(n0)))))))))
| ~ diagonal_attack(s(s(X0)),s(n0),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list))) ),
inference(global_subsumption_just,[status(thm)],[c_304523,c_1233,c_1546,c_304523]) ).
tcf(c_305766,plain,
! [X0: $i] :
( same(s(s(s(s(s(s(s(n0))))))),s(s(X0)))
| same(s(s(s(s(s(s(s(s(s(n0))))))))),s(s(X0)))
| diagonal_attack(s(s(X0)),s(s(n0)),cons(s(s(s(s(s(s(n0)))))),empty_list))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(n0),s(s(s(s(s(s(s(s(n0)))))))))
| ~ diagonal_attack(s(s(X0)),s(n0),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list))) ),
inference(instantiation,[status(thm)],[c_305759]) ).
tcf(c_308467,plain,
! [X0: $i] :
( same(s(s(s(s(s(s(s(n0))))))),s(s(X0)))
| same(s(s(s(s(s(s(s(s(s(n0))))))))),s(s(X0)))
| diagonal_attack(s(s(X0)),s(s(n0)),cons(s(s(s(s(s(s(n0)))))),empty_list))
| ~ diagonal_attack(s(s(X0)),s(n0),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list))) ),
inference(global_subsumption_just,[status(thm)],[c_305766,c_1186,c_1492,c_305766]) ).
tcf(c_308476,plain,
( same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(n0))))))
| same(s(s(s(s(s(s(s(s(s(n0))))))))),s(s(s(s(s(n0))))))
| diagonal_attack(s(s(s(s(s(n0))))),s(s(n0)),cons(s(s(s(s(s(s(n0)))))),empty_list))
| ~ diagonal_attack(s(s(s(s(s(n0))))),s(n0),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list))) ),
inference(instantiation,[status(thm)],[c_308467]) ).
tcf(c_309841,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( same(X4,s(s(X0)))
| same(X3,s(s(X0)))
| diagonal_attack(s(s(X0)),s(s(n0)),cons(s(s(X2)),cons(s(s(s(s(s(s(n0)))))),empty_list)))
| ~ sum(X4,s(n0),s(s(X1)))
| ~ sum(s(s(X1)),s(n0),X3)
| ~ diagonal_attack(s(s(X0)),s(n0),cons(s(s(X1)),cons(s(s(X2)),cons(s(s(s(s(s(s(n0)))))),empty_list)))) ),
inference(instantiation,[status(thm)],[c_303428]) ).
tcf(c_313829,plain,
! [X0: $i,X1: $i,X2: $i] :
( same(X2,s(s(X0)))
| same(s(s(s(s(s(s(n0)))))),s(s(X0)))
| diagonal_attack(s(s(X0)),s(s(n0)),cons(s(s(X1)),cons(s(s(s(s(s(s(n0)))))),empty_list)))
| ~ sum(X2,s(n0),s(s(s(s(s(n0))))))
| ~ sum(s(s(s(s(s(n0))))),s(n0),s(s(s(s(s(s(n0)))))))
| ~ diagonal_attack(s(s(X0)),s(n0),cons(s(s(s(s(s(n0))))),cons(s(s(X1)),cons(s(s(s(s(s(s(n0)))))),empty_list)))) ),
inference(instantiation,[status(thm)],[c_309841]) ).
tcf(c_314694,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( same(X4,X0)
| same(s(s(s(s(X1)))),X0)
| diagonal_attack(X0,s(s(s(n0))),cons(X2,X3))
| ~ sum(X4,s(s(n0)),s(s(X1)))
| ~ sum(s(s(X1)),s(s(n0)),s(s(s(s(X1)))))
| ~ diagonal_attack(X0,s(s(n0)),cons(s(s(X1)),cons(X2,X3))) ),
inference(instantiation,[status(thm)],[c_299390]) ).
tcf(c_315416,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( same(s(s(s(s(X1)))),s(s(s(s(s(s(s(X0))))))))
| same(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(X0))))))))
| diagonal_attack(s(s(s(s(s(s(s(X0))))))),s(s(s(n0))),cons(X2,X3))
| ~ sum(s(s(X1)),s(s(n0)),s(s(s(s(X1)))))
| ~ sum(s(s(s(s(s(s(n0)))))),s(s(n0)),s(s(X1)))
| ~ diagonal_attack(s(s(s(s(s(s(s(X0))))))),s(s(n0)),cons(s(s(X1)),cons(X2,X3))) ),
inference(instantiation,[status(thm)],[c_314694]) ).
tcf(c_319358,plain,
! [X0: $i,X1: $i,X2: $i] :
( same(X2,s(s(X0)))
| same(s(s(s(s(s(s(n0)))))),s(s(X0)))
| diagonal_attack(s(s(X0)),s(s(n0)),cons(s(s(X1)),cons(s(s(s(s(s(s(n0)))))),empty_list)))
| ~ sum(X2,s(n0),s(s(s(s(s(n0))))))
| ~ diagonal_attack(s(s(X0)),s(n0),cons(s(s(s(s(s(n0))))),cons(s(s(X1)),cons(s(s(s(s(s(s(n0)))))),empty_list)))) ),
inference(global_subsumption_just,[status(thm)],[c_313829,c_755,c_756,c_313829]) ).
tcf(c_319363,plain,
! [X0: $i,X1: $i] :
( same(s(s(s(s(n0)))),s(s(X0)))
| same(s(s(s(s(s(s(n0)))))),s(s(X0)))
| diagonal_attack(s(s(X0)),s(s(n0)),cons(s(s(X1)),cons(s(s(s(s(s(s(n0)))))),empty_list)))
| ~ sum(s(s(s(s(n0)))),s(n0),s(s(s(s(s(n0))))))
| ~ diagonal_attack(s(s(X0)),s(n0),cons(s(s(s(s(s(n0))))),cons(s(s(X1)),cons(s(s(s(s(s(s(n0)))))),empty_list)))) ),
inference(instantiation,[status(thm)],[c_319358]) ).
tcf(c_324849,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( same(s(s(s(s(X1)))),s(s(s(s(s(s(s(X0))))))))
| ~ diagonal_attack(s(s(s(s(s(s(s(X0))))))),s(s(n0)),cons(s(s(X1)),cons(X2,X3)))
| ~ sum(s(s(s(s(s(s(n0)))))),s(s(n0)),s(s(X1)))
| ~ sum(s(s(X1)),s(s(n0)),s(s(s(s(X1)))))
| diagonal_attack(s(s(s(s(s(s(s(X0))))))),s(s(s(n0))),cons(X2,X3)) ),
inference(global_subsumption_just,[status(thm)],[c_315416,c_83,c_21973,c_70037,c_70068,c_70117,c_70196,c_70373,c_315416]) ).
tcf(c_324850,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( same(s(s(s(s(X1)))),s(s(s(s(s(s(s(X0))))))))
| diagonal_attack(s(s(s(s(s(s(s(X0))))))),s(s(s(n0))),cons(X2,X3))
| ~ sum(s(s(X1)),s(s(n0)),s(s(s(s(X1)))))
| ~ sum(s(s(s(s(s(s(n0)))))),s(s(n0)),s(s(X1)))
| ~ diagonal_attack(s(s(s(s(s(s(s(X0))))))),s(s(n0)),cons(s(s(X1)),cons(X2,X3))) ),
inference(renaming,[status(thm)],[c_324849]) ).
tcf(c_324853,plain,
! [X0: $i,X1: $i,X2: $i] :
( diagonal_attack(s(s(s(s(s(s(s(X0))))))),s(s(s(n0))),cons(X1,X2))
| same(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(X0))))))))
| ~ sum(s(s(s(s(s(s(n0)))))),s(s(n0)),s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(s(s(s(s(n0)))))))),s(s(n0)),s(s(s(s(s(s(s(s(s(s(n0)))))))))))
| ~ diagonal_attack(s(s(s(s(s(s(s(X0))))))),s(s(n0)),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(X1,X2))) ),
inference(instantiation,[status(thm)],[c_324850]) ).
tcf(c_328206,plain,
! [X0: $i,X1: $i] :
( same(s(s(s(s(n0)))),s(s(X0)))
| same(s(s(s(s(s(s(n0)))))),s(s(X0)))
| diagonal_attack(s(s(X0)),s(s(n0)),cons(s(s(X1)),cons(s(s(s(s(s(s(n0)))))),empty_list)))
| ~ diagonal_attack(s(s(X0)),s(n0),cons(s(s(s(s(s(n0))))),cons(s(s(X1)),cons(s(s(s(s(s(s(n0)))))),empty_list)))) ),
inference(global_subsumption_just,[status(thm)],[c_319363,c_338,c_339,c_319363]) ).
tcf(c_331436,plain,
( same(s(s(s(n0))),s(s(s(s(s(s(s(n0))))))))
| diagonal_attack(s(s(s(s(s(s(s(n0))))))),s(s(s(s(n0)))),empty_list)
| same(s(s(s(s(s(s(s(s(s(n0))))))))),s(s(s(s(s(s(s(n0))))))))
| ~ diagonal_attack(s(s(s(s(s(s(s(n0))))))),s(s(s(n0))),cons(s(s(s(s(s(s(n0)))))),empty_list)) ),
inference(instantiation,[status(thm)],[c_305551]) ).
tcf(c_338550,plain,
( ~ diagonal_attack(s(s(s(s(s(s(s(n0))))))),s(s(s(n0))),cons(s(s(s(s(s(s(n0)))))),empty_list))
| diagonal_attack(s(s(s(s(s(s(s(n0))))))),s(s(s(s(n0)))),empty_list) ),
inference(global_subsumption_just,[status(thm)],[c_331436,c_9752,c_21231,c_78033,c_82422,c_85464,c_94643,c_98972,c_121551,c_134701,c_138952,c_170673,c_206209,c_331436]) ).
tcf(c_338551,plain,
( diagonal_attack(s(s(s(s(s(s(s(n0))))))),s(s(s(s(n0)))),empty_list)
| ~ diagonal_attack(s(s(s(s(s(s(s(n0))))))),s(s(s(n0))),cons(s(s(s(s(s(s(n0)))))),empty_list)) ),
inference(renaming,[status(thm)],[c_338550]) ).
tcf(c_340209,plain,
! [X0: $i,X1: $i,X2: $i] :
( diagonal_attack(s(s(s(s(s(s(s(X0))))))),s(s(s(n0))),cons(X1,X2))
| same(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(X0))))))))
| ~ diagonal_attack(s(s(s(s(s(s(s(X0))))))),s(s(n0)),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(X1,X2))) ),
inference(global_subsumption_just,[status(thm)],[c_324853,c_943,c_944,c_1233,c_1546,c_3065,c_10396,c_324853]) ).
tcf(c_340228,plain,
! [X0: $i] :
( same(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(X0))))))))
| diagonal_attack(s(s(s(s(s(s(s(X0))))))),s(s(s(n0))),cons(s(s(s(s(s(s(n0)))))),empty_list))
| ~ diagonal_attack(s(s(s(s(s(s(s(X0))))))),s(s(n0)),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list))) ),
inference(instantiation,[status(thm)],[c_340209]) ).
tcf(c_340233,plain,
! [X0: $i] :
( same(s(s(s(s(n0)))),s(s(s(s(s(s(s(X0))))))))
| same(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(X0))))))))
| diagonal_attack(s(s(s(s(s(s(s(X0))))))),s(s(n0)),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list)))
| ~ diagonal_attack(s(s(s(s(s(s(s(X0))))))),s(n0),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list)))) ),
inference(instantiation,[status(thm)],[c_328206]) ).
tcf(c_340239,plain,
( same(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(n0))))))))
| diagonal_attack(s(s(s(s(s(s(s(n0))))))),s(s(s(n0))),cons(s(s(s(s(s(s(n0)))))),empty_list))
| ~ diagonal_attack(s(s(s(s(s(s(s(n0))))))),s(s(n0)),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list))) ),
inference(instantiation,[status(thm)],[c_340228]) ).
tcf(c_340245,plain,
( same(s(s(s(s(n0)))),s(s(s(s(s(s(s(n0))))))))
| same(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(n0))))))))
| diagonal_attack(s(s(s(s(s(s(s(n0))))))),s(s(n0)),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list)))
| ~ diagonal_attack(s(s(s(s(s(s(s(n0))))))),s(n0),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list)))) ),
inference(instantiation,[status(thm)],[c_340233]) ).
tcf(c_347244,plain,
! [X0: $i] : ~ diagonal_attack(s(X0),s(s(s(s(n0)))),empty_list),
inference(instantiation,[status(thm)],[c_74]) ).
tcf(c_354931,plain,
~ diagonal_attack(s(s(s(s(s(s(s(n0))))))),s(s(s(s(n0)))),empty_list),
inference(instantiation,[status(thm)],[c_347244]) ).
tcf(c_380598,plain,
! [X0: $i] : less(s(n0),s(s(X0))),
inference(resolution,[status(thm)],[c_76,c_77]) ).
tcf(c_380605,plain,
! [X0: $i] : less(s(s(n0)),s(s(s(X0)))),
inference(resolution,[status(thm)],[c_380598,c_76]) ).
tcf(c_380738,plain,
! [X0: $i] : less(s(s(s(n0))),s(s(s(s(X0))))),
inference(resolution,[status(thm)],[c_380605,c_76]) ).
tcf(c_380789,plain,
! [X0: $i] : less(s(s(s(s(n0)))),s(s(s(s(s(X0)))))),
inference(resolution,[status(thm)],[c_380738,c_76]) ).
tcf(c_380824,plain,
! [X0: $i] : sum(X0,s(n0),s(X0)),
inference(resolution,[status(thm)],[c_71,c_72]) ).
tcf(c_380873,plain,
! [X0: $i] : sum(X0,s(s(n0)),s(s(X0))),
inference(resolution,[status(thm)],[c_380824,c_71]) ).
tcf(c_380938,plain,
! [X0: $i,X1: $i,X2: $i] : select(X0,cons(X1,cons(X0,X2)),cons(X1,X2)),
inference(resolution,[status(thm)],[c_80,c_81]) ).
tcf(c_380963,plain,
! [X0: $i,X1: $i,X2: $i] :
( range(X0,X1,cons(X0,X2))
| ~ less(X0,X1)
| ~ range(s(X0),X1,X2) ),
inference(resolution,[status(thm)],[c_70,c_380824]) ).
tcf(c_381025,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : select(X0,cons(X1,cons(X2,cons(X0,X3))),cons(X1,cons(X2,X3))),
inference(resolution,[status(thm)],[c_380938,c_80]) ).
tcf(c_381072,plain,
! [X0: $i,X1: $i,X2: $i] :
( diagonal_attack(X0,s(n0),X2)
| do_queens(X1,X2,cons(X0,X2))
| ~ select(X0,X1,empty_list) ),
inference(resolution,[status(thm)],[c_181,c_73]) ).
tcf(c_381118,plain,
! [X0: $i] : sum(X0,s(s(s(n0))),s(s(s(X0)))),
inference(resolution,[status(thm)],[c_380873,c_71]) ).
tcf(c_381172,plain,
! [X0: $i] : sum(X0,s(s(s(s(n0)))),s(s(s(s(X0))))),
inference(resolution,[status(thm)],[c_381118,c_71]) ).
tcf(c_381216,plain,
! [X0: $i] : less(s(s(s(s(s(n0))))),s(s(s(s(s(s(X0))))))),
inference(resolution,[status(thm)],[c_380789,c_76]) ).
tcf(c_381361,plain,
! [X0: $i] : less(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(X0)))))))),
inference(resolution,[status(thm)],[c_381216,c_76]) ).
tcf(c_381453,plain,
! [X0: $i] :
( range(X0,s(X0),cons(X0,cons(s(X0),empty_list)))
| ~ less(X0,s(X0)) ),
inference(resolution,[status(thm)],[c_380963,c_69]) ).
tcf(c_381833,plain,
! [X0: $i,X1: $i] :
( diagonal_attack(X0,s(n0),X1)
| do_queens(cons(X0,empty_list),X1,cons(X0,X1)) ),
inference(resolution,[status(thm)],[c_381072,c_81]) ).
tcf(c_381897,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( diagonal_attack(X0,s(n0),X3)
| diagonal_attack(X2,s(n0),cons(X0,X3))
| do_queens(X1,X3,cons(X2,cons(X0,X3)))
| ~ select(X0,X1,cons(X2,empty_list)) ),
inference(resolution,[status(thm)],[c_381833,c_181]) ).
tcf(c_381953,plain,
! [X0: $i] : less(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(s(X0))))))))),
inference(resolution,[status(thm)],[c_381361,c_76]) ).
tcf(c_382101,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ do_queens(X1,empty_list,X2)
| ~ sum(s(s(s(s(n0)))),s(n0),X0)
| ~ range(X0,s(s(s(s(s(s(s(s(n0)))))))),X1) ),
inference(resolution,[status(thm)],[c_199,c_381172]) ).
tcf(c_382331,plain,
range(s(s(s(s(s(s(s(n0))))))),s(s(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))),
inference(resolution,[status(thm)],[c_381953,c_381453]) ).
tcf(c_383390,plain,
! [X0: $i,X1: $i,X2: $i] :
( diagonal_attack(X0,s(n0),X2)
| diagonal_attack(X1,s(n0),cons(X0,X2))
| do_queens(cons(X0,cons(X1,empty_list)),X2,cons(X1,cons(X0,X2))) ),
inference(resolution,[status(thm)],[c_381897,c_81]) ).
tcf(c_383488,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( diagonal_attack(X0,s(n0),X4)
| diagonal_attack(X2,s(n0),cons(X0,X4))
| diagonal_attack(X3,s(n0),cons(X2,cons(X0,X4)))
| do_queens(X1,X4,cons(X3,cons(X2,cons(X0,X4))))
| ~ select(X0,X1,cons(X2,cons(X3,empty_list))) ),
inference(resolution,[status(thm)],[c_383390,c_181]) ).
tcf(c_384895,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( diagonal_attack(X2,s(n0),X3)
| diagonal_attack(X0,s(n0),cons(X2,X3))
| diagonal_attack(X1,s(n0),cons(X0,cons(X2,X3)))
| do_queens(cons(X0,cons(X1,cons(X2,empty_list))),X3,cons(X1,cons(X0,cons(X2,X3)))) ),
inference(resolution,[status(thm)],[c_383488,c_381025]) ).
tcf(c_385596,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( diagonal_attack(X0,s(n0),X5)
| diagonal_attack(X4,s(n0),cons(X0,X5))
| diagonal_attack(X2,s(n0),cons(X4,cons(X0,X5)))
| diagonal_attack(X3,s(n0),cons(X2,cons(X4,cons(X0,X5))))
| do_queens(X1,X5,cons(X3,cons(X2,cons(X4,cons(X0,X5)))))
| ~ select(X0,X1,cons(X2,cons(X3,cons(X4,empty_list)))) ),
inference(resolution,[status(thm)],[c_384895,c_181]) ).
tcf(c_385669,plain,
( range(s(s(s(s(s(s(n0)))))),s(s(s(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))))
| ~ less(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(resolution,[status(thm)],[c_382331,c_380963]) ).
tcf(c_390381,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( diagonal_attack(X1,s(n0),X4)
| diagonal_attack(X3,s(n0),cons(X1,X4))
| diagonal_attack(X0,s(n0),cons(X3,cons(X1,X4)))
| diagonal_attack(X2,s(n0),cons(X0,cons(X3,cons(X1,X4))))
| do_queens(cons(X0,cons(X1,cons(X2,cons(X3,empty_list)))),X4,cons(X2,cons(X0,cons(X3,cons(X1,X4))))) ),
inference(resolution,[status(thm)],[c_385596,c_380938]) ).
tcf(c_396954,plain,
range(s(s(s(s(s(s(n0)))))),s(s(s(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)))),
inference(global_subsumption_just,[status(thm)],[c_385669,c_85,c_288,c_303,c_319,c_350,c_380,c_426,c_549,c_890,c_912,c_943,c_944,c_1118,c_1119,c_1186,c_1492,c_2347,c_2513,c_2514,c_2938,c_3017,c_3642]) ).
tcf(c_396959,plain,
( range(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(s(n0)))))))),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)))))
| ~ less(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(resolution,[status(thm)],[c_396954,c_380963]) ).
tcf(c_398950,plain,
range(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(s(n0)))))))),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))))),
inference(global_subsumption_just,[status(thm)],[c_396959,c_85,c_288,c_303,c_319,c_350,c_380,c_426,c_549,c_755,c_756,c_890,c_912,c_943,c_944,c_1118,c_1119,c_1186,c_1492,c_2333,c_2334,c_2347,c_2513,c_2514,c_2933,c_2938,c_3017,c_3638,c_3642,c_5220,c_5226,c_9383]) ).
tcf(c_398956,plain,
! [X0: $i] :
( ~ sum(s(s(s(s(n0)))),s(n0),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))))))),cons(s(s(s(s(s(s(s(s(n0)))))))),empty_list)))),empty_list,X0) ),
inference(resolution,[status(thm)],[c_398950,c_382101]) ).
tcf(c_399732,plain,
! [X0: $i] : ~ 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),
inference(global_subsumption_just,[status(thm)],[c_398956,c_85,c_288,c_303,c_319,c_338,c_339,c_350,c_380,c_426,c_434,c_541,c_549,c_707,c_755,c_756,c_890,c_912,c_943,c_944,c_1118,c_1119,c_1186,c_1492,c_2333,c_2334,c_2347,c_2513,c_2514,c_2933,c_2938,c_3017,c_3638,c_3642,c_5220,c_5226,c_9383,c_11694]) ).
tcf(c_399777,plain,
( diagonal_attack(s(s(s(s(s(s(n0)))))),s(n0),empty_list)
| diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(n0),cons(s(s(s(s(s(s(n0)))))),empty_list))
| diagonal_attack(s(s(s(s(s(n0))))),s(n0),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list)))
| diagonal_attack(s(s(s(s(s(s(s(n0))))))),s(n0),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list)))) ),
inference(resolution,[status(thm)],[c_399732,c_390381]) ).
tcf(c_399778,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_399777,c_354931,c_340245,c_340239,c_338551,c_308476,c_223595,c_206306,c_189444,c_151962,c_146684,c_137319,c_103060,c_102967,c_98978,c_98121,c_94643,c_94382,c_92268,c_91068,c_89687,c_86561,c_85464,c_85394,c_84758,c_84720,c_84132,c_82422,c_78408,c_78033,c_70811,c_70374,c_70197,c_70118,c_70069,c_70038,c_62006,c_30797,c_21974,c_21231,c_12304,c_10212,c_9752,c_9751,c_3065,c_944,c_943,c_756,c_755,c_434,c_384,c_383,c_367,c_366,c_339,c_338,c_89]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : PUZ034-1.004 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.05/0.30 % Computer : n012.cluster.edu
% 0.05/0.30 % Model : x86_64 x86_64
% 0.05/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.30 % Memory : 8046.5625MB
% 0.05/0.30 % OS : Linux 6.8.0-71-generic
% 0.05/0.30 % CPULimit : 300
% 0.05/0.30 % WCLimit : 300
% 0.05/0.30 % DateTime : Thu Sep 24 06:43:35 UTC 2026
% 0.05/0.30 % CPUTime :
% 0.05/0.30 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.05/0.33 Running first-order theorem proving
% 0.05/0.33 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.33
% 0.07/0.33 % ======== iProver multi-core TPTP/SMT =========
% 0.07/0.33
% 0.07/0.33 % Detected problem language: tptp
% 0.07/0.34 % Proving...
% 104.65/27.27 % SZS status Started for theBenchmark.p
% 104.65/27.27 % SZS status Unsatisfiable for theBenchmark.p
% 104.65/27.27
% 104.65/27.27 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 104.65/27.27
% 104.65/27.27 % ------ iProver source info
% 104.65/27.27
% 104.65/27.27 % git: date: 2026-07-19 20:42:38 +0200
% 104.65/27.27 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 104.65/27.27 % git: non_committed_changes: false
% 104.65/27.27
% 104.65/27.27 % ------ Parsing...% successful
% 104.65/27.27
% 104.65/27.27
% 104.65/27.27 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 104.65/27.27
% 104.65/27.27 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe:1:0s pe:2:0s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 104.65/27.27
% 104.65/27.27 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 104.65/27.27 % ------ Proving...
% 104.65/27.27 % ------ Problem Properties
% 104.65/27.27
% 104.65/27.27 %
% 104.65/27.27 % clauses 16
% 104.65/27.27 % conjectures 0
% 104.65/27.27 % EPR 3
% 104.65/27.27 % Horn 14
% 104.65/27.27 % unary 8
% 104.65/27.27 % binary 4
% 104.65/27.27 % lits 35
% 104.65/27.27 % lits eq 0
% 104.65/27.27 % fd_pure 0
% 104.65/27.27 % fd_pseudo 0
% 104.65/27.27 % fd_cond 0
% 104.65/27.27 % fd_pseudo_cond 0
% 104.65/27.27 % AC symbols 0
% 104.65/27.27
% 104.65/27.27 % ------ Schedule dynamic 5 is on
% 104.65/27.27
% 104.65/27.27 % ------ no conjectures: strip conj schedule
% 104.65/27.27
% 104.65/27.27 % ------ no equalities: superposition off
% 104.65/27.27
% 104.65/27.27 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" stripped conjectures Time Limit: 10.
% 104.65/27.27
% 104.65/27.27
% 104.65/27.27 % ------
% 104.65/27.27 % Current options:
% 104.65/27.27 % ------
% 104.65/27.27
% 104.65/27.27
% 104.65/27.27 %
% 104.65/27.27
% 104.65/27.27 % ------ Proving...
% 104.65/27.27 % Proof_search_loop: time out after: 8835 full_loop iterations
% 104.65/27.27
% 104.65/27.27 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" stripped conjectures Time Limit: 15.
% 104.65/27.27
% 104.65/27.27
% 104.65/27.27 % ------
% 104.65/27.27 % Current options:
% 104.65/27.27 % ------
% 104.65/27.27
% 104.65/27.27
% 104.65/27.27 %
% 104.65/27.27
% 104.65/27.27 % ------ Proving...
% 104.65/27.27 % Proof_search_loop: time out after: 18056 full_loop iterations
% 104.65/27.27
% 104.65/27.27 % ------ Option_1: Negative Selections stripped conjectures Time Limit: 35.
% 104.65/27.27
% 104.65/27.27
% 104.65/27.27 % ------
% 104.65/27.27 % Current options:
% 104.65/27.27 % ------
% 104.65/27.27
% 104.65/27.27
% 104.65/27.27 %
% 104.65/27.27
% 104.65/27.27 % ------ Proving...
% 104.65/27.27 %
% 104.65/27.27
% 104.65/27.27 % SZS status Unsatisfiable for theBenchmark.p
% 104.65/27.27
% 104.65/27.27 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 104.65/27.28
% 104.65/27.28
%------------------------------------------------------------------------------