%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PUZ034-1.004 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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 : Sun Sep 27 08:23:10 AM UTC 2026
% Result : Unsatisfiable 258.14s 35.52s
% Output : CNFRefutation 258.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 18
% Syntax : Number of formulae : 126 ( 54 unt; 0 def)
% Number of atoms : 318 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 323 ( 131 ~; 192 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 3 avg)
% Maximal term depth : 13 ( 4 avg)
% 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 : 240 ( 34 sgn 45 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(place_a_queen1,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ do_queens(VAR_4,cons(VAR_3,VAR_1),VAR_2)
| attack(VAR_3,VAR_1)
| ~ select(VAR_3,VAR_0,VAR_4)
| do_queens(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',place_a_queen1) ).
cnf(c_1,plain,
( ~ do_queens(E,cons(D,B),C)
| attack(D,B)
| ~ select(D,A,E)
| do_queens(A,B,C) ),
inference(clausify,[status(thm)],[place_a_queen1]) ).
fof(attack,axiom,
! [VAR_0,VAR_1] :
( ~ attack(VAR_0,VAR_1)
| diagonal_attack(VAR_0,s(n0),VAR_1) ),
file('theBenchmark.p',attack) ).
cnf(c_2,plain,
( ~ attack(A,B)
| diagonal_attack(A,s(n0),B) ),
inference(clausify,[status(thm)],[attack]) ).
fof(set_up_queens,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ do_queens(VAR_4,empty_list,VAR_1)
| ~ range(VAR_2,VAR_3,VAR_4)
| ~ sum(VAR_0,VAR_0,VAR_3)
| ~ sum(VAR_0,s(n0),VAR_2)
| queens(VAR_0,VAR_1) ),
file('theBenchmark.p',set_up_queens) ).
cnf(c_3,plain,
( ~ do_queens(E,empty_list,B)
| ~ range(C,D,E)
| ~ sum(A,A,D)
| ~ sum(A,s(n0),C)
| queens(A,B) ),
inference(clausify,[status(thm)],[set_up_queens]) ).
fof(place_queens,axiom,
! [VAR_0] : ~ queens(s(s(s(s(n0)))),VAR_0),
file('theBenchmark.p',place_queens) ).
cnf(c_4,plain,
~ queens(s(s(s(s(n0)))),A),
inference(clausify,[status(thm)],[place_queens]) ).
cnf(c_5,plain,
( ~ do_queens(C,empty_list,D)
| ~ range(A,B,C)
| ~ sum(s(s(s(s(n0)))),s(s(s(s(n0)))),B)
| ~ sum(s(s(s(s(n0)))),s(n0),A) ),
inference(resolve,[status(thm)],[c_3,c_4]) ).
fof(make_list_of_numbers1,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ range(VAR_3,VAR_1,VAR_2)
| ~ sum(VAR_0,s(n0),VAR_3)
| ~ less(VAR_0,VAR_1)
| range(VAR_0,VAR_1,cons(VAR_0,VAR_2)) ),
file('theBenchmark.p',make_list_of_numbers1) ).
cnf(c_6,plain,
( ~ range(D,B,C)
| ~ sum(A,s(n0),D)
| ~ less(A,B)
| range(A,B,cons(A,C)) ),
inference(clausify,[status(thm)],[make_list_of_numbers1]) ).
fof(make_list_of_numbers2,axiom,
! [VAR_0] : range(VAR_0,VAR_0,cons(VAR_0,empty_list)),
file('theBenchmark.p',make_list_of_numbers2) ).
cnf(c_7,plain,
range(A,A,cons(A,empty_list)),
inference(clausify,[status(thm)],[make_list_of_numbers2]) ).
fof(less1,axiom,
! [VAR_0] : less(n0,s(VAR_0)),
file('theBenchmark.p',less1) ).
cnf(c_8,plain,
less(n0,s(A)),
inference(clausify,[status(thm)],[less1]) ).
fof(less2,axiom,
! [VAR_0,VAR_1] :
( ~ less(VAR_0,VAR_1)
| less(s(VAR_0),s(VAR_1)) ),
file('theBenchmark.p',less2) ).
cnf(c_9,plain,
( ~ less(A,B)
| less(s(A),s(B)) ),
inference(clausify,[status(thm)],[less2]) ).
fof(add_0,axiom,
! [VAR_0] : sum(VAR_0,n0,VAR_0),
file('theBenchmark.p',add_0) ).
cnf(c_10,plain,
sum(A,n0,A),
inference(clausify,[status(thm)],[add_0]) ).
fof(add,axiom,
! [VAR_0,VAR_1,VAR_2] :
( sum(VAR_0,s(VAR_1),s(VAR_2))
| ~ sum(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',add) ).
cnf(c_11,plain,
( sum(A,s(B),s(C))
| ~ sum(A,B,C) ),
inference(clausify,[status(thm)],[add]) ).
fof(select1,axiom,
! [VAR_0,VAR_1] : select(VAR_0,cons(VAR_0,VAR_1),VAR_1),
file('theBenchmark.p',select1) ).
cnf(c_12,plain,
select(A,cons(A,B),B),
inference(clausify,[status(thm)],[select1]) ).
fof(select2,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ select(VAR_0,VAR_2,VAR_3)
| select(VAR_0,cons(VAR_1,VAR_2),cons(VAR_1,VAR_3)) ),
file('theBenchmark.p',select2) ).
cnf(c_13,plain,
( ~ select(A,C,D)
| select(A,cons(B,C),cons(B,D)) ),
inference(clausify,[status(thm)],[select2]) ).
fof(same_definition1,axiom,
! [VAR_0] : ~ same(s(VAR_0),n0),
file('theBenchmark.p',same_definition1) ).
cnf(c_14,plain,
~ same(s(A),n0),
inference(clausify,[status(thm)],[same_definition1]) ).
fof(same_definition2,axiom,
! [VAR_0] : ~ same(n0,s(VAR_0)),
file('theBenchmark.p',same_definition2) ).
cnf(c_15,plain,
~ same(n0,s(A)),
inference(clausify,[status(thm)],[same_definition2]) ).
fof(same_definition3,axiom,
! [VAR_0,VAR_1] :
( same(VAR_0,VAR_1)
| ~ same(s(VAR_0),s(VAR_1)) ),
file('theBenchmark.p',same_definition3) ).
cnf(c_16,plain,
( same(A,B)
| ~ same(s(A),s(B)) ),
inference(clausify,[status(thm)],[same_definition3]) ).
fof(check_diagonals1,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( diagonal_attack(VAR_0,VAR_6,VAR_3)
| ~ sum(VAR_1,s(n0),VAR_6)
| same(VAR_5,VAR_0)
| ~ sum(VAR_2,VAR_1,VAR_5)
| same(VAR_4,VAR_0)
| ~ sum(VAR_4,VAR_1,VAR_2)
| ~ diagonal_attack(VAR_0,VAR_1,cons(VAR_2,VAR_3)) ),
file('theBenchmark.p',check_diagonals1) ).
cnf(c_17,plain,
( diagonal_attack(A,V6,D)
| ~ sum(B,s(n0),V6)
| same(F,A)
| ~ sum(C,B,F)
| same(E,A)
| ~ sum(E,B,C)
| ~ diagonal_attack(A,B,cons(C,D)) ),
inference(clausify,[status(thm)],[check_diagonals1]) ).
fof(check_diagonals2,axiom,
! [VAR_0,VAR_1] : ~ diagonal_attack(VAR_0,VAR_1,empty_list),
file('theBenchmark.p',check_diagonals2) ).
cnf(c_18,plain,
~ diagonal_attack(A,B,empty_list),
inference(clausify,[status(thm)],[check_diagonals2]) ).
fof(place_a_queen2,axiom,
! [VAR_0] : do_queens(empty_list,VAR_0,VAR_0),
file('theBenchmark.p',place_a_queen2) ).
cnf(c_19,plain,
do_queens(empty_list,A,A),
inference(clausify,[status(thm)],[place_a_queen2]) ).
cnf(c_20,plain,
( diagonal_attack(D,s(n0),B)
| ~ do_queens(E,cons(D,B),C)
| ~ select(D,A,E)
| do_queens(A,B,C) ),
inference(resolve,[status(thm)],[c_1,c_2]) ).
cnf(c_28,plain,
( ~ sum(A,s(n0),B)
| ~ less(A,B)
| range(A,B,cons(A,cons(B,empty_list))) ),
inference(resolve,[status(thm)],[c_7,c_6]) ).
cnf(c_30,plain,
less(s(n0),s(s(A))),
inference(resolve,[status(thm)],[c_9,c_8]) ).
cnf(c_31,plain,
sum(A,s(n0),s(A)),
inference(resolve,[status(thm)],[c_11,c_10]) ).
cnf(c_32,plain,
select(A,cons(B,cons(A,C)),cons(B,C)),
inference(resolve,[status(thm)],[c_13,c_12]) ).
cnf(c_33,plain,
~ same(s(n0),s(s(A))),
inference(resolve,[status(thm)],[c_16,c_15]) ).
cnf(c_34,plain,
~ same(s(s(A)),s(n0)),
inference(resolve,[status(thm)],[c_16,c_14]) ).
cnf(c_2584,plain,
( diagonal_attack(A,s(n0),C)
| ~ do_queens(B,cons(A,C),D)
| do_queens(cons(A,B),C,D) ),
inference(resolve,[status(thm)],[c_20,c_12]) ).
cnf(c_36,plain,
( diagonal_attack(A,s(n0),B)
| do_queens(cons(A,empty_list),B,cons(A,B)) ),
inference(resolve,[status(thm)],[c_2584,c_19]) ).
cnf(c_37,plain,
~ same(s(s(n0)),s(s(s(A)))),
inference(resolve,[status(thm)],[c_16,c_33]) ).
cnf(c_38,plain,
~ same(s(s(s(A))),s(s(n0))),
inference(resolve,[status(thm)],[c_16,c_34]) ).
cnf(c_39,plain,
~ same(s(s(s(n0))),s(s(s(s(A))))),
inference(resolve,[status(thm)],[c_16,c_37]) ).
cnf(c_40,plain,
~ same(s(s(s(s(A)))),s(s(s(n0)))),
inference(resolve,[status(thm)],[c_16,c_38]) ).
cnf(c_41,plain,
( ~ less(A,s(A))
| range(A,s(A),cons(A,cons(s(A),empty_list))) ),
inference(resolve,[status(thm)],[c_31,c_28]) ).
cnf(c_42,plain,
sum(A,s(s(n0)),s(s(A))),
inference(resolve,[status(thm)],[c_31,c_11]) ).
cnf(c_57,plain,
less(s(s(n0)),s(s(s(A)))),
inference(resolve,[status(thm)],[c_30,c_9]) ).
cnf(c_59,plain,
sum(A,s(s(s(n0))),s(s(s(A)))),
inference(resolve,[status(thm)],[c_42,c_11]) ).
cnf(c_66,plain,
select(A,cons(B,cons(C,cons(A,D))),cons(B,cons(C,D))),
inference(resolve,[status(thm)],[c_32,c_13]) ).
cnf(c_69,plain,
less(s(s(s(n0))),s(s(s(s(A))))),
inference(resolve,[status(thm)],[c_57,c_9]) ).
cnf(c_2585,plain,
( diagonal_attack(B,s(n0),D)
| ~ do_queens(cons(A,C),cons(B,D),E)
| do_queens(cons(A,cons(B,C)),D,E) ),
inference(resolve,[status(thm)],[c_20,c_32]) ).
cnf(c_73,plain,
( diagonal_attack(A,s(n0),cons(B,C))
| diagonal_attack(B,s(n0),C)
| do_queens(cons(A,cons(B,empty_list)),C,cons(A,cons(B,C))) ),
inference(resolve,[status(thm)],[c_2585,c_36]) ).
cnf(c_77,plain,
sum(A,s(s(s(s(n0)))),s(s(s(s(A))))),
inference(resolve,[status(thm)],[c_59,c_11]) ).
cnf(c_91,plain,
less(s(s(s(s(n0)))),s(s(s(s(s(A)))))),
inference(resolve,[status(thm)],[c_69,c_9]) ).
cnf(c_107,plain,
~ same(s(s(s(s(n0)))),s(s(s(s(s(A)))))),
inference(resolve,[status(thm)],[c_16,c_39]) ).
cnf(c_124,plain,
~ same(s(s(s(s(s(A))))),s(s(s(s(n0))))),
inference(resolve,[status(thm)],[c_16,c_40]) ).
cnf(c_131,plain,
less(s(s(s(s(s(n0))))),s(s(s(s(s(s(A))))))),
inference(resolve,[status(thm)],[c_91,c_9]) ).
cnf(c_154,plain,
less(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(A)))))))),
inference(resolve,[status(thm)],[c_131,c_9]) ).
cnf(c_2586,plain,
( diagonal_attack(A,s(n0),C)
| ~ do_queens(B,cons(A,C),D)
| do_queens(cons(A,B),C,D) ),
inference(resolve,[status(thm)],[c_20,c_12]) ).
cnf(c_161,plain,
( diagonal_attack(B,s(n0),cons(C,cons(A,D)))
| diagonal_attack(C,s(n0),cons(A,D))
| diagonal_attack(A,s(n0),D)
| do_queens(cons(A,cons(B,cons(C,empty_list))),D,cons(B,cons(C,cons(A,D)))) ),
inference(resolve,[status(thm)],[c_2586,c_73]) ).
cnf(c_199,plain,
less(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(s(A))))))))),
inference(resolve,[status(thm)],[c_154,c_9]) ).
cnf(c_225,plain,
~ same(s(s(s(s(s(n0))))),s(s(s(s(s(s(A))))))),
inference(resolve,[status(thm)],[c_16,c_107]) ).
cnf(c_263,plain,
~ same(s(s(s(s(s(s(A)))))),s(s(s(s(s(n0)))))),
inference(resolve,[status(thm)],[c_16,c_124]) ).
cnf(c_267,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(resolve,[status(thm)],[c_199,c_41]) ).
cnf(c_2587,plain,
( diagonal_attack(C,s(n0),E)
| ~ do_queens(cons(A,cons(B,D)),cons(C,E),F)
| do_queens(cons(A,cons(B,cons(C,D))),E,F) ),
inference(resolve,[status(thm)],[c_20,c_66]) ).
cnf(c_367,plain,
( diagonal_attack(B,s(n0),cons(D,cons(A,cons(C,E))))
| diagonal_attack(D,s(n0),cons(A,cons(C,E)))
| diagonal_attack(A,s(n0),cons(C,E))
| diagonal_attack(C,s(n0),E)
| do_queens(cons(A,cons(B,cons(C,cons(D,empty_list)))),E,cons(B,cons(D,cons(A,cons(C,E))))) ),
inference(resolve,[status(thm)],[c_2587,c_161]) ).
cnf(c_450,plain,
~ same(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(A)))))))),
inference(resolve,[status(thm)],[c_16,c_225]) ).
cnf(c_2588,plain,
( diagonal_attack(A,E,C)
| ~ sum(s(n0),s(n0),E)
| same(D,A)
| ~ sum(s(B),s(n0),D)
| same(B,A)
| ~ diagonal_attack(A,s(n0),cons(s(B),C)) ),
inference(resolve,[status(thm)],[c_17,c_31]) ).
cnf(c_2589,plain,
( diagonal_attack(s(s(s(s(s(n0))))),D,B)
| ~ sum(s(n0),s(n0),D)
| same(C,s(s(s(s(s(n0))))))
| ~ sum(s(s(s(s(s(s(s(A))))))),s(n0),C)
| ~ diagonal_attack(s(s(s(s(s(n0))))),s(n0),cons(s(s(s(s(s(s(s(A))))))),B)) ),
inference(resolve,[status(thm)],[c_2588,c_263]) ).
cnf(c_2590,plain,
( diagonal_attack(s(s(s(s(s(n0))))),C,B)
| ~ sum(s(n0),s(n0),C)
| same(s(s(s(s(s(s(s(s(A)))))))),s(s(s(s(s(n0))))))
| ~ diagonal_attack(s(s(s(s(s(n0))))),s(n0),cons(s(s(s(s(s(s(s(A))))))),B)) ),
inference(resolve,[status(thm)],[c_2589,c_31]) ).
cnf(c_2591,plain,
( diagonal_attack(s(s(s(s(s(n0))))),C,B)
| ~ sum(s(n0),s(n0),C)
| ~ diagonal_attack(s(s(s(s(s(n0))))),s(n0),cons(s(s(s(s(s(s(s(A))))))),B)) ),
inference(resolve,[status(thm)],[c_2590,c_263]) ).
cnf(c_2592,plain,
( diagonal_attack(s(s(s(s(s(n0))))),s(s(n0)),B)
| ~ diagonal_attack(s(s(s(s(s(n0))))),s(n0),cons(s(s(s(s(s(s(s(A))))))),B)) ),
inference(resolve,[status(thm)],[c_2591,c_31]) ).
cnf(c_543,plain,
~ diagonal_attack(s(s(s(s(s(n0))))),s(n0),cons(s(s(s(s(s(s(s(A))))))),empty_list)),
inference(resolve,[status(thm)],[c_2592,c_18]) ).
cnf(c_546,plain,
~ same(s(s(s(s(s(s(s(A))))))),s(s(s(s(s(s(n0))))))),
inference(resolve,[status(thm)],[c_16,c_263]) ).
cnf(c_2593,plain,
( ~ range(C,s(s(s(s(s(s(s(A))))))),B)
| ~ sum(s(s(s(s(s(s(n0)))))),s(n0),C)
| range(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(A))))))),cons(s(s(s(s(s(s(n0)))))),B)) ),
inference(resolve,[status(thm)],[c_6,c_154]) ).
cnf(c_2594,plain,
( ~ range(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(s(A))))))),B)
| range(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(A))))))),cons(s(s(s(s(s(s(n0)))))),B)) ),
inference(resolve,[status(thm)],[c_2593,c_31]) ).
cnf(c_640,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(resolve,[status(thm)],[c_2594,c_267]) ).
cnf(c_2595,plain,
( ~ range(C,s(s(s(s(s(s(A)))))),B)
| ~ sum(s(s(s(s(s(n0))))),s(n0),C)
| range(s(s(s(s(s(n0))))),s(s(s(s(s(s(A)))))),cons(s(s(s(s(s(n0))))),B)) ),
inference(resolve,[status(thm)],[c_6,c_131]) ).
cnf(c_2596,plain,
( ~ range(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(A)))))),B)
| range(s(s(s(s(s(n0))))),s(s(s(s(s(s(A)))))),cons(s(s(s(s(s(n0))))),B)) ),
inference(resolve,[status(thm)],[c_2595,c_31]) ).
cnf(c_1015,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(resolve,[status(thm)],[c_2596,c_640]) ).
cnf(c_2597,plain,
( diagonal_attack(A,E,C)
| ~ sum(s(s(s(n0))),s(n0),E)
| same(D,A)
| ~ sum(s(s(s(B))),s(s(s(n0))),D)
| same(B,A)
| ~ diagonal_attack(A,s(s(s(n0))),cons(s(s(s(B))),C)) ),
inference(resolve,[status(thm)],[c_17,c_59]) ).
cnf(c_2598,plain,
( diagonal_attack(s(s(s(s(s(A))))),D,B)
| ~ sum(s(s(s(n0))),s(n0),D)
| same(C,s(s(s(s(s(A))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(s(s(n0))),C)
| ~ diagonal_attack(s(s(s(s(s(A))))),s(s(s(n0))),cons(s(s(s(s(s(s(s(n0))))))),B)) ),
inference(resolve,[status(thm)],[c_2597,c_107]) ).
cnf(c_2599,plain,
( diagonal_attack(s(s(s(s(s(A))))),C,B)
| ~ sum(s(s(s(n0))),s(n0),C)
| same(s(s(s(s(s(s(s(s(s(s(n0)))))))))),s(s(s(s(s(A))))))
| ~ diagonal_attack(s(s(s(s(s(A))))),s(s(s(n0))),cons(s(s(s(s(s(s(s(n0))))))),B)) ),
inference(resolve,[status(thm)],[c_2598,c_59]) ).
cnf(c_2600,plain,
( diagonal_attack(s(s(s(s(s(s(n0)))))),B,A)
| ~ sum(s(s(s(n0))),s(n0),B)
| ~ diagonal_attack(s(s(s(s(s(s(n0)))))),s(s(s(n0))),cons(s(s(s(s(s(s(s(n0))))))),A)) ),
inference(resolve,[status(thm)],[c_2599,c_546]) ).
cnf(c_2601,plain,
( diagonal_attack(s(s(s(s(s(s(n0)))))),s(s(s(s(n0)))),A)
| ~ diagonal_attack(s(s(s(s(s(s(n0)))))),s(s(s(n0))),cons(s(s(s(s(s(s(s(n0))))))),A)) ),
inference(resolve,[status(thm)],[c_2600,c_31]) ).
cnf(c_1138,plain,
~ diagonal_attack(s(s(s(s(s(s(n0)))))),s(s(s(n0))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)),
inference(resolve,[status(thm)],[c_2601,c_18]) ).
cnf(c_1152,plain,
~ same(s(s(s(s(s(s(s(s(A)))))))),s(s(s(s(s(s(s(n0)))))))),
inference(resolve,[status(thm)],[c_16,c_546]) ).
cnf(c_2602,plain,
( ~ do_queens(B,empty_list,C)
| ~ range(s(s(s(s(s(n0))))),A,B)
| ~ sum(s(s(s(s(n0)))),s(s(s(s(n0)))),A) ),
inference(resolve,[status(thm)],[c_5,c_31]) ).
cnf(c_2603,plain,
( ~ do_queens(A,empty_list,B)
| ~ range(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(s(n0)))))))),A) ),
inference(resolve,[status(thm)],[c_2602,c_77]) ).
cnf(c_2604,plain,
~ 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,A),
inference(resolve,[status(thm)],[c_2603,c_1015]) ).
cnf(c_2605,plain,
( diagonal_attack(s(s(s(s(s(s(n0)))))),s(n0),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list))))
| diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(n0),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| diagonal_attack(s(s(s(s(s(n0))))),s(n0),cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| diagonal_attack(s(s(s(s(s(s(s(n0))))))),s(n0),empty_list) ),
inference(resolve,[status(thm)],[c_2604,c_367]) ).
cnf(c_2606,plain,
( diagonal_attack(s(s(s(s(s(s(n0)))))),s(n0),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list))))
| diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(n0),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| diagonal_attack(s(s(s(s(s(n0))))),s(n0),cons(s(s(s(s(s(s(s(n0))))))),empty_list)) ),
inference(resolve,[status(thm)],[c_18,c_2605]) ).
cnf(c_1295,plain,
( diagonal_attack(s(s(s(s(s(s(n0)))))),s(n0),cons(s(s(s(s(s(s(s(s(n0)))))))),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list))))
| diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(n0),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list))) ),
inference(resolve,[status(thm)],[c_543,c_2606]) ).
cnf(c_1901,plain,
~ same(s(s(s(s(s(s(s(s(s(A))))))))),s(s(s(s(s(s(s(s(n0))))))))),
inference(resolve,[status(thm)],[c_16,c_1152]) ).
cnf(c_2607,plain,
( diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(n0),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| diagonal_attack(s(s(s(s(s(s(n0)))))),C,cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| ~ sum(s(n0),s(n0),C)
| same(B,s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(s(s(s(n0)))))))),s(n0),B)
| same(A,s(s(s(s(s(s(n0)))))))
| ~ sum(A,s(n0),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(resolve,[status(thm)],[c_17,c_1295]) ).
cnf(c_2608,plain,
( diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(n0),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| diagonal_attack(s(s(s(s(s(s(n0)))))),B,cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| ~ sum(s(n0),s(n0),B)
| same(A,s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(s(s(s(n0)))))))),s(n0),A)
| same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(n0))))))) ),
inference(resolve,[status(thm)],[c_2607,c_31]) ).
cnf(c_2609,plain,
( diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(n0),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| diagonal_attack(s(s(s(s(s(s(n0)))))),A,cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| ~ sum(s(n0),s(n0),A)
| 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(n0))))))),s(s(s(s(s(s(n0))))))) ),
inference(resolve,[status(thm)],[c_2608,c_31]) ).
cnf(c_2610,plain,
( diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(n0),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| diagonal_attack(s(s(s(s(s(s(n0)))))),s(s(n0)),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| 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(n0))))))),s(s(s(s(s(s(n0))))))) ),
inference(resolve,[status(thm)],[c_2609,c_31]) ).
cnf(c_2611,plain,
( diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(n0),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| diagonal_attack(s(s(s(s(s(s(n0)))))),s(s(n0)),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| same(s(s(s(s(s(s(s(s(s(n0))))))))),s(s(s(s(s(s(n0))))))) ),
inference(resolve,[status(thm)],[c_546,c_2610]) ).
cnf(c_2561,plain,
( diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(n0),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| diagonal_attack(s(s(s(s(s(s(n0)))))),s(s(n0)),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list))) ),
inference(resolve,[status(thm)],[c_546,c_2611]) ).
cnf(c_2612,plain,
( diagonal_attack(s(s(s(s(s(s(n0)))))),s(s(n0)),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),C,cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| ~ sum(s(n0),s(n0),C)
| same(B,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(s(n0))))),s(n0),B)
| same(A,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(A,s(n0),s(s(s(s(s(n0)))))) ),
inference(resolve,[status(thm)],[c_17,c_2561]) ).
cnf(c_2613,plain,
( diagonal_attack(s(s(s(s(s(s(n0)))))),s(s(n0)),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),B,cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| ~ sum(s(n0),s(n0),B)
| same(A,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(s(n0))))),s(n0),A)
| same(s(s(s(s(n0)))),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(resolve,[status(thm)],[c_2612,c_31]) ).
cnf(c_2614,plain,
( diagonal_attack(s(s(s(s(s(s(n0)))))),s(s(n0)),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),A,cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| ~ sum(s(n0),s(n0),A)
| same(s(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(s(n0))))))))) ),
inference(resolve,[status(thm)],[c_2613,c_31]) ).
cnf(c_2615,plain,
( diagonal_attack(s(s(s(s(s(s(n0)))))),s(s(n0)),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(s(n0)),cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| same(s(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(s(n0))))))))) ),
inference(resolve,[status(thm)],[c_2614,c_31]) ).
cnf(c_2616,plain,
( diagonal_attack(s(s(s(s(s(s(n0)))))),s(s(n0)),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(s(n0)),cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| same(s(s(s(s(s(s(n0)))))),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(resolve,[status(thm)],[c_107,c_2615]) ).
cnf(c_2564,plain,
( diagonal_attack(s(s(s(s(s(s(n0)))))),s(s(n0)),cons(s(s(s(s(s(n0))))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)))
| diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(s(n0)),cons(s(s(s(s(s(s(s(n0))))))),empty_list)) ),
inference(resolve,[status(thm)],[c_450,c_2616]) ).
cnf(c_2617,plain,
( diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(s(n0)),cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| diagonal_attack(s(s(s(s(s(s(n0)))))),C,cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| ~ sum(s(s(n0)),s(n0),C)
| same(B,s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(n0))))),s(s(n0)),B)
| same(A,s(s(s(s(s(s(n0)))))))
| ~ sum(A,s(s(n0)),s(s(s(s(s(n0)))))) ),
inference(resolve,[status(thm)],[c_17,c_2564]) ).
cnf(c_2618,plain,
( diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(s(n0)),cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| diagonal_attack(s(s(s(s(s(s(n0)))))),B,cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| ~ sum(s(s(n0)),s(n0),B)
| same(A,s(s(s(s(s(s(n0)))))))
| ~ sum(s(s(s(s(s(n0))))),s(s(n0)),A)
| same(s(s(s(n0))),s(s(s(s(s(s(n0))))))) ),
inference(resolve,[status(thm)],[c_2617,c_42]) ).
cnf(c_2619,plain,
( diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(s(n0)),cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| diagonal_attack(s(s(s(s(s(s(n0)))))),A,cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| ~ sum(s(s(n0)),s(n0),A)
| same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(n0)))))))
| same(s(s(s(n0))),s(s(s(s(s(s(n0))))))) ),
inference(resolve,[status(thm)],[c_2618,c_42]) ).
cnf(c_2620,plain,
( diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(s(n0)),cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| diagonal_attack(s(s(s(s(s(s(n0)))))),s(s(s(n0))),cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(n0)))))))
| same(s(s(s(n0))),s(s(s(s(s(s(n0))))))) ),
inference(resolve,[status(thm)],[c_2619,c_31]) ).
cnf(c_2621,plain,
( diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(s(n0)),cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| diagonal_attack(s(s(s(s(s(s(n0)))))),s(s(s(n0))),cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| same(s(s(s(s(s(s(s(n0))))))),s(s(s(s(s(s(n0))))))) ),
inference(resolve,[status(thm)],[c_39,c_2620]) ).
cnf(c_2622,plain,
( diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(s(n0)),cons(s(s(s(s(s(s(s(n0))))))),empty_list))
| diagonal_attack(s(s(s(s(s(s(n0)))))),s(s(s(n0))),cons(s(s(s(s(s(s(s(n0))))))),empty_list)) ),
inference(resolve,[status(thm)],[c_546,c_2621]) ).
cnf(c_2567,plain,
diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(s(n0)),cons(s(s(s(s(s(s(s(n0))))))),empty_list)),
inference(resolve,[status(thm)],[c_1138,c_2622]) ).
cnf(c_2623,plain,
( diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),C,empty_list)
| ~ sum(s(s(n0)),s(n0),C)
| same(B,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(s(n0)),B)
| same(A,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(A,s(s(n0)),s(s(s(s(s(s(s(n0)))))))) ),
inference(resolve,[status(thm)],[c_17,c_2567]) ).
cnf(c_2624,plain,
( diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),B,empty_list)
| ~ sum(s(s(n0)),s(n0),B)
| same(A,s(s(s(s(s(s(s(s(n0)))))))))
| ~ sum(s(s(s(s(s(s(s(n0))))))),s(s(n0)),A)
| same(s(s(s(s(s(n0))))),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(resolve,[status(thm)],[c_2623,c_42]) ).
cnf(c_2625,plain,
( diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),A,empty_list)
| ~ sum(s(s(n0)),s(n0),A)
| same(s(s(s(s(s(s(s(s(s(n0))))))))),s(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(resolve,[status(thm)],[c_2624,c_42]) ).
cnf(c_2626,plain,
( diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(n0))),empty_list)
| same(s(s(s(s(s(s(s(s(s(n0))))))))),s(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(resolve,[status(thm)],[c_2625,c_31]) ).
cnf(c_2627,plain,
( diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(n0))),empty_list)
| same(s(s(s(s(s(s(s(s(s(n0))))))))),s(s(s(s(s(s(s(s(n0))))))))) ),
inference(resolve,[status(thm)],[c_225,c_2626]) ).
cnf(c_2628,plain,
diagonal_attack(s(s(s(s(s(s(s(s(n0)))))))),s(s(s(n0))),empty_list),
inference(resolve,[status(thm)],[c_1901,c_2627]) ).
cnf(c_2583,plain,
$false,
inference(resolve,[status(thm)],[c_18,c_2628]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ034-1.004 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.52 % Computer : n017.cluster.edu
% 0.07/0.52 % Model : x86_64 x86_64
% 0.07/0.52 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.52 % Memory : 8046.5625MB
% 0.07/0.52 % OS : Linux 6.8.0-71-generic
% 0.07/0.52 % CPULimit : 300
% 0.07/0.52 % WCLimit : 300
% 0.07/0.52 % DateTime : Sat Sep 26 05:01:34 UTC 2026
% 0.07/0.52 % CPUTime :
% 0.07/0.52 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/0.52 % Process 4072288 was started by sandbox on n017,
% 0.07/0.52 % Sat Sep 26 05:01:34 2026
% 0.07/0.52 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.07/0.53
% 0.07/0.53 % From the command line: assign(max_seconds, 300).
% 258.14/35.52
% 258.14/35.52 % Assigning unary symbol s kb_weight 0 and highest precedence (11).
% 258.14/35.52
% 258.14/35.52 % given #500 (T,wt=64): 1476 -sum(s(s(s(s(n0)))),s(n0),s(n0)) | -sum(s(s(s(s(n0)))),s(s(s(s(n0)))),s(s(s(n0)))) | diagonal_attack(s(s(n0)),s(n0),cons(s(s(s(n0))),empty_list)) | diagonal_attack(s(n0),s(n0),cons(s(s(n0)),cons(s(s(s(n0))),empty_list))). [resolve(202,c,159,a),unit_del(c,18)].
% 258.14/35.52
% 258.14/35.52 % SZS status Unsatisfiable for theBenchmark
% 258.14/35.52
% 258.14/35.52 % Proof 1 at 2.54 (+ 0.05) seconds.
% 258.14/35.52 % Length of proof is 63.
% 258.14/35.52 % Level of proof is 15.
% 258.14/35.52 % Maximum clause weight is 88.000.
% 258.14/35.52 % Given clauses 989.
% 258.14/35.52
% 258.14/35.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------