%------------------------------------------------------------------------------
% File : hopCoP---0.1
% Problem : PUZ034-1.004 : TPTP v9.0.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Jul 25 01:24:30 PM UTC 2025
% Result : Unsatisfiable 13.20s 2.00s
% Output : CNFRefutation 13.20s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named place_queens)
% Comments :
%------------------------------------------------------------------------------
cnf(17,plain,
~ queens(s(s(s(s(n0)))),X0),
inference(cnf,[status(esa)],[place_queens]) ).
cnf(l0,plain,
~ queens(s(s(s(s(n0)))),cons(s(s(s(s(s(s(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)],[17]) ).
cnf(16,plain,
( ~ range(X0,X1,X2)
| ~ sum(X3,X3,X1)
| ~ sum(X3,s(n0),X0)
| ~ do_queens(X2,empty_list,X4)
| queens(X3,X4) ),
inference(cnf,[status(esa)],[set_up_queens]) ).
cnf(l1,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(n0)))),s(s(s(s(n0)))),s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(n0)))),s(n0),s(s(s(s(s(n0))))))
| ~ 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,cons(s(s(s(s(s(s(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)))))
| queens(s(s(s(s(n0)))),cons(s(s(s(s(s(s(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)],[16]) ).
cnf(5,plain,
( ~ sum(X0,X1,X2)
| sum(X0,s(X1),s(X2)) ),
inference(cnf,[status(esa)],[add]) ).
cnf(l7,plain,
( ~ sum(s(s(s(s(n0)))),n0,s(s(s(s(n0)))))
| sum(s(s(s(s(n0)))),s(n0),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(14,plain,
( ~ do_queens(X0,cons(X1,X2),X3)
| ~ select(X1,X4,X0)
| do_queens(X4,X2,X3)
| attack(X1,X2) ),
inference(cnf,[status(esa)],[place_a_queen1]) ).
cnf(l4,plain,
( ~ do_queens(cons(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))),cons(s(s(s(s(s(s(n0)))))),empty_list),cons(s(s(s(s(s(s(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)))))
| ~ select(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)))),cons(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))))
| 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,cons(s(s(s(s(s(s(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)))))
| attack(s(s(s(s(s(s(n0)))))),empty_list) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(4,plain,
sum(X0,n0,X0),
inference(cnf,[status(esa)],[add_0]) ).
cnf(l9,plain,
sum(s(s(s(s(n0)))),n0,s(s(s(s(n0))))),
inference(instantiation,[status(thm)],[4]) ).
cnf(7,plain,
( ~ select(X0,X1,X2)
| select(X0,cons(X3,X1),cons(X3,X2)) ),
inference(cnf,[status(esa)],[select2]) ).
cnf(l10,plain,
( ~ select(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))),cons(s(s(s(s(s(s(s(n0))))))),cons(s(s(s(s(s(s(s(s(n0)))))))),empty_list)))
| select(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)))),cons(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)],[7]) ).
cnf(6,plain,
select(X0,cons(X0,X1),X1),
inference(cnf,[status(esa)],[select1]) ).
cnf(l16,plain,
select(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))),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)],[6]) ).
cnf(11,plain,
( ~ attack(X0,X1)
| diagonal_attack(X0,s(n0),X1) ),
inference(cnf,[status(esa)],[attack]) ).
cnf(l8,plain,
( ~ attack(s(s(s(s(s(s(n0)))))),empty_list)
| diagonal_attack(s(s(s(s(s(s(n0)))))),s(n0),empty_list) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(0,plain,
( ~ range(X0,X1,X2)
| ~ less(X3,X1)
| ~ sum(X3,s(n0),X0)
| range(X3,X1,cons(X3,X2)) ),
inference(cnf,[status(esa)],[make_list_of_numbers1]) ).
cnf(l5,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(n0))))),s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(s(n0))))),s(n0),s(s(s(s(s(s(n0)))))))
| 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)],[0]) ).
cnf(3,plain,
( ~ less(X0,X1)
| less(s(X0),s(X1)) ),
inference(cnf,[status(esa)],[less2]) ).
cnf(l31,plain,
( ~ less(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(s(s(n0))))))))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l18,plain,
( ~ sum(s(s(s(s(s(n0))))),n0,s(s(s(s(s(n0))))))
| sum(s(s(s(s(s(n0))))),s(n0),s(s(s(s(s(s(n0))))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(13,plain,
~ diagonal_attack(X0,X1,empty_list),
inference(cnf,[status(esa)],[check_diagonals2]) ).
cnf(l12,plain,
~ diagonal_attack(s(s(s(s(s(s(n0)))))),s(n0),empty_list),
inference(instantiation,[status(thm)],[13]) ).
cnf(l2,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(s(s(n0)))),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l11,plain,
( ~ do_queens(cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list)),cons(s(s(s(s(s(s(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)))))
| ~ select(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))))))),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)))
| do_queens(cons(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))),cons(s(s(s(s(s(s(n0)))))),empty_list),cons(s(s(s(s(s(s(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)))))
| attack(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list)) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l3,plain,
( ~ sum(s(s(s(s(n0)))),s(s(n0)),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)],[5]) ).
cnf(l33,plain,
( ~ less(s(s(s(n0))),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)],[3]) ).
cnf(l13,plain,
( ~ attack(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list))
| diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(n0),cons(s(s(s(s(s(s(n0)))))),empty_list)) ),
inference(instantiation,[status(thm)],[11]) ).
cnf(l6,plain,
( ~ sum(s(s(s(s(n0)))),s(n0),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)],[5]) ).
cnf(12,plain,
( ~ sum(X0,s(n0),X1)
| ~ sum(X2,X0,X3)
| ~ sum(X4,X0,X2)
| ~ diagonal_attack(X5,X0,cons(X2,X6))
| diagonal_attack(X5,X1,X6)
| same(X4,X5)
| same(X3,X5) ),
inference(cnf,[status(esa)],[check_diagonals1]) ).
cnf(l22,plain,
( ~ sum(s(n0),s(n0),s(s(n0)))
| ~ sum(s(s(s(s(s(s(n0)))))),s(n0),s(s(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(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(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))))))))) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l39,plain,
( ~ less(s(s(n0)),s(s(s(s(s(n0))))))
| less(s(s(s(n0))),s(s(s(s(s(s(n0))))))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l239,plain,
( ~ less(s(n0),s(s(s(s(n0)))))
| less(s(s(n0)),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l20,plain,
sum(s(s(s(s(s(n0))))),n0,s(s(s(s(s(n0)))))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l256,plain,
( ~ less(n0,s(s(s(n0))))
| less(s(n0),s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l19,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(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(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)],[0]) ).
cnf(l26,plain,
( ~ do_queens(cons(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(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list))),cons(s(s(s(s(s(s(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)))))
| ~ select(s(s(s(s(s(n0))))),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)),cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| do_queens(cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list)),cons(s(s(s(s(s(s(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)))))
| attack(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list))) ),
inference(instantiation,[status(thm)],[14]) ).
cnf(l41,plain,
( ~ do_queens(empty_list,cons(s(s(s(s(s(s(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)))),cons(s(s(s(s(s(s(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)))))
| ~ select(s(s(s(s(s(s(s(n0))))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list),empty_list)
| do_queens(cons(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(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list))),cons(s(s(s(s(s(s(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)))))
| attack(s(s(s(s(s(s(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)],[14]) ).
cnf(2,plain,
less(n0,s(X0)),
inference(cnf,[status(esa)],[less1]) ).
cnf(l289,plain,
less(n0,s(s(s(n0)))),
inference(instantiation,[status(thm)],[2]) ).
cnf(l38,plain,
( ~ attack(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(n0)))))),empty_list)))
| 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)],[11]) ).
cnf(15,plain,
do_queens(empty_list,X0,X0),
inference(cnf,[status(esa)],[place_a_queen2]) ).
cnf(l42,plain,
do_queens(empty_list,cons(s(s(s(s(s(s(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)))),cons(s(s(s(s(s(s(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)],[15]) ).
cnf(l46,plain,
select(s(s(s(s(s(n0))))),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)),cons(s(s(s(s(s(s(s(n0))))))),empty_list)),
inference(instantiation,[status(thm)],[6]) ).
cnf(l21,plain,
( ~ less(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(n0))))))))
| less(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(10,plain,
( ~ same(s(X0),s(X1))
| same(X0,X1) ),
inference(cnf,[status(esa)],[same_definition3]) ).
cnf(l36,plain,
( ~ same(s(s(s(s(s(s(s(n0))))))),s(s(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)],[10]) ).
cnf(l25,plain,
( ~ sum(s(s(s(s(s(s(n0)))))),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)))))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l35,plain,
~ diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(s(n0)),empty_list),
inference(instantiation,[status(thm)],[13]) ).
cnf(l30,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))
| ~ 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(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)],[0]) ).
cnf(l54,plain,
( ~ less(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(n0))))))))
| less(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l63,plain,
( ~ less(s(s(s(s(s(n0))))),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)],[3]) ).
cnf(l29,plain,
( ~ sum(s(n0),n0,s(n0))
| sum(s(n0),s(n0),s(s(n0))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l59,plain,
select(s(s(s(s(s(s(s(n0))))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list),empty_list),
inference(instantiation,[status(thm)],[6]) ).
cnf(l49,plain,
( ~ sum(s(s(s(s(s(s(s(n0))))))),n0,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))))))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l56,plain,
( ~ attack(s(s(s(s(s(s(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))))
| 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)],[11]) ).
cnf(l66,plain,
sum(s(s(s(s(s(s(s(n0))))))),n0,s(s(s(s(s(s(s(n0)))))))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l37,plain,
( ~ same(s(s(s(s(s(n0))))),s(s(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)],[10]) ).
cnf(l32,plain,
sum(s(n0),n0,s(n0)),
inference(instantiation,[status(thm)],[4]) ).
cnf(l65,plain,
( ~ less(s(s(s(s(n0)))),s(s(s(s(s(n0))))))
| less(s(s(s(s(s(n0))))),s(s(s(s(s(s(n0))))))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(1,plain,
range(X0,X0,cons(X0,empty_list)),
inference(cnf,[status(esa)],[make_list_of_numbers2]) ).
cnf(l53,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)],[1]) ).
cnf(l14,plain,
( ~ sum(s(s(s(s(n0)))),n0,s(s(s(s(n0)))))
| sum(s(s(s(s(n0)))),s(n0),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l165,plain,
( ~ less(s(s(s(n0))),s(s(s(s(n0)))))
| less(s(s(s(s(n0)))),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l170,plain,
( ~ less(s(s(n0)),s(s(s(n0))))
| less(s(s(s(n0))),s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l220,plain,
( ~ less(s(n0),s(s(n0)))
| less(s(s(n0)),s(s(s(n0)))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l73,plain,
( ~ 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(n0)))),s(n0),s(s(s(s(s(n0))))))
| ~ 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))))
| 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)))
| 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)))))))) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l23,plain,
( ~ less(s(s(s(s(n0)))),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)],[3]) ).
cnf(l136,plain,
( ~ same(s(s(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(n0))))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l60,plain,
( ~ sum(s(n0),s(n0),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))))))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(n0),s(s(s(s(s(s(s(s(n0)))))))))
| ~ 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(n0))))),s(s(n0)),cons(s(s(s(s(s(s(n0)))))),empty_list))
| 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)))))) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l182,plain,
( ~ sum(s(s(n0)),s(n0),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)))))))))))
| ~ sum(s(s(s(s(s(s(n0)))))),s(s(n0)),s(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(s(s(n0))),cons(s(s(s(s(s(s(n0)))))),empty_list))
| same(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(n0))))))))
| same(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(n0)))))))) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l233,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)))))))),s(s(n0)),s(s(s(s(s(s(s(s(s(s(n0))))))))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l78,plain,
( ~ sum(s(s(s(s(s(s(s(n0))))))),n0,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))))))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l27,plain,
( ~ sum(s(s(s(s(s(s(n0)))))),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)))))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l234,plain,
( ~ sum(s(s(s(s(s(s(s(s(n0)))))))),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)))))))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l191,plain,
( ~ sum(s(s(s(s(s(s(s(s(n0)))))))),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)))))))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l202,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)],[4]) ).
cnf(l125,plain,
( ~ sum(s(n0),n0,s(n0))
| sum(s(n0),s(n0),s(s(n0))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l15,plain,
( ~ select(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)),cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| select(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))))))),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))) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l246,plain,
( ~ same(s(s(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(n0))))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l71,plain,
( ~ same(s(s(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(n0))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l198,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)))))),s(s(n0)),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l68,plain,
( ~ sum(s(s(n0)),s(n0),s(s(s(n0))))
| ~ 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(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))
| 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)))))) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l129,plain,
( ~ sum(s(s(s(s(n0)))),n0,s(s(s(s(n0)))))
| sum(s(s(s(s(n0)))),s(n0),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l17,plain,
sum(s(s(s(s(n0)))),n0,s(s(s(s(n0))))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l43,plain,
( ~ less(s(s(s(n0))),s(s(s(s(s(n0))))))
| less(s(s(s(s(n0)))),s(s(s(s(s(s(n0))))))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l103,plain,
sum(s(s(s(s(s(s(s(n0))))))),n0,s(s(s(s(s(s(s(n0)))))))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l24,plain,
( ~ sum(s(s(s(s(s(n0))))),n0,s(s(s(s(s(n0))))))
| sum(s(s(s(s(s(n0))))),s(n0),s(s(s(s(s(s(n0))))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l310,plain,
( ~ less(n0,s(n0))
| less(s(n0),s(s(n0))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l135,plain,
sum(s(s(s(s(n0)))),n0,s(s(s(s(n0))))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l124,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)))))),s(s(n0)),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l104,plain,
~ diagonal_attack(s(s(s(s(s(n0))))),s(s(s(n0))),empty_list),
inference(instantiation,[status(thm)],[13]) ).
cnf(l99,plain,
( ~ sum(s(s(n0)),n0,s(s(n0)))
| sum(s(s(n0)),s(n0),s(s(s(n0)))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l50,plain,
( ~ select(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(s(s(n0)))))))),empty_list),empty_list)
| select(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)),cons(s(s(s(s(s(s(s(n0))))))),empty_list)) ),
inference(instantiation,[status(thm)],[7]) ).
cnf(l70,plain,
( ~ same(s(s(s(s(n0)))),s(s(s(s(s(n0))))))
| same(s(s(s(n0))),s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l45,plain,
( ~ less(s(s(n0)),s(s(s(s(n0)))))
| less(s(s(s(n0))),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l249,plain,
( ~ same(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(s(s(n0))))))))
| same(s(s(s(s(s(s(s(s(s(n0))))))))),s(s(s(s(s(s(n0))))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l251,plain,
( ~ same(s(s(s(s(s(n0))))),s(s(s(s(s(s(n0)))))))
| same(s(s(s(s(n0)))),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l184,plain,
sum(s(s(n0)),n0,s(s(n0))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l408,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)],[4]) ).
cnf(l378,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(n0)))))))),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l98,plain,
( ~ same(s(s(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(n0))))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l28,plain,
sum(s(s(s(s(s(s(n0)))))),n0,s(s(s(s(s(s(n0))))))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l271,plain,
( ~ sum(s(s(s(s(s(s(n0)))))),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)))))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l201,plain,
sum(s(n0),n0,s(n0)),
inference(instantiation,[status(thm)],[4]) ).
cnf(l140,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(n0))))))),s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l311,plain,
less(n0,s(n0)),
inference(instantiation,[status(thm)],[2]) ).
cnf(l75,plain,
( ~ sum(s(s(s(s(n0)))),s(n0),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)],[5]) ).
cnf(l172,plain,
( ~ same(s(s(s(s(s(n0))))),s(s(s(s(s(s(n0)))))))
| same(s(s(s(s(n0)))),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l264,plain,
( ~ same(s(s(s(s(n0)))),s(s(s(s(s(n0))))))
| same(s(s(s(n0))),s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l222,plain,
( ~ sum(s(s(n0)),n0,s(s(n0)))
| sum(s(s(n0)),s(n0),s(s(s(n0)))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l128,plain,
( ~ sum(s(s(s(s(s(n0))))),n0,s(s(s(s(s(n0))))))
| sum(s(s(s(s(s(n0))))),s(n0),s(s(s(s(s(s(n0))))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l380,plain,
sum(s(s(n0)),n0,s(s(n0))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l92,plain,
( ~ same(s(s(s(s(n0)))),s(s(s(s(s(s(s(n0))))))))
| same(s(s(s(n0))),s(s(s(s(s(s(n0))))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l169,plain,
( ~ same(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(s(n0)))))
| same(s(s(s(s(s(s(s(n0))))))),s(s(s(n0)))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l72,plain,
( ~ less(s(n0),s(s(s(n0))))
| less(s(s(n0)),s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l67,plain,
( ~ sum(s(n0),n0,s(n0))
| sum(s(n0),s(n0),s(s(n0))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l277,plain,
( ~ same(s(s(s(n0))),s(s(s(s(s(s(n0)))))))
| same(s(s(n0)),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l144,plain,
( ~ same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(n0)))))
| same(s(s(s(s(s(s(n0)))))),s(s(s(n0)))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l61,plain,
select(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(s(s(s(n0)))))))),empty_list),empty_list),
inference(instantiation,[status(thm)],[6]) ).
cnf(l155,plain,
( ~ sum(s(s(s(s(n0)))),n0,s(s(s(s(n0)))))
| sum(s(s(s(s(n0)))),s(n0),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l151,plain,
( ~ sum(s(s(s(s(s(s(n0)))))),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)))))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l411,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(n0))))))),s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l428,plain,
( ~ same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(n0)))))
| same(s(s(s(s(s(s(n0)))))),s(s(s(n0)))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l34,plain,
sum(s(s(s(s(s(s(n0)))))),n0,s(s(s(s(s(s(n0))))))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l224,plain,
sum(s(s(s(s(s(s(n0)))))),n0,s(s(s(s(s(s(n0))))))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l178,plain,
( ~ same(s(s(s(s(s(s(s(n0))))))),s(s(s(n0))))
| same(s(s(s(s(s(s(n0)))))),s(s(n0))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l183,plain,
( ~ sum(s(s(s(n0))),s(n0),s(s(s(s(n0)))))
| ~ 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(n0))),s(s(s(n0))),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(s(s(n0)))),empty_list)
| same(s(s(s(n0))),s(s(s(s(s(s(s(n0))))))))
| same(s(s(s(s(s(s(s(s(s(n0))))))))),s(s(s(s(s(s(s(n0)))))))) ),
inference(instantiation,[status(thm)],[12]) ).
cnf(l74,plain,
( ~ same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(n0))))))
| same(s(s(s(s(s(s(n0)))))),s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l95,plain,
( ~ same(s(s(s(s(n0)))),s(s(s(s(s(s(s(n0))))))))
| same(s(s(s(n0))),s(s(s(s(s(s(n0))))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l425,plain,
sum(s(s(s(s(s(s(n0)))))),n0,s(s(s(s(s(s(n0))))))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l146,plain,
( ~ same(s(s(s(s(s(n0))))),s(s(s(s(s(s(n0)))))))
| same(s(s(s(s(n0)))),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l297,plain,
( ~ same(s(s(s(s(s(s(s(s(s(n0))))))))),s(s(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)],[10]) ).
cnf(l279,plain,
( ~ same(s(s(s(s(s(s(n0)))))),s(s(s(s(n0)))))
| same(s(s(s(s(s(n0))))),s(s(s(n0)))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l40,plain,
sum(s(s(s(s(s(n0))))),n0,s(s(s(s(s(n0)))))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l154,plain,
( ~ same(s(s(s(s(s(s(n0)))))),s(s(s(n0))))
| same(s(s(s(s(s(n0))))),s(s(n0))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l133,plain,
( ~ same(s(s(s(n0))),s(s(s(s(n0)))))
| same(s(s(n0)),s(s(s(n0)))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l248,plain,
sum(s(n0),n0,s(n0)),
inference(instantiation,[status(thm)],[4]) ).
cnf(l302,plain,
( ~ same(s(s(n0)),s(s(s(s(s(n0))))))
| same(s(n0),s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l265,plain,
( ~ same(s(s(s(n0))),s(s(s(s(n0)))))
| same(s(s(n0)),s(s(s(n0)))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l176,plain,
( ~ same(s(s(s(n0))),s(s(s(s(s(s(n0)))))))
| same(s(s(n0)),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l267,plain,
( ~ same(s(s(n0)),s(s(s(n0))))
| same(s(n0),s(s(n0))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l406,plain,
( ~ same(s(s(s(s(s(n0))))),s(s(s(n0))))
| same(s(s(s(s(n0)))),s(s(n0))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l396,plain,
( ~ same(s(s(n0)),s(s(s(s(s(n0))))))
| same(s(n0),s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l421,plain,
( ~ same(s(s(s(s(n0)))),s(s(s(s(s(n0))))))
| same(s(s(s(n0))),s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l255,plain,
~ diagonal_attack(s(s(s(s(s(s(s(n0))))))),s(s(s(s(n0)))),empty_list),
inference(instantiation,[status(thm)],[13]) ).
cnf(l268,plain,
( ~ same(s(n0),s(s(n0)))
| same(n0,s(n0)) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l414,plain,
( ~ same(s(s(n0)),s(s(s(n0))))
| same(s(n0),s(s(n0))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l296,plain,
( ~ same(s(s(s(n0))),s(s(s(s(s(s(s(n0))))))))
| same(s(s(n0)),s(s(s(s(s(s(n0))))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l405,plain,
( ~ same(s(n0),s(s(s(s(n0)))))
| same(n0,s(s(s(n0)))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(9,plain,
~ same(n0,s(X0)),
inference(cnf,[status(esa)],[same_definition2]) ).
cnf(l432,plain,
~ same(n0,s(s(s(n0)))),
inference(instantiation,[status(thm)],[9]) ).
cnf(l387,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(n0))))))),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l430,plain,
( ~ same(s(s(s(n0))),s(s(s(s(n0)))))
| same(s(s(n0)),s(s(s(n0)))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l416,plain,
( ~ same(s(n0),s(s(n0)))
| same(n0,s(n0)) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l351,plain,
sum(s(s(s(s(n0)))),n0,s(s(s(s(n0))))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l82,plain,
( ~ less(n0,s(s(n0)))
| less(s(n0),s(s(s(n0)))) ),
inference(instantiation,[status(thm)],[3]) ).
cnf(l409,plain,
( ~ same(s(s(s(s(n0)))),s(s(n0)))
| same(s(s(s(n0))),s(n0)) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l417,plain,
~ same(n0,s(n0)),
inference(instantiation,[status(thm)],[9]) ).
cnf(l290,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(s(s(n0))),s(s(s(s(s(s(s(s(s(n0)))))))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l420,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)))))),s(s(n0)),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l185,plain,
( ~ sum(s(s(s(n0))),n0,s(s(s(n0))))
| sum(s(s(s(n0))),s(n0),s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l438,plain,
( ~ same(s(s(n0)),s(s(s(n0))))
| same(s(n0),s(s(n0))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l186,plain,
sum(s(s(s(n0))),n0,s(s(s(n0)))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l221,plain,
( ~ same(s(s(s(s(s(s(n0)))))),s(s(n0)))
| same(s(s(s(s(s(n0))))),s(n0)) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l410,plain,
( ~ same(s(s(n0)),s(s(s(s(s(s(n0)))))))
| same(s(n0),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l441,plain,
( ~ same(s(s(s(n0))),s(n0))
| same(s(s(n0)),n0) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l442,plain,
( ~ sum(s(s(s(s(s(s(n0)))))),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)))))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l108,plain,
less(n0,s(s(n0))),
inference(instantiation,[status(thm)],[2]) ).
cnf(l407,plain,
( ~ same(s(s(s(s(s(n0))))),s(n0))
| same(s(s(s(s(n0)))),n0) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l439,plain,
~ same(n0,s(n0)),
inference(instantiation,[status(thm)],[9]) ).
cnf(l412,plain,
( ~ same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(n0))))))
| same(s(s(s(s(s(s(n0)))))),s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l195,plain,
( ~ same(s(s(s(s(n0)))),s(s(s(s(s(n0))))))
| same(s(s(s(n0))),s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(8,plain,
~ same(s(X0),n0),
inference(cnf,[status(esa)],[same_definition1]) ).
cnf(l435,plain,
~ same(s(s(s(s(n0)))),n0),
inference(instantiation,[status(thm)],[8]) ).
cnf(l446,plain,
sum(s(s(s(s(s(s(n0)))))),n0,s(s(s(s(s(s(n0))))))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l448,plain,
~ same(s(s(n0)),n0),
inference(instantiation,[status(thm)],[8]) ).
cnf(l147,plain,
sum(s(s(s(s(s(n0))))),n0,s(s(s(s(s(n0)))))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l444,plain,
( ~ same(s(n0),s(s(n0)))
| same(n0,s(n0)) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l449,plain,
~ same(n0,s(n0)),
inference(instantiation,[status(thm)],[9]) ).
cnf(l443,plain,
( ~ same(s(s(s(s(s(s(n0)))))),s(s(s(s(n0)))))
| same(s(s(s(s(s(n0))))),s(s(s(n0)))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l431,plain,
( ~ same(s(s(s(s(s(s(n0)))))),s(s(s(n0))))
| same(s(s(s(s(s(n0))))),s(s(n0))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l422,plain,
( ~ same(s(s(s(s(s(n0))))),s(s(n0)))
| same(s(s(s(s(n0)))),s(n0)) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l190,plain,
( ~ sum(s(s(s(n0))),s(s(n0)),s(s(s(s(s(n0))))))
| sum(s(s(s(n0))),s(s(s(n0))),s(s(s(s(s(s(n0))))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l382,plain,
( ~ same(s(n0),s(s(s(s(n0)))))
| same(n0,s(s(s(n0)))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l426,plain,
~ same(n0,s(s(s(n0)))),
inference(instantiation,[status(thm)],[9]) ).
cnf(l427,plain,
( ~ same(s(s(s(s(n0)))),s(n0))
| same(s(s(s(n0))),n0) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l413,plain,
( ~ sum(s(s(s(n0))),s(n0),s(s(s(s(n0)))))
| sum(s(s(s(n0))),s(s(n0)),s(s(s(s(s(n0)))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l423,plain,
( ~ same(s(s(s(n0))),s(s(s(s(n0)))))
| same(s(s(n0)),s(s(s(n0)))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l447,plain,
( ~ same(s(s(s(s(s(n0))))),s(s(s(n0))))
| same(s(s(s(s(n0)))),s(s(n0))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l418,plain,
( ~ same(s(n0),s(s(s(s(s(n0))))))
| same(n0,s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l429,plain,
~ same(s(s(s(n0))),n0),
inference(instantiation,[status(thm)],[8]) ).
cnf(l424,plain,
( ~ same(s(s(n0)),s(s(s(n0))))
| same(s(n0),s(s(n0))) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l451,plain,
( ~ same(s(s(s(s(n0)))),s(s(n0)))
| same(s(s(s(n0))),s(n0)) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l433,plain,
( ~ same(s(s(s(s(s(n0))))),s(s(n0)))
| same(s(s(s(s(n0)))),s(n0)) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l440,plain,
( ~ same(s(s(s(s(n0)))),s(n0))
| same(s(s(s(n0))),n0) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l415,plain,
( ~ sum(s(s(s(n0))),n0,s(s(s(n0))))
| sum(s(s(s(n0))),s(n0),s(s(s(s(n0))))) ),
inference(instantiation,[status(thm)],[5]) ).
cnf(l452,plain,
( ~ same(s(s(s(n0))),s(n0))
| same(s(s(n0)),n0) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l437,plain,
( ~ same(s(n0),s(s(n0)))
| same(n0,s(n0)) ),
inference(instantiation,[status(thm)],[10]) ).
cnf(l453,plain,
~ same(s(s(n0)),n0),
inference(instantiation,[status(thm)],[8]) ).
cnf(l419,plain,
sum(s(s(s(n0))),n0,s(s(s(n0)))),
inference(instantiation,[status(thm)],[4]) ).
cnf(l445,plain,
~ same(s(s(s(n0))),n0),
inference(instantiation,[status(thm)],[8]) ).
cnf(l454,plain,
~ same(n0,s(s(s(s(n0))))),
inference(instantiation,[status(thm)],[9]) ).
cnf(l450,plain,
~ same(n0,s(n0)),
inference(instantiation,[status(thm)],[9]) ).
cnf(final,plain,
$false,
inference(ground_refutation,[status(thm)],[l0,l1,l7,l4,l9,l10,l16,l8,l5,l31,l18,l12,l2,l11,l3,l33,l13,l6,l22,l39,l239,l20,l256,l19,l26,l41,l289,l38,l42,l46,l21,l36,l25,l35,l30,l54,l63,l29,l59,l49,l56,l66,l37,l32,l65,l53,l14,l165,l170,l220,l73,l23,l136,l60,l182,l233,l78,l27,l234,l191,l202,l125,l15,l246,l71,l198,l68,l129,l17,l43,l103,l24,l310,l135,l124,l104,l99,l50,l70,l45,l249,l251,l184,l408,l378,l98,l28,l271,l201,l140,l311,l75,l172,l264,l222,l128,l380,l92,l169,l72,l67,l277,l144,l61,l155,l151,l411,l428,l34,l224,l178,l183,l74,l95,l425,l146,l297,l279,l40,l154,l133,l248,l302,l265,l176,l267,l406,l396,l421,l255,l268,l414,l296,l405,l432,l387,l430,l416,l351,l82,l409,l417,l290,l420,l185,l438,l186,l221,l410,l441,l442,l108,l407,l439,l412,l195,l435,l446,l448,l147,l444,l449,l443,l431,l422,l190,l382,l426,l427,l413,l423,l447,l418,l429,l424,l451,l433,l440,l415,l452,l437,l453,l419,l445,l454,l450]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : PUZ034-1.004 : TPTP v9.0.0. Released v1.0.0.
% 0.12/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.34 % Computer : n019.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Mon Jul 21 15:54:04 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.20/0.34 % launching worker at depth: 1
% 0.20/0.34 % launching worker at depth: 6
% 0.20/0.34 % launching worker at depth: 7
% 0.20/0.34 % launching worker at depth: 5
% 0.20/0.34 % launching worker at depth: 2
% 0.20/0.34 % launching worker at depth: 4
% 0.20/0.34 % launching worker at depth: 8
% 0.20/0.34 % launching worker at depth: 3
% 0.20/0.35 % launching worker at depth: 9
% 0.20/0.35 % launching worker at depth: 10
% 0.20/0.35 % launching worker at depth: 11
% 0.20/0.35 % launching worker at depth: 12
% 0.20/0.35 % launching worker at depth: 13
% 0.20/0.35 % launching worker at depth: 14
% 0.20/0.37 % launching worker at depth: 15
% 0.20/0.37 % launching worker at depth: 16
% 0.20/0.38 % launching worker at depth: 17
% 2.01/0.62 % launching worker at depth: 18
% 2.57/0.68 % launching worker at depth: 19
% 8.35/1.44 % launching worker at depth: 20
% 13.20/2.00 % SZS status Theorem for theBenchmark
% 13.20/2.00 % SZS output start CNFRefutation
% See solution above
%------------------------------------------------------------------------------