%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : PUZ129+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:32:07 PM UTC 2026
% Result : Theorem 3.45s 0.86s
% Output : Proof 3.45s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 2
% Syntax : Number of formulae : 94 ( 79 unt; 0 def)
% Number of atoms : 256 ( 123 equ)
% Maximal formula atoms : 36 ( 2 avg)
% Number of connectives : 240 ( 78 ~; 58 |; 82 &)
% ( 0 <=>; 22 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 2 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 10 con; 0-4 aty)
% Number of variables : 113 ( 2 sgn 44 !; 28 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f0,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('/export/starexec/sandbox/benchmark/theBenchmark.p',prove) ).
fof(f0_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(negated_conjecture,[status(cth)],[f0]) ).
fof(f0_nnf,plain,
( ? [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(nnf_transformation,[status(thm)],[f0_neg]) ).
fof(f0_sk,plain,
! [A,C,D,E,G,I,K,L,M,N,O,Q] :
( sk6 = sk7
& cyclist(sk7)
& grocer(sk6)
& ( ( Q = sk5(Q)
& person(sk5(Q)) )
| ~ cyclist(Q) )
& ( ( O = sk4(O)
& person(sk4(O)) )
| ~ grocer(O) )
& ( M != N
| ~ property1(N,dishonest,pos)
| ~ property1(M,honest,pos)
| ~ person(M) )
& ( K != L
| ~ property1(L,unhealthy,pos)
| ~ property1(K,healthy,pos)
| ~ person(K) )
& ( ( I = sk3(I)
& property1(sk3(I),dishonest,pos) )
| ~ property1(I,unhealthy,pos)
| ~ cyclist(I) )
& ( ( G = sk2(G)
& property1(sk2(G),industrious,pos) )
| ~ cyclist(G) )
& ( ( E = sk1(E)
& property1(sk1(E),honest,pos) )
| ~ property1(E,industrious,pos)
| ~ grocer(E) )
& ( C != D
| ~ property1(D,healthy,pos)
| ~ grocer(C) )
& ( ( A = sk0(A)
& property1(sk0(A),healthy,pos) )
| ~ property1(A,industrious,pos)
| ~ property1(A,honest,pos)
| ~ person(A) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2,sk3,sk4,sk5,sk6,sk7])],[f0_nnf]) ).
cnf(c2,plain,
( X2 != X3
| ~ property1(X3,healthy,pos)
| ~ grocer(X2) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t20,plain,
ifeq(grocer(X1),true,ifeq(property1(X2,healthy,pos),true,ifeq(X1,X2,false,true),true),true) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t34,plain,
ifeq(grocer(X1),true,ifeq(property1(X2,healthy,pos),true,ifeq(X1,X2,false,true),true),true) = true,
inference(orient,[status(thm)],[t20]) ).
cnf(c0,plain,
( property1(sk0(X0),healthy,pos)
| ~ property1(X0,industrious,pos)
| ~ property1(X0,honest,pos)
| ~ person(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t23,plain,
ifeq(person(X1),true,ifeq(property1(X1,honest,pos),true,ifeq(property1(X1,industrious,pos),true,property1(sk0(X1),healthy,pos),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t28,plain,
ifeq(person(X1),true,ifeq(property1(X1,honest,pos),true,ifeq(property1(X1,industrious,pos),true,property1(sk0(X1),healthy,pos),true),true),true) = true,
inference(orient,[status(thm)],[t23]) ).
cnf(c1,plain,
( X0 = sk0(X0)
| ~ property1(X0,industrious,pos)
| ~ property1(X0,honest,pos)
| ~ person(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t22,plain,
ifeq(person(X1),true,ifeq(property1(X1,honest,pos),true,ifeq(property1(X1,industrious,pos),true,X1,sk0(X1)),sk0(X1)),sk0(X1)) = sk0(X1),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t57,plain,
ifeq(person(X1),true,ifeq(property1(X1,honest,pos),true,ifeq(property1(X1,industrious,pos),true,X1,sk0(X1)),sk0(X1)),sk0(X1)) = sk0(X1),
inference(orient,[status(thm)],[t22]) ).
cnf(c3,plain,
( property1(sk1(X4),honest,pos)
| ~ property1(X4,industrious,pos)
| ~ grocer(X4) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t19,plain,
ifeq(grocer(X1),true,ifeq(property1(X1,industrious,pos),true,property1(sk1(X1),honest,pos),true),true) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t36,plain,
ifeq(grocer(X1),true,ifeq(property1(X1,industrious,pos),true,property1(sk1(X1),honest,pos),true),true) = true,
inference(orient,[status(thm)],[t19]) ).
cnf(c4,plain,
( X4 = sk1(X4)
| ~ property1(X4,industrious,pos)
| ~ grocer(X4) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t17,plain,
ifeq(grocer(X1),true,ifeq(property1(X1,industrious,pos),true,X1,sk1(X1)),sk1(X1)) = sk1(X1),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t69,plain,
ifeq(grocer(X1),true,ifeq(property1(X1,industrious,pos),true,X1,sk1(X1)),sk1(X1)) = sk1(X1),
inference(orient,[status(thm)],[t17]) ).
cnf(c5,plain,
( property1(sk2(X6),industrious,pos)
| ~ cyclist(X6) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t15,plain,
ifeq(cyclist(X1),true,property1(sk2(X1),industrious,pos),true) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t32,plain,
ifeq(cyclist(X1),true,property1(sk2(X1),industrious,pos),true) = true,
inference(orient,[status(thm)],[t15]) ).
cnf(c6,plain,
( X6 = sk2(X6)
| ~ cyclist(X6) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi5,negated_conjecture,
ifeq(cyclist(X0),true,X0,sk2(X0)) = sk2(X0),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(c16,plain,
cyclist(sk7),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi13,negated_conjecture,
cyclist(sk7) = true,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t3,plain,
sk2(sk7) = sk7,
inference(hyper_resolution,[status(thm)],[hi5,hi13]) ).
cnf(t75,plain,
sk2(sk7) = sk7,
inference(orient,[status(thm)],[t3]) ).
cnf(t76,plain,
true = ifeq(cyclist(sk7),true,property1(sk7,industrious,pos),true),
inference(cp,[status(thm)],[t32,t75]) ).
cnf(t1,plain,
cyclist(sk7) = true,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t52,plain,
cyclist(sk7) = true,
inference(orient,[status(thm)],[t1]) ).
cnf(t127,plain,
true = ifeq(true,true,property1(sk7,industrious,pos),true),
inference(step,[status(thm)],[t76,t52]) ).
cnf(t8,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t25,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t8]) ).
cnf(t128,plain,
true = property1(sk7,industrious,pos),
inference(step,[status(thm)],[t127,t25]) ).
cnf(t94,plain,
property1(sk7,industrious,pos) = true,
inference(orient,[status(thm)],[t128]) ).
cnf(t95,plain,
sk1(sk7) = ifeq(grocer(sk7),true,ifeq(true,true,sk7,sk1(sk7)),sk1(sk7)),
inference(cp,[status(thm)],[t69,t94]) ).
cnf(c15,plain,
grocer(sk6),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t2,plain,
grocer(sk6) = true,
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(t54,plain,
grocer(sk6) = true,
inference(orient,[status(thm)],[t2]) ).
cnf(c17,plain,
sk6 = sk7,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t0,plain,
sk7 = sk6,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(t72,plain,
sk6 = sk7,
inference(orient,[status(thm)],[t0]) ).
cnf(t119,plain,
grocer(sk7) = true,
inference(step,[status(thm)],[t54,t72]) ).
cnf(t73,plain,
grocer(sk7) = true,
inference(rw,[status(thm)],[t119]) ).
cnf(t84,plain,
grocer(sk7) = true,
inference(orient,[status(thm)],[t73]) ).
cnf(t129,plain,
sk1(sk7) = ifeq(true,true,ifeq(true,true,sk7,sk1(sk7)),sk1(sk7)),
inference(step,[status(thm)],[t95,t84]) ).
cnf(t130,plain,
sk1(sk7) = ifeq(true,true,sk7,sk1(sk7)),
inference(step,[status(thm)],[t129,t25]) ).
cnf(t131,plain,
sk1(sk7) = sk7,
inference(step,[status(thm)],[t130,t25]) ).
cnf(t99,plain,
sk1(sk7) = sk7,
inference(orient,[status(thm)],[t131]) ).
cnf(t100,plain,
true = ifeq(grocer(sk7),true,ifeq(property1(sk7,industrious,pos),true,property1(sk7,honest,pos),true),true),
inference(cp,[status(thm)],[t36,t99]) ).
cnf(t132,plain,
true = ifeq(true,true,ifeq(property1(sk7,industrious,pos),true,property1(sk7,honest,pos),true),true),
inference(step,[status(thm)],[t100,t84]) ).
cnf(t133,plain,
true = ifeq(property1(sk7,industrious,pos),true,property1(sk7,honest,pos),true),
inference(step,[status(thm)],[t132,t25]) ).
cnf(t134,plain,
true = ifeq(true,true,property1(sk7,honest,pos),true),
inference(step,[status(thm)],[t133,t94]) ).
cnf(t135,plain,
true = property1(sk7,honest,pos),
inference(step,[status(thm)],[t134,t25]) ).
cnf(t101,plain,
property1(sk7,honest,pos) = true,
inference(orient,[status(thm)],[t135]) ).
cnf(t103,plain,
sk0(sk7) = ifeq(person(sk7),true,ifeq(true,true,ifeq(property1(sk7,industrious,pos),true,sk7,sk0(sk7)),sk0(sk7)),sk0(sk7)),
inference(cp,[status(thm)],[t57,t101]) ).
cnf(c13,plain,
( person(sk5(X16))
| ~ cyclist(X16) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t12,plain,
ifeq(cyclist(X1),true,person(sk5(X1)),true) = true,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t33,plain,
ifeq(cyclist(X1),true,person(sk5(X1)),true) = true,
inference(orient,[status(thm)],[t12]) ).
cnf(c14,plain,
( X16 = sk5(X16)
| ~ cyclist(X16) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi11,negated_conjecture,
ifeq(cyclist(X0),true,X0,sk5(X0)) = sk5(X0),
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t5,plain,
sk5(sk7) = sk7,
inference(hyper_resolution,[status(thm)],[hi11,hi13]) ).
cnf(t78,plain,
sk5(sk7) = sk7,
inference(orient,[status(thm)],[t5]) ).
cnf(t79,plain,
true = ifeq(cyclist(sk7),true,person(sk7),true),
inference(cp,[status(thm)],[t33,t78]) ).
cnf(t125,plain,
true = ifeq(true,true,person(sk7),true),
inference(step,[status(thm)],[t79,t52]) ).
cnf(t126,plain,
true = person(sk7),
inference(step,[status(thm)],[t125,t25]) ).
cnf(t89,plain,
person(sk7) = true,
inference(orient,[status(thm)],[t126]) ).
cnf(t136,plain,
sk0(sk7) = ifeq(true,true,ifeq(true,true,ifeq(property1(sk7,industrious,pos),true,sk7,sk0(sk7)),sk0(sk7)),sk0(sk7)),
inference(step,[status(thm)],[t103,t89]) ).
cnf(t137,plain,
sk0(sk7) = ifeq(true,true,ifeq(property1(sk7,industrious,pos),true,sk7,sk0(sk7)),sk0(sk7)),
inference(step,[status(thm)],[t136,t25]) ).
cnf(t138,plain,
sk0(sk7) = ifeq(property1(sk7,industrious,pos),true,sk7,sk0(sk7)),
inference(step,[status(thm)],[t137,t25]) ).
cnf(t139,plain,
sk0(sk7) = ifeq(true,true,sk7,sk0(sk7)),
inference(step,[status(thm)],[t138,t94]) ).
cnf(t140,plain,
sk0(sk7) = sk7,
inference(step,[status(thm)],[t139,t25]) ).
cnf(t105,plain,
sk0(sk7) = sk7,
inference(orient,[status(thm)],[t140]) ).
cnf(t106,plain,
true = ifeq(person(sk7),true,ifeq(property1(sk7,honest,pos),true,ifeq(property1(sk7,industrious,pos),true,property1(sk7,healthy,pos),true),true),true),
inference(cp,[status(thm)],[t28,t105]) ).
cnf(t141,plain,
true = ifeq(true,true,ifeq(property1(sk7,honest,pos),true,ifeq(property1(sk7,industrious,pos),true,property1(sk7,healthy,pos),true),true),true),
inference(step,[status(thm)],[t106,t89]) ).
cnf(t142,plain,
true = ifeq(property1(sk7,honest,pos),true,ifeq(property1(sk7,industrious,pos),true,property1(sk7,healthy,pos),true),true),
inference(step,[status(thm)],[t141,t25]) ).
cnf(t143,plain,
true = ifeq(true,true,ifeq(property1(sk7,industrious,pos),true,property1(sk7,healthy,pos),true),true),
inference(step,[status(thm)],[t142,t101]) ).
cnf(t144,plain,
true = ifeq(property1(sk7,industrious,pos),true,property1(sk7,healthy,pos),true),
inference(step,[status(thm)],[t143,t25]) ).
cnf(t145,plain,
true = ifeq(true,true,property1(sk7,healthy,pos),true),
inference(step,[status(thm)],[t144,t94]) ).
cnf(t146,plain,
true = property1(sk7,healthy,pos),
inference(step,[status(thm)],[t145,t25]) ).
cnf(t107,plain,
property1(sk7,healthy,pos) = true,
inference(orient,[status(thm)],[t146]) ).
cnf(t108,plain,
true = ifeq(grocer(X1),true,ifeq(true,true,ifeq(X1,sk7,false,true),true),true),
inference(cp,[status(thm)],[t34,t107]) ).
cnf(t148,plain,
true = ifeq(grocer(X1),true,ifeq(X1,sk7,false,true),true),
inference(step,[status(thm)],[t108,t25]) ).
cnf(t111,plain,
ifeq(grocer(X1),true,ifeq(X1,sk7,false,true),true) = true,
inference(orient,[status(thm)],[t148]) ).
cnf(t112,plain,
true = ifeq(true,true,ifeq(sk7,sk7,false,true),true),
inference(cp,[status(thm)],[t111,t84]) ).
cnf(t149,plain,
true = ifeq(sk7,sk7,false,true),
inference(step,[status(thm)],[t112,t25]) ).
cnf(t150,plain,
true = false,
inference(step,[status(thm)],[t149,t25]) ).
cnf(t114,plain,
false = true,
inference(orient,[status(thm)],[t150]) ).
cnf(c9,plain,
( X10 != X11
| ~ property1(X11,unhealthy,pos)
| ~ property1(X10,healthy,pos)
| ~ person(X10) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(c10,plain,
( X12 != X13
| ~ property1(X13,dishonest,pos)
| ~ property1(X12,honest,pos)
| ~ person(X12) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c2,c9,c10]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t114]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ129+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n009.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Thu Sep 24 06:59:28 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 3.45/0.86 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.45/0.86 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------