%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PUZ129+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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:21 AM UTC 2026
% Result : Theorem 0.09s 0.38s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 1
% Syntax : Number of formulae : 51 ( 20 unt; 0 def)
% Number of atoms : 282 ( 73 equ)
% Maximal formula atoms : 46 ( 5 avg)
% Number of connectives : 364 ( 133 ~; 110 |; 99 &)
% ( 0 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-1 aty)
% Number of variables : 104 ( 0 sgn 62 !; 28 ?)
% Comments :
%------------------------------------------------------------------------------
fof(prove,conjecture,
( ( ! [Q] :
( cyclist(Q)
=> ? [R] :
( Q = R
& person(R) ) )
& ! [O] :
( grocer(O)
=> ? [P] :
( O = P
& person(P) ) )
& ! [M] :
( ( property1(M,honest,pos)
& person(M) )
=> ~ ? [N] :
( M = N
& property1(N,dishonest,pos) ) )
& ! [K] :
( ( property1(K,healthy,pos)
& person(K) )
=> ~ ? [L] :
( K = L
& property1(L,unhealthy,pos) ) )
& ! [I] :
( ( property1(I,unhealthy,pos)
& cyclist(I) )
=> ? [J] :
( I = J
& property1(J,dishonest,pos) ) )
& ! [G] :
( cyclist(G)
=> ? [H] :
( G = H
& property1(H,industrious,pos) ) )
& ! [E] :
( ( property1(E,industrious,pos)
& grocer(E) )
=> ? [F] :
( E = F
& property1(F,honest,pos) ) )
& ! [C] :
( grocer(C)
=> ~ ? [D] :
( C = D
& property1(D,healthy,pos) ) )
& ! [A] :
( ( property1(A,industrious,pos)
& property1(A,honest,pos)
& person(A) )
=> ? [B] :
( A = B
& property1(B,healthy,pos) ) ) )
=> ! [S] :
( grocer(S)
=> ~ ? [T] :
( S = T
& cyclist(T) ) ) ),
file('theBenchmark.p',prove) ).
fof(prove_neg,negated_conjecture,
~ ( ( ! [Q] :
( cyclist(Q)
=> ? [R] :
( Q = R
& person(R) ) )
& ! [O] :
( grocer(O)
=> ? [P] :
( O = P
& person(P) ) )
& ! [M] :
( ( property1(M,honest,pos)
& person(M) )
=> ~ ? [N] :
( M = N
& property1(N,dishonest,pos) ) )
& ! [K] :
( ( property1(K,healthy,pos)
& person(K) )
=> ~ ? [L] :
( K = L
& property1(L,unhealthy,pos) ) )
& ! [I] :
( ( property1(I,unhealthy,pos)
& cyclist(I) )
=> ? [J] :
( I = J
& property1(J,dishonest,pos) ) )
& ! [G] :
( cyclist(G)
=> ? [H] :
( G = H
& property1(H,industrious,pos) ) )
& ! [E] :
( ( property1(E,industrious,pos)
& grocer(E) )
=> ? [F] :
( E = F
& property1(F,honest,pos) ) )
& ! [C] :
( grocer(C)
=> ~ ? [D] :
( C = D
& property1(D,healthy,pos) ) )
& ! [A] :
( ( property1(A,industrious,pos)
& property1(A,honest,pos)
& person(A) )
=> ? [B] :
( A = B
& property1(B,healthy,pos) ) ) )
=> ! [S] :
( grocer(S)
=> ~ ? [T] :
( S = T
& cyclist(T) ) ) ),
inference(assume_negation,[status(cth)],[prove]) ).
fof(nnf_1,plain,
( ? [S] :
( ? [T] :
( T = S
& cyclist(T) )
& grocer(S) )
& ! [Q] :
( ? [R] :
( R = Q
& person(R) )
| ~ cyclist(Q) )
& ! [O] :
( ? [P] :
( P = O
& person(P) )
| ~ grocer(O) )
& ! [M] :
( ! [N] :
( N != M
| ~ property1(N,dishonest,pos) )
| ~ property1(M,honest,pos)
| ~ person(M) )
& ! [K] :
( ! [L] :
( L != K
| ~ property1(L,unhealthy,pos) )
| ~ property1(K,healthy,pos)
| ~ person(K) )
& ! [I] :
( ? [J] :
( J = I
& property1(J,dishonest,pos) )
| ~ property1(I,unhealthy,pos)
| ~ cyclist(I) )
& ! [G] :
( ? [H] :
( H = G
& property1(H,industrious,pos) )
| ~ cyclist(G) )
& ! [E] :
( ? [F] :
( F = E
& property1(F,honest,pos) )
| ~ property1(E,industrious,pos)
| ~ grocer(E) )
& ! [C] :
( ! [D] :
( D != C
| ~ property1(D,healthy,pos) )
| ~ grocer(C) )
& ! [A] :
( ? [B] :
( B = A
& property1(B,healthy,pos) )
| ~ property1(A,industrious,pos)
| ~ property1(A,honest,pos)
| ~ person(A) ) ),
inference(fof_nnf,[status(thm)],[prove_neg]) ).
fof(sk_prove_neg_sk,plain,
( sK4 = sK2
& cyclist(sK4)
& grocer(sK2)
& ! [Q] :
( ( sK7(Q) = Q
& person(sK7(Q)) )
| ~ cyclist(Q) )
& ! [O] :
( ( sK0(O) = O
& person(sK0(O)) )
| ~ grocer(O) )
& ! [M] :
( ! [N] :
( N != M
| ~ property1(N,dishonest,pos) )
| ~ property1(M,honest,pos)
| ~ person(M) )
& ! [K] :
( ! [L] :
( L != K
| ~ property1(L,unhealthy,pos) )
| ~ property1(K,healthy,pos)
| ~ person(K) )
& ! [I] :
( ( sK6(I) = I
& property1(sK6(I),dishonest,pos) )
| ~ property1(I,unhealthy,pos)
| ~ cyclist(I) )
& ! [G] :
( ( sK5(G) = G
& property1(sK5(G),industrious,pos) )
| ~ cyclist(G) )
& ! [E] :
( ( sK3(E) = E
& property1(sK3(E),honest,pos) )
| ~ property1(E,industrious,pos)
| ~ grocer(E) )
& ! [C] :
( ! [D] :
( D != C
| ~ property1(D,healthy,pos) )
| ~ grocer(C) )
& ! [A] :
( ( sK1(A) = A
& property1(sK1(A),healthy,pos) )
| ~ property1(A,industrious,pos)
| ~ property1(A,honest,pos)
| ~ person(A) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK3,sK5,sK6,sK0,sK7,sK2,sK4]),skolemize(B,sK1(A)),skolemize(F,sK3(E)),skolemize(H,sK5(G)),skolemize(J,sK6(I)),skolemize(P,sK0(O)),skolemize(R,sK7(Q)),skolemize(S,sK2),skolemize(T,sK4)],[nnf_1]) ).
fof(sk_prove_neg,plain,
( sK4 = sK2
& cyclist(sK4)
& grocer(sK2)
& ! [VAR_0] :
( sK7(VAR_0) = VAR_0
| ~ cyclist(VAR_0) )
& ! [VAR_0] :
( person(sK7(VAR_0))
| ~ cyclist(VAR_0) )
& ! [VAR_0] :
( sK0(VAR_0) = VAR_0
| ~ grocer(VAR_0) )
& ! [VAR_0] :
( person(sK0(VAR_0))
| ~ grocer(VAR_0) )
& ! [VAR_0,VAR_1] :
( VAR_1 != VAR_0
| ~ property1(VAR_1,dishonest,pos)
| ~ property1(VAR_0,honest,pos)
| ~ person(VAR_0) )
& ! [VAR_0,VAR_1] :
( VAR_1 != VAR_0
| ~ property1(VAR_1,unhealthy,pos)
| ~ property1(VAR_0,healthy,pos)
| ~ person(VAR_0) )
& ! [VAR_0] :
( sK6(VAR_0) = VAR_0
| ~ property1(VAR_0,unhealthy,pos)
| ~ cyclist(VAR_0) )
& ! [VAR_0] :
( property1(sK6(VAR_0),dishonest,pos)
| ~ property1(VAR_0,unhealthy,pos)
| ~ cyclist(VAR_0) )
& ! [VAR_0] :
( sK5(VAR_0) = VAR_0
| ~ cyclist(VAR_0) )
& ! [VAR_0] :
( property1(sK5(VAR_0),industrious,pos)
| ~ cyclist(VAR_0) )
& ! [VAR_0] :
( sK3(VAR_0) = VAR_0
| ~ property1(VAR_0,industrious,pos)
| ~ grocer(VAR_0) )
& ! [VAR_0] :
( property1(sK3(VAR_0),honest,pos)
| ~ property1(VAR_0,industrious,pos)
| ~ grocer(VAR_0) )
& ! [VAR_0,VAR_1] :
( VAR_1 != VAR_0
| ~ property1(VAR_1,healthy,pos)
| ~ grocer(VAR_0) )
& ! [VAR_0] :
( sK1(VAR_0) = VAR_0
| ~ property1(VAR_0,industrious,pos)
| ~ property1(VAR_0,honest,pos)
| ~ person(VAR_0) )
& ! [VAR_0] :
( property1(sK1(VAR_0),healthy,pos)
| ~ property1(VAR_0,industrious,pos)
| ~ property1(VAR_0,honest,pos)
| ~ person(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_prove_neg_sk]) ).
cnf(c_2,negated_conjecture,
( person(sK0(A))
| ~ grocer(A) ),
inference(split_conjunct,[status(thm)],[sk_prove_neg]) ).
cnf(c_5,negated_conjecture,
( sK1(A) = A
| ~ property1(A,industrious,pos)
| ~ property1(A,honest,pos)
| ~ person(A) ),
inference(split_conjunct,[status(thm)],[sk_prove_neg]) ).
cnf(c_6,negated_conjecture,
( property1(sK1(A),healthy,pos)
| ~ property1(A,industrious,pos)
| ~ property1(A,honest,pos)
| ~ person(A) ),
inference(split_conjunct,[status(thm)],[sk_prove_neg]) ).
cnf(c_8,negated_conjecture,
grocer(sK2),
inference(split_conjunct,[status(thm)],[sk_prove_neg]) ).
cnf(c_11,negated_conjecture,
( sK1(sK0(A)) = sK0(A)
| ~ property1(sK0(A),industrious,pos)
| ~ property1(sK0(A),honest,pos)
| ~ grocer(A) ),
inference(resolve,[status(thm)],[c_2,c_5]) ).
cnf(c_12,negated_conjecture,
( property1(sK1(sK0(A)),healthy,pos)
| ~ property1(sK0(A),industrious,pos)
| ~ property1(sK0(A),honest,pos)
| ~ grocer(A) ),
inference(resolve,[status(thm)],[c_2,c_6]) ).
cnf(c_13,negated_conjecture,
( sK0(A) = A
| ~ grocer(A) ),
inference(split_conjunct,[status(thm)],[sk_prove_neg]) ).
cnf(c_14,negated_conjecture,
( sK3(A) = A
| ~ property1(A,industrious,pos)
| ~ grocer(A) ),
inference(split_conjunct,[status(thm)],[sk_prove_neg]) ).
cnf(c_15,negated_conjecture,
( property1(sK3(A),honest,pos)
| ~ property1(A,industrious,pos)
| ~ grocer(A) ),
inference(split_conjunct,[status(thm)],[sk_prove_neg]) ).
cnf(c_16,negated_conjecture,
( B != A
| ~ property1(B,healthy,pos)
| ~ grocer(A) ),
inference(split_conjunct,[status(thm)],[sk_prove_neg]) ).
cnf(c_17,negated_conjecture,
cyclist(sK4),
inference(split_conjunct,[status(thm)],[sk_prove_neg]) ).
cnf(c_21,negated_conjecture,
( sK5(A) = A
| ~ cyclist(A) ),
inference(split_conjunct,[status(thm)],[sk_prove_neg]) ).
cnf(c_22,negated_conjecture,
( property1(sK5(A),industrious,pos)
| ~ cyclist(A) ),
inference(split_conjunct,[status(thm)],[sk_prove_neg]) ).
cnf(c_33,negated_conjecture,
property1(sK5(sK4),industrious,pos),
inference(resolve,[status(thm)],[c_17,c_22]) ).
cnf(c_34,negated_conjecture,
sK5(sK4) = sK4,
inference(resolve,[status(thm)],[c_17,c_21]) ).
cnf(c_38,negated_conjecture,
sK4 = sK2,
inference(split_conjunct,[status(thm)],[sk_prove_neg]) ).
cnf(c_43,negated_conjecture,
( sK1(sK0(sK2)) = sK0(sK2)
| ~ property1(sK0(sK2),industrious,pos)
| ~ property1(sK0(sK2),honest,pos) ),
inference(resolve,[status(thm)],[c_8,c_11]) ).
cnf(c_44,negated_conjecture,
( property1(sK1(sK0(sK2)),healthy,pos)
| ~ property1(sK0(sK2),industrious,pos)
| ~ property1(sK0(sK2),honest,pos) ),
inference(resolve,[status(thm)],[c_8,c_12]) ).
cnf(c_45,negated_conjecture,
sK0(sK2) = sK2,
inference(resolve,[status(thm)],[c_13,c_8]) ).
cnf(c_46,negated_conjecture,
( sK3(sK2) = sK2
| ~ property1(sK2,industrious,pos) ),
inference(resolve,[status(thm)],[c_14,c_8]) ).
cnf(c_47,negated_conjecture,
( property1(sK3(sK2),honest,pos)
| ~ property1(sK2,industrious,pos) ),
inference(resolve,[status(thm)],[c_15,c_8]) ).
cnf(c_48,negated_conjecture,
( A != sK2
| ~ property1(A,healthy,pos) ),
inference(resolve,[status(thm)],[c_16,c_8]) ).
cnf(c_49,negated_conjecture,
( sK2 != A
| ~ property1(A,healthy,pos) ),
inference(copy,[status(thm)],[c_48]) ).
cnf(c_50,negated_conjecture,
property1(sK5(sK2),industrious,pos),
inference(paramod,[status(thm)],[c_38,c_33]) ).
cnf(c_75,negated_conjecture,
sK5(sK2) = sK4,
inference(paramod,[status(thm)],[c_38,c_34]) ).
cnf(c_58,negated_conjecture,
sK5(sK2) = sK2,
inference(paramod,[status(thm)],[c_38,c_75]) ).
cnf(c_76,negated_conjecture,
( property1(sK1(sK0(sK2)),healthy,pos)
| ~ property1(sK0(sK2),industrious,pos)
| ~ property1(sK2,honest,pos) ),
inference(paramod,[status(thm)],[c_45,c_44]) ).
cnf(c_77,negated_conjecture,
( property1(sK1(sK0(sK2)),healthy,pos)
| ~ property1(sK2,industrious,pos)
| ~ property1(sK2,honest,pos) ),
inference(paramod,[status(thm)],[c_45,c_76]) ).
cnf(c_59,negated_conjecture,
( property1(sK1(sK2),healthy,pos)
| ~ property1(sK2,industrious,pos)
| ~ property1(sK2,honest,pos) ),
inference(paramod,[status(thm)],[c_45,c_77]) ).
cnf(c_78,negated_conjecture,
( sK1(sK0(sK2)) = sK0(sK2)
| ~ property1(sK0(sK2),industrious,pos)
| ~ property1(sK2,honest,pos) ),
inference(paramod,[status(thm)],[c_45,c_43]) ).
cnf(c_79,negated_conjecture,
( sK1(sK0(sK2)) = sK0(sK2)
| ~ property1(sK2,industrious,pos)
| ~ property1(sK2,honest,pos) ),
inference(paramod,[status(thm)],[c_45,c_78]) ).
cnf(c_80,negated_conjecture,
( sK1(sK2) = sK0(sK2)
| ~ property1(sK2,industrious,pos)
| ~ property1(sK2,honest,pos) ),
inference(paramod,[status(thm)],[c_45,c_79]) ).
cnf(c_60,negated_conjecture,
( sK1(sK2) = sK2
| ~ property1(sK2,industrious,pos)
| ~ property1(sK2,honest,pos) ),
inference(paramod,[status(thm)],[c_45,c_80]) ).
cnf(c_63,negated_conjecture,
property1(sK2,industrious,pos),
inference(paramod,[status(thm)],[c_58,c_50]) ).
cnf(c_64,negated_conjecture,
( sK1(sK2) = sK2
| ~ property1(sK2,honest,pos) ),
inference(resolve,[status(thm)],[c_63,c_60]) ).
cnf(c_65,negated_conjecture,
( property1(sK1(sK2),healthy,pos)
| ~ property1(sK2,honest,pos) ),
inference(resolve,[status(thm)],[c_63,c_59]) ).
cnf(c_66,negated_conjecture,
property1(sK3(sK2),honest,pos),
inference(resolve,[status(thm)],[c_63,c_47]) ).
cnf(c_67,negated_conjecture,
sK3(sK2) = sK2,
inference(resolve,[status(thm)],[c_63,c_46]) ).
cnf(c_68,negated_conjecture,
property1(sK2,honest,pos),
inference(paramod,[status(thm)],[c_67,c_66]) ).
cnf(c_69,negated_conjecture,
property1(sK1(sK2),healthy,pos),
inference(resolve,[status(thm)],[c_68,c_65]) ).
cnf(c_70,negated_conjecture,
sK1(sK2) = sK2,
inference(resolve,[status(thm)],[c_68,c_64]) ).
cnf(c_72,negated_conjecture,
property1(sK2,healthy,pos),
inference(paramod,[status(thm)],[c_70,c_69]) ).
cnf(c_81,negated_conjecture,
sK2 = sK0(sK2),
inference(copy,[status(thm)],[c_45]) ).
cnf(c_82,negated_conjecture,
~ property1(sK0(sK2),healthy,pos),
inference(resolve,[status(thm)],[c_49,c_81]) ).
cnf(c_83,negated_conjecture,
~ property1(sK2,healthy,pos),
inference(paramod,[status(thm)],[c_45,c_82]) ).
cnf(c_74,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_72,c_83]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ129+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n026.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 05:20:40 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 158387 was started by sandbox on n026,
% 0.09/0.36 % Sat Sep 26 05:20:40 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.37
% 0.09/0.37 % From the command line: assign(max_seconds, 300).
% 0.09/0.38
% 0.09/0.38 % SZS status Theorem for theBenchmark
% 0.09/0.38
% 0.09/0.38 % Proof 1 at 0.00 (+ 0.00) seconds.
% 0.09/0.38 % Length of proof is 38.
% 0.09/0.38 % Level of proof is 9.
% 0.09/0.38 % Maximum clause weight is 16.000.
% 0.09/0.38 % Given clauses 3.
% 0.09/0.38
% 0.09/0.38 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------