%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : PUZ129+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 08:54:30 AM UTC 2026
% Result : Theorem 204.65s 205.00s
% Output : Proof 205.94s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% 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(f_1_1,negated_conjecture,
( ~ ! [S] :
( grocer(S)
=> ~ ? [T] :
( S = T
& cyclist(T) ) )
& ! [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) ) ) ),
inference(negate,[status(cth)],[prove]) ).
fof(f_1_2,negated_conjecture,
( ? [S] :
( ? [T] :
( S = T
& cyclist(T) )
& grocer(S) )
& ! [Q] :
( ? [R] :
( Q = R
& person(R) )
| ~ cyclist(Q) )
& ! [O] :
( ? [P] :
( O = P
& person(P) )
| ~ grocer(O) )
& ! [M] :
( ! [N] :
( M != N
| ~ property1(N,dishonest,pos) )
| ~ property1(M,honest,pos)
| ~ person(M) )
& ! [K] :
( ! [L] :
( K != L
| ~ property1(L,unhealthy,pos) )
| ~ property1(K,healthy,pos)
| ~ person(K) )
& ! [I] :
( ? [J] :
( I = J
& property1(J,dishonest,pos) )
| ~ property1(I,unhealthy,pos)
| ~ cyclist(I) )
& ! [G] :
( ? [H] :
( G = H
& property1(H,industrious,pos) )
| ~ cyclist(G) )
& ! [E] :
( ? [F] :
( E = F
& property1(F,honest,pos) )
| ~ property1(E,industrious,pos)
| ~ grocer(E) )
& ! [C] :
( ! [D] :
( C != D
| ~ property1(D,healthy,pos) )
| ~ grocer(C) )
& ! [A] :
( ? [B] :
( A = B
& property1(B,healthy,pos) )
| ~ property1(A,industrious,pos)
| ~ property1(A,honest,pos)
| ~ person(A) ) ),
inference(fof_nnf,[status(thm)],[f_1_1]) ).
fof(f_1_3,negated_conjecture,
( ? [U_19] :
( ? [U_18] :
( U_19 = U_18
& cyclist(U_18) )
& grocer(U_19) )
& ! [U_17] :
( ? [U_16] :
( U_17 = U_16
& person(U_16) )
| ~ cyclist(U_17) )
& ! [U_15] :
( ? [U_14] :
( U_15 = U_14
& person(U_14) )
| ~ grocer(U_15) )
& ! [U_13] :
( ! [U_12] :
( U_13 != U_12
| ~ property1(U_12,dishonest,pos) )
| ~ property1(U_13,honest,pos)
| ~ person(U_13) )
& ! [U_11] :
( ! [U_10] :
( U_11 != U_10
| ~ property1(U_10,unhealthy,pos) )
| ~ property1(U_11,healthy,pos)
| ~ person(U_11) )
& ! [U_9] :
( ? [U_8] :
( U_9 = U_8
& property1(U_8,dishonest,pos) )
| ~ property1(U_9,unhealthy,pos)
| ~ cyclist(U_9) )
& ! [U_7] :
( ? [U_6] :
( U_7 = U_6
& property1(U_6,industrious,pos) )
| ~ cyclist(U_7) )
& ! [U_5] :
( ? [U_4] :
( U_5 = U_4
& property1(U_4,honest,pos) )
| ~ property1(U_5,industrious,pos)
| ~ grocer(U_5) )
& ! [U_3] :
( ! [U_2] :
( U_3 != U_2
| ~ property1(U_2,healthy,pos) )
| ~ grocer(U_3) )
& ! [U_1] :
( ? [U_0] :
( U_1 = U_0
& property1(U_0,healthy,pos) )
| ~ property1(U_1,industrious,pos)
| ~ property1(U_1,honest,pos)
| ~ person(U_1) ) ),
inference(variable_rename,[status(thm)],[f_1_2]) ).
fof(f_1_4,negated_conjecture,
( ? [U_19] :
( ? [U_18] :
( U_19 = U_18
& cyclist(U_18) )
& grocer(U_19) )
& ! [U_17] :
( ? [U_16] :
( U_17 = U_16
& person(U_16) )
| ~ cyclist(U_17) )
& ! [U_15] :
( ? [U_14] :
( U_15 = U_14
& person(U_14) )
| ~ grocer(U_15) )
& ! [U_13] :
( ! [U_12] :
( U_13 != U_12
| ~ property1(U_12,dishonest,pos) )
| ~ property1(U_13,honest,pos)
| ~ person(U_13) )
& ! [U_11] :
( ! [U_10] :
( U_11 != U_10
| ~ property1(U_10,unhealthy,pos) )
| ~ property1(U_11,healthy,pos)
| ~ person(U_11) )
& ! [U_9] :
( ? [U_8] :
( U_9 = U_8
& property1(U_8,dishonest,pos) )
| ~ property1(U_9,unhealthy,pos)
| ~ cyclist(U_9) )
& ! [U_7] :
( ? [U_6] :
( U_7 = U_6
& property1(U_6,industrious,pos) )
| ~ cyclist(U_7) )
& ! [U_5] :
( ? [U_4] :
( U_5 = U_4
& property1(U_4,honest,pos) )
| ~ property1(U_5,industrious,pos)
| ~ grocer(U_5) )
& ! [U_3] :
( ! [U_2] :
( U_3 != U_2
| ~ property1(U_2,healthy,pos) )
| ~ grocer(U_3) )
& ! [U_1] :
( ( U_1 = sK1(U_1)
& property1(sK1(U_1),healthy,pos) )
| ~ property1(U_1,industrious,pos)
| ~ property1(U_1,honest,pos)
| ~ person(U_1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_0,sK1(U_1))],[f_1_3]) ).
fof(f_1_5,negated_conjecture,
( ? [U_19] :
( ? [U_18] :
( U_19 = U_18
& cyclist(U_18) )
& grocer(U_19) )
& ! [U_17] :
( ? [U_16] :
( U_17 = U_16
& person(U_16) )
| ~ cyclist(U_17) )
& ! [U_15] :
( ? [U_14] :
( U_15 = U_14
& person(U_14) )
| ~ grocer(U_15) )
& ! [U_13] :
( ! [U_12] :
( U_13 != U_12
| ~ property1(U_12,dishonest,pos) )
| ~ property1(U_13,honest,pos)
| ~ person(U_13) )
& ! [U_11] :
( ! [U_10] :
( U_11 != U_10
| ~ property1(U_10,unhealthy,pos) )
| ~ property1(U_11,healthy,pos)
| ~ person(U_11) )
& ! [U_9] :
( ? [U_8] :
( U_9 = U_8
& property1(U_8,dishonest,pos) )
| ~ property1(U_9,unhealthy,pos)
| ~ cyclist(U_9) )
& ! [U_7] :
( ? [U_6] :
( U_7 = U_6
& property1(U_6,industrious,pos) )
| ~ cyclist(U_7) )
& ! [U_5] :
( ( U_5 = sK2(U_5)
& property1(sK2(U_5),honest,pos) )
| ~ property1(U_5,industrious,pos)
| ~ grocer(U_5) )
& ! [U_3] :
( ! [U_2] :
( U_3 != U_2
| ~ property1(U_2,healthy,pos) )
| ~ grocer(U_3) )
& ! [U_1] :
( ( U_1 = sK1(U_1)
& property1(sK1(U_1),healthy,pos) )
| ~ property1(U_1,industrious,pos)
| ~ property1(U_1,honest,pos)
| ~ person(U_1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_4,sK2(U_5))],[f_1_4]) ).
fof(f_1_6,negated_conjecture,
( ? [U_19] :
( ? [U_18] :
( U_19 = U_18
& cyclist(U_18) )
& grocer(U_19) )
& ! [U_17] :
( ? [U_16] :
( U_17 = U_16
& person(U_16) )
| ~ cyclist(U_17) )
& ! [U_15] :
( ? [U_14] :
( U_15 = U_14
& person(U_14) )
| ~ grocer(U_15) )
& ! [U_13] :
( ! [U_12] :
( U_13 != U_12
| ~ property1(U_12,dishonest,pos) )
| ~ property1(U_13,honest,pos)
| ~ person(U_13) )
& ! [U_11] :
( ! [U_10] :
( U_11 != U_10
| ~ property1(U_10,unhealthy,pos) )
| ~ property1(U_11,healthy,pos)
| ~ person(U_11) )
& ! [U_9] :
( ? [U_8] :
( U_9 = U_8
& property1(U_8,dishonest,pos) )
| ~ property1(U_9,unhealthy,pos)
| ~ cyclist(U_9) )
& ! [U_7] :
( ( U_7 = sK3(U_7)
& property1(sK3(U_7),industrious,pos) )
| ~ cyclist(U_7) )
& ! [U_5] :
( ( U_5 = sK2(U_5)
& property1(sK2(U_5),honest,pos) )
| ~ property1(U_5,industrious,pos)
| ~ grocer(U_5) )
& ! [U_3] :
( ! [U_2] :
( U_3 != U_2
| ~ property1(U_2,healthy,pos) )
| ~ grocer(U_3) )
& ! [U_1] :
( ( U_1 = sK1(U_1)
& property1(sK1(U_1),healthy,pos) )
| ~ property1(U_1,industrious,pos)
| ~ property1(U_1,honest,pos)
| ~ person(U_1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_6,sK3(U_7))],[f_1_5]) ).
fof(f_1_7,negated_conjecture,
( ? [U_19] :
( ? [U_18] :
( U_19 = U_18
& cyclist(U_18) )
& grocer(U_19) )
& ! [U_17] :
( ? [U_16] :
( U_17 = U_16
& person(U_16) )
| ~ cyclist(U_17) )
& ! [U_15] :
( ? [U_14] :
( U_15 = U_14
& person(U_14) )
| ~ grocer(U_15) )
& ! [U_13] :
( ! [U_12] :
( U_13 != U_12
| ~ property1(U_12,dishonest,pos) )
| ~ property1(U_13,honest,pos)
| ~ person(U_13) )
& ! [U_11] :
( ! [U_10] :
( U_11 != U_10
| ~ property1(U_10,unhealthy,pos) )
| ~ property1(U_11,healthy,pos)
| ~ person(U_11) )
& ! [U_9] :
( ( U_9 = sK4(U_9)
& property1(sK4(U_9),dishonest,pos) )
| ~ property1(U_9,unhealthy,pos)
| ~ cyclist(U_9) )
& ! [U_7] :
( ( U_7 = sK3(U_7)
& property1(sK3(U_7),industrious,pos) )
| ~ cyclist(U_7) )
& ! [U_5] :
( ( U_5 = sK2(U_5)
& property1(sK2(U_5),honest,pos) )
| ~ property1(U_5,industrious,pos)
| ~ grocer(U_5) )
& ! [U_3] :
( ! [U_2] :
( U_3 != U_2
| ~ property1(U_2,healthy,pos) )
| ~ grocer(U_3) )
& ! [U_1] :
( ( U_1 = sK1(U_1)
& property1(sK1(U_1),healthy,pos) )
| ~ property1(U_1,industrious,pos)
| ~ property1(U_1,honest,pos)
| ~ person(U_1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_8,sK4(U_9))],[f_1_6]) ).
fof(f_1_8,negated_conjecture,
( ? [U_19] :
( ? [U_18] :
( U_19 = U_18
& cyclist(U_18) )
& grocer(U_19) )
& ! [U_17] :
( ? [U_16] :
( U_17 = U_16
& person(U_16) )
| ~ cyclist(U_17) )
& ! [U_15] :
( ( U_15 = sK5(U_15)
& person(sK5(U_15)) )
| ~ grocer(U_15) )
& ! [U_13] :
( ! [U_12] :
( U_13 != U_12
| ~ property1(U_12,dishonest,pos) )
| ~ property1(U_13,honest,pos)
| ~ person(U_13) )
& ! [U_11] :
( ! [U_10] :
( U_11 != U_10
| ~ property1(U_10,unhealthy,pos) )
| ~ property1(U_11,healthy,pos)
| ~ person(U_11) )
& ! [U_9] :
( ( U_9 = sK4(U_9)
& property1(sK4(U_9),dishonest,pos) )
| ~ property1(U_9,unhealthy,pos)
| ~ cyclist(U_9) )
& ! [U_7] :
( ( U_7 = sK3(U_7)
& property1(sK3(U_7),industrious,pos) )
| ~ cyclist(U_7) )
& ! [U_5] :
( ( U_5 = sK2(U_5)
& property1(sK2(U_5),honest,pos) )
| ~ property1(U_5,industrious,pos)
| ~ grocer(U_5) )
& ! [U_3] :
( ! [U_2] :
( U_3 != U_2
| ~ property1(U_2,healthy,pos) )
| ~ grocer(U_3) )
& ! [U_1] :
( ( U_1 = sK1(U_1)
& property1(sK1(U_1),healthy,pos) )
| ~ property1(U_1,industrious,pos)
| ~ property1(U_1,honest,pos)
| ~ person(U_1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_14,sK5(U_15))],[f_1_7]) ).
fof(f_1_9,negated_conjecture,
( ? [U_19] :
( ? [U_18] :
( U_19 = U_18
& cyclist(U_18) )
& grocer(U_19) )
& ! [U_17] :
( ( U_17 = sK6(U_17)
& person(sK6(U_17)) )
| ~ cyclist(U_17) )
& ! [U_15] :
( ( U_15 = sK5(U_15)
& person(sK5(U_15)) )
| ~ grocer(U_15) )
& ! [U_13] :
( ! [U_12] :
( U_13 != U_12
| ~ property1(U_12,dishonest,pos) )
| ~ property1(U_13,honest,pos)
| ~ person(U_13) )
& ! [U_11] :
( ! [U_10] :
( U_11 != U_10
| ~ property1(U_10,unhealthy,pos) )
| ~ property1(U_11,healthy,pos)
| ~ person(U_11) )
& ! [U_9] :
( ( U_9 = sK4(U_9)
& property1(sK4(U_9),dishonest,pos) )
| ~ property1(U_9,unhealthy,pos)
| ~ cyclist(U_9) )
& ! [U_7] :
( ( U_7 = sK3(U_7)
& property1(sK3(U_7),industrious,pos) )
| ~ cyclist(U_7) )
& ! [U_5] :
( ( U_5 = sK2(U_5)
& property1(sK2(U_5),honest,pos) )
| ~ property1(U_5,industrious,pos)
| ~ grocer(U_5) )
& ! [U_3] :
( ! [U_2] :
( U_3 != U_2
| ~ property1(U_2,healthy,pos) )
| ~ grocer(U_3) )
& ! [U_1] :
( ( U_1 = sK1(U_1)
& property1(sK1(U_1),healthy,pos) )
| ~ property1(U_1,industrious,pos)
| ~ property1(U_1,honest,pos)
| ~ person(U_1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_16,sK6(U_17))],[f_1_8]) ).
fof(f_1_10,negated_conjecture,
( ? [U_18] :
( sK7 = U_18
& cyclist(U_18) )
& grocer(sK7)
& ! [U_17] :
( ( U_17 = sK6(U_17)
& person(sK6(U_17)) )
| ~ cyclist(U_17) )
& ! [U_15] :
( ( U_15 = sK5(U_15)
& person(sK5(U_15)) )
| ~ grocer(U_15) )
& ! [U_13] :
( ! [U_12] :
( U_13 != U_12
| ~ property1(U_12,dishonest,pos) )
| ~ property1(U_13,honest,pos)
| ~ person(U_13) )
& ! [U_11] :
( ! [U_10] :
( U_11 != U_10
| ~ property1(U_10,unhealthy,pos) )
| ~ property1(U_11,healthy,pos)
| ~ person(U_11) )
& ! [U_9] :
( ( U_9 = sK4(U_9)
& property1(sK4(U_9),dishonest,pos) )
| ~ property1(U_9,unhealthy,pos)
| ~ cyclist(U_9) )
& ! [U_7] :
( ( U_7 = sK3(U_7)
& property1(sK3(U_7),industrious,pos) )
| ~ cyclist(U_7) )
& ! [U_5] :
( ( U_5 = sK2(U_5)
& property1(sK2(U_5),honest,pos) )
| ~ property1(U_5,industrious,pos)
| ~ grocer(U_5) )
& ! [U_3] :
( ! [U_2] :
( U_3 != U_2
| ~ property1(U_2,healthy,pos) )
| ~ grocer(U_3) )
& ! [U_1] :
( ( U_1 = sK1(U_1)
& property1(sK1(U_1),healthy,pos) )
| ~ property1(U_1,industrious,pos)
| ~ property1(U_1,honest,pos)
| ~ person(U_1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_19,sK7)],[f_1_9]) ).
fof(f_1_11,negated_conjecture,
( sK7 = sK8
& cyclist(sK8)
& grocer(sK7)
& ! [U_17] :
( ( U_17 = sK6(U_17)
& person(sK6(U_17)) )
| ~ cyclist(U_17) )
& ! [U_15] :
( ( U_15 = sK5(U_15)
& person(sK5(U_15)) )
| ~ grocer(U_15) )
& ! [U_13] :
( ! [U_12] :
( U_13 != U_12
| ~ property1(U_12,dishonest,pos) )
| ~ property1(U_13,honest,pos)
| ~ person(U_13) )
& ! [U_11] :
( ! [U_10] :
( U_11 != U_10
| ~ property1(U_10,unhealthy,pos) )
| ~ property1(U_11,healthy,pos)
| ~ person(U_11) )
& ! [U_9] :
( ( U_9 = sK4(U_9)
& property1(sK4(U_9),dishonest,pos) )
| ~ property1(U_9,unhealthy,pos)
| ~ cyclist(U_9) )
& ! [U_7] :
( ( U_7 = sK3(U_7)
& property1(sK3(U_7),industrious,pos) )
| ~ cyclist(U_7) )
& ! [U_5] :
( ( U_5 = sK2(U_5)
& property1(sK2(U_5),honest,pos) )
| ~ property1(U_5,industrious,pos)
| ~ grocer(U_5) )
& ! [U_3] :
( ! [U_2] :
( U_3 != U_2
| ~ property1(U_2,healthy,pos) )
| ~ grocer(U_3) )
& ! [U_1] :
( ( U_1 = sK1(U_1)
& property1(sK1(U_1),healthy,pos) )
| ~ property1(U_1,industrious,pos)
| ~ property1(U_1,honest,pos)
| ~ person(U_1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_18,sK8)],[f_1_10]) ).
fof(f_1_12,negated_conjecture,
( ! [U_17] :
( U_17 = sK6(U_17)
| ~ sP5(U_17) )
& ! [U_17] :
( person(sK6(U_17))
| ~ sP5(U_17) )
& ! [U_15] :
( U_15 = sK5(U_15)
| ~ sP4(U_15) )
& ! [U_15] :
( person(sK5(U_15))
| ~ sP4(U_15) )
& ! [U_9] :
( U_9 = sK4(U_9)
| ~ sP3(U_9) )
& ! [U_9] :
( property1(sK4(U_9),dishonest,pos)
| ~ sP3(U_9) )
& ! [U_7] :
( U_7 = sK3(U_7)
| ~ sP2(U_7) )
& ! [U_7] :
( property1(sK3(U_7),industrious,pos)
| ~ sP2(U_7) )
& ! [U_5] :
( U_5 = sK2(U_5)
| ~ sP1(U_5) )
& ! [U_5] :
( property1(sK2(U_5),honest,pos)
| ~ sP1(U_5) )
& ! [U_1] :
( U_1 = sK1(U_1)
| ~ sP0(U_1) )
& ! [U_1] :
( property1(sK1(U_1),healthy,pos)
| ~ sP0(U_1) )
& sK7 = sK8
& cyclist(sK8)
& grocer(sK7)
& ! [U_17] :
( sP5(U_17)
| ~ cyclist(U_17) )
& ! [U_15] :
( sP4(U_15)
| ~ grocer(U_15) )
& ! [U_13,U_12] :
( U_13 != U_12
| ~ property1(U_12,dishonest,pos)
| ~ property1(U_13,honest,pos)
| ~ person(U_13) )
& ! [U_11,U_10] :
( U_11 != U_10
| ~ property1(U_10,unhealthy,pos)
| ~ property1(U_11,healthy,pos)
| ~ person(U_11) )
& ! [U_9] :
( sP3(U_9)
| ~ property1(U_9,unhealthy,pos)
| ~ cyclist(U_9) )
& ! [U_7] :
( sP2(U_7)
| ~ cyclist(U_7) )
& ! [U_5] :
( sP1(U_5)
| ~ property1(U_5,industrious,pos)
| ~ grocer(U_5) )
& ! [U_3,U_2] :
( U_3 != U_2
| ~ property1(U_2,healthy,pos)
| ~ grocer(U_3) )
& ! [U_1] :
( sP0(U_1)
| ~ property1(U_1,industrious,pos)
| ~ property1(U_1,honest,pos)
| ~ person(U_1) ) ),
inference(definitional_conversion,[status(esa),new_symbols(definitional,[sP0,sP1,sP2,sP3,sP4,sP5])],[f_1_11]) ).
cnf(f_1_13,negated_conjecture,
( sP0(U_1)
| ~ property1(U_1,industrious,pos)
| ~ property1(U_1,honest,pos)
| ~ person(U_1) ),
inference(clausify,[status(thm)],[f_1_12]) ).
cnf(f_1_14,negated_conjecture,
( U_3 != U_2
| ~ property1(U_2,healthy,pos)
| ~ grocer(U_3) ),
inference(clausify,[status(thm)],[f_1_12]) ).
cnf(f_1_15,negated_conjecture,
( sP1(U_5)
| ~ property1(U_5,industrious,pos)
| ~ grocer(U_5) ),
inference(clausify,[status(thm)],[f_1_12]) ).
cnf(f_1_16,negated_conjecture,
( sP2(U_7)
| ~ cyclist(U_7) ),
inference(clausify,[status(thm)],[f_1_12]) ).
cnf(f_1_17,negated_conjecture,
( sP3(U_9)
| ~ property1(U_9,unhealthy,pos)
| ~ cyclist(U_9) ),
inference(clausify,[status(thm)],[f_1_12]) ).
cnf(f_1_18,negated_conjecture,
( U_11 != U_10
| ~ property1(U_10,unhealthy,pos)
| ~ property1(U_11,healthy,pos)
| ~ person(U_11) ),
inference(clausify,[status(thm)],[f_1_12]) ).
cnf(f_1_19,negated_conjecture,
( U_13 != U_12
| ~ property1(U_12,dishonest,pos)
| ~ property1(U_13,honest,pos)
| ~ person(U_13) ),
inference(clausify,[status(thm)],[f_1_12]) ).
cnf(f_1_20,negated_conjecture,
( sP4(U_15)
| ~ grocer(U_15) ),
inference(clausify,[status(thm)],[f_1_12]) ).
cnf(f_1_21,negated_conjecture,
( sP5(U_17)
| ~ cyclist(U_17) ),
inference(clausify,[status(thm)],[f_1_12]) ).
cnf(f_1_22,negated_conjecture,
grocer(sK7),
inference(clausify,[status(thm)],[f_1_12]) ).
cnf(f_1_23,negated_conjecture,
cyclist(sK8),
inference(clausify,[status(thm)],[f_1_12]) ).
cnf(f_1_24,negated_conjecture,
sK7 = sK8,
inference(clausify,[status(thm)],[f_1_12]) ).
cnf(f_1_25,negated_conjecture,
( property1(sK1(U_1),healthy,pos)
| ~ sP0(U_1) ),
inference(clausify,[status(thm)],[f_1_12]) ).
cnf(f_1_26,negated_conjecture,
( U_1 = sK1(U_1)
| ~ sP0(U_1) ),
inference(clausify,[status(thm)],[f_1_12]) ).
cnf(f_1_27,negated_conjecture,
( property1(sK2(U_5),honest,pos)
| ~ sP1(U_5) ),
inference(clausify,[status(thm)],[f_1_12]) ).
cnf(f_1_28,negated_conjecture,
( U_5 = sK2(U_5)
| ~ sP1(U_5) ),
inference(clausify,[status(thm)],[f_1_12]) ).
cnf(f_1_29,negated_conjecture,
( property1(sK3(U_7),industrious,pos)
| ~ sP2(U_7) ),
inference(clausify,[status(thm)],[f_1_12]) ).
cnf(f_1_30,negated_conjecture,
( U_7 = sK3(U_7)
| ~ sP2(U_7) ),
inference(clausify,[status(thm)],[f_1_12]) ).
cnf(f_1_31,negated_conjecture,
( property1(sK4(U_9),dishonest,pos)
| ~ sP3(U_9) ),
inference(clausify,[status(thm)],[f_1_12]) ).
cnf(f_1_32,negated_conjecture,
( U_9 = sK4(U_9)
| ~ sP3(U_9) ),
inference(clausify,[status(thm)],[f_1_12]) ).
cnf(f_1_33,negated_conjecture,
( person(sK5(U_15))
| ~ sP4(U_15) ),
inference(clausify,[status(thm)],[f_1_12]) ).
cnf(f_1_34,negated_conjecture,
( U_15 = sK5(U_15)
| ~ sP4(U_15) ),
inference(clausify,[status(thm)],[f_1_12]) ).
cnf(f_1_35,negated_conjecture,
( person(sK6(U_17))
| ~ sP5(U_17) ),
inference(clausify,[status(thm)],[f_1_12]) ).
cnf(f_1_36,negated_conjecture,
( U_17 = sK6(U_17)
| ~ sP5(U_17) ),
inference(clausify,[status(thm)],[f_1_12]) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( sK1(Eq_x_0) = sK1(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( sK2(Eq_x_0) = sK2(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( sK3(Eq_x_0) = sK3(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( sK4(Eq_x_0) = sK4(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( sK5(Eq_x_0) = sK5(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( sK6(Eq_x_0) = sK6(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_10,axiom,
( person(Eq_y_0)
| ~ person(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_11,axiom,
( property1(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ property1(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_12,axiom,
( grocer(Eq_y_0)
| ~ grocer(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_13,axiom,
( cyclist(Eq_y_0)
| ~ cyclist(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_14,axiom,
( sP0(Eq_y_0)
| ~ sP0(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_15,axiom,
( sP1(Eq_y_0)
| ~ sP1(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_16,axiom,
( sP2(Eq_y_0)
| ~ sP2(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_17,axiom,
( sP3(Eq_y_0)
| ~ sP3(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_18,axiom,
( sP4(Eq_y_0)
| ~ sP4(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_19,axiom,
( sP5(Eq_y_0)
| ~ sP5(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ129+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 This is a FOF_THM_RFO_SEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n014.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sat Sep 19 20:04:35 UTC 2026
% 0.11/0.37 % CPUTime :
% 204.65/205.00 % SZS status Theorem for theBenchmark
% 204.65/205.00 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------