%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYN549+1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n020.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 03:35:10 PM UTC 2026
% Result : Theorem 41.13s 5.68s
% Output : Proof 41.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 75
% Number of leaves : 3
% Syntax : Number of formulae : 146 ( 10 unt; 0 def)
% Number of atoms : 577 ( 0 equ)
% Maximal formula atoms : 18 ( 3 avg)
% Number of connectives : 573 ( 142 ~; 397 |; 29 &)
% ( 2 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 1 con; 0-1 aty)
% Number of variables : 91 ( 0 sgn 23 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X,Y,Z] :
( ( reachable(Y,Z)
& reachable(X,Y) )
=> reachable(X,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity_of_reachable) ).
fof(f1_nnf,plain,
! [X,Y,Z] :
( reachable(X,Z)
| ~ reachable(Y,Z)
| ~ reachable(X,Y) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Y,Z] :
( reachable(X,Z)
| ~ reachable(Y,Z)
| ~ reachable(X,Y) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( reachable(X0,X2)
| ~ reachable(X1,X2)
| ~ reachable(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
fof(f0,axiom,
! [X] : reachable(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_of_reachable) ).
fof(f0_nnf,plain,
! [X] : reachable(X,X),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X] : reachable(X,X),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
reachable(X0,X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
fof(f2,conjecture,
? [X] :
( ! [Y] :
( reachable(X,Y)
=> ( ? [Z] :
( ( ? [V] :
( q(V)
& reachable(Z,V) )
| p(Z) )
& reachable(Y,Z) )
<=> ( ? [W] :
( q(W)
& reachable(Y,W) )
| ? [W] :
( p(W)
& reachable(Y,W) ) ) ) )
& reachable(initial_world,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this) ).
fof(f2_neg,negated_conjecture,
~ ? [X] :
( ! [Y] :
( reachable(X,Y)
=> ( ? [Z] :
( ( ? [V] :
( q(V)
& reachable(Z,V) )
| p(Z) )
& reachable(Y,Z) )
<=> ( ? [W] :
( q(W)
& reachable(Y,W) )
| ? [W] :
( p(W)
& reachable(Y,W) ) ) ) )
& reachable(initial_world,X) ),
inference(negated_conjecture,[status(cth)],[f2]) ).
fof(f2_nnf,plain,
! [X] :
( ? [Y] :
( ( ( ( ? [W] :
( q(W)
& reachable(Y,W) )
| ? [W] :
( p(W)
& reachable(Y,W) ) )
& ! [Z] :
( ( ! [V] :
( ~ q(V)
| ~ reachable(Z,V) )
& ~ p(Z) )
| ~ reachable(Y,Z) ) )
| ( ! [W] :
( ~ q(W)
| ~ reachable(Y,W) )
& ! [W] :
( ~ p(W)
| ~ reachable(Y,W) )
& ? [Z] :
( ( ? [V] :
( q(V)
& reachable(Z,V) )
| p(Z) )
& reachable(Y,Z) ) ) )
& reachable(X,Y) )
| ~ reachable(initial_world,X) ),
inference(nnf_transformation,[status(thm)],[f2_neg]) ).
fof(f2_sk,plain,
! [X,W,Z,V] :
( ( ( ( ( ( q(sk4(X))
& reachable(sk0(X),sk4(X)) )
| ( p(sk3(X))
& reachable(sk0(X),sk3(X)) ) )
& ( ( ( ~ q(V)
| ~ reachable(Z,V) )
& ~ p(Z) )
| ~ reachable(sk0(X),Z) ) )
| ( ( ~ q(W)
| ~ reachable(sk0(X),W) )
& ( ~ p(W)
| ~ reachable(sk0(X),W) )
& ( ( q(sk2(X))
& reachable(sk1(X),sk2(X)) )
| p(sk1(X)) )
& reachable(sk0(X),sk1(X)) ) )
& reachable(X,sk0(X)) )
| ~ reachable(initial_world,X) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2,sk3,sk4])],[f2_nnf]) ).
cnf(c8,plain,
( q(sk4(X0))
| p(sk3(X0))
| reachable(sk0(X0),sk1(X0))
| ~ reachable(initial_world,X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p53,plain,
( q(sk4(initial_world))
| p(sk3(initial_world))
| reachable(sk0(initial_world),sk1(initial_world)) ),
inference(resolution,[status(thm)],[c0,c8]) ).
cnf(p387,plain,
( q(sk4(initial_world))
| p(sk3(initial_world))
| reachable(sk0(initial_world),X0)
| ~ reachable(sk1(initial_world),X0) ),
inference(resolution,[status(thm)],[c1,p53]) ).
cnf(c14,plain,
( q(sk4(X0))
| p(sk3(X0))
| reachable(sk1(X0),sk2(X0))
| p(sk1(X0))
| ~ reachable(initial_world,X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p62,plain,
( q(sk4(initial_world))
| p(sk3(initial_world))
| reachable(sk1(initial_world),sk2(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[c0,c14]) ).
cnf(p1060,plain,
( q(sk4(initial_world))
| p(sk3(initial_world))
| p(sk1(initial_world))
| q(sk4(initial_world))
| p(sk3(initial_world))
| reachable(sk0(initial_world),sk2(initial_world)) ),
inference(resolution,[status(thm)],[p387,p62]) ).
cnf(p3406,plain,
( q(sk4(initial_world))
| p(sk1(initial_world))
| q(sk4(initial_world))
| p(sk3(initial_world))
| reachable(sk0(initial_world),sk2(initial_world)) ),
inference(factoring,[status(thm)],[p1060]) ).
cnf(p3408,plain,
( p(sk1(initial_world))
| q(sk4(initial_world))
| p(sk3(initial_world))
| reachable(sk0(initial_world),sk2(initial_world)) ),
inference(factoring,[status(thm)],[p3406]) ).
cnf(c32,plain,
( q(sk4(X0))
| p(sk3(X0))
| ~ q(X4)
| ~ reachable(sk0(X0),X4)
| ~ reachable(initial_world,X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p58,plain,
( q(sk4(initial_world))
| p(sk3(initial_world))
| ~ q(X0)
| ~ reachable(sk0(initial_world),X0) ),
inference(resolution,[status(thm)],[c0,c32]) ).
cnf(p3413,plain,
( q(sk4(initial_world))
| p(sk3(initial_world))
| ~ q(sk2(initial_world))
| p(sk1(initial_world))
| q(sk4(initial_world))
| p(sk3(initial_world)) ),
inference(resolution,[status(thm)],[p3408,p58]) ).
cnf(p3424,plain,
( q(sk4(initial_world))
| ~ q(sk2(initial_world))
| p(sk1(initial_world))
| q(sk4(initial_world))
| p(sk3(initial_world)) ),
inference(factoring,[status(thm)],[p3413]) ).
cnf(p3426,plain,
( ~ q(sk2(initial_world))
| p(sk1(initial_world))
| q(sk4(initial_world))
| p(sk3(initial_world)) ),
inference(factoring,[status(thm)],[p3424]) ).
cnf(c16,plain,
( ~ q(X3)
| ~ reachable(X2,X3)
| ~ reachable(sk0(X0),X2)
| q(sk2(X0))
| p(sk1(X0))
| ~ reachable(initial_world,X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p69,plain,
( ~ q(X1)
| ~ reachable(X0,X1)
| ~ reachable(sk0(initial_world),X0)
| q(sk2(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[c0,c16]) ).
cnf(p167,plain,
( ~ q(X0)
| ~ reachable(sk0(initial_world),X0)
| q(sk2(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p69,c0]) ).
cnf(c19,plain,
( reachable(sk0(X0),sk4(X0))
| p(sk3(X0))
| q(sk2(X0))
| p(sk1(X0))
| ~ reachable(initial_world,X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p64,plain,
( reachable(sk0(initial_world),sk4(initial_world))
| p(sk3(initial_world))
| q(sk2(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[c0,c19]) ).
cnf(p174,plain,
( p(sk3(initial_world))
| q(sk2(initial_world))
| p(sk1(initial_world))
| ~ q(sk4(initial_world))
| q(sk2(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p167,p64]) ).
cnf(p280,plain,
( p(sk3(initial_world))
| q(sk2(initial_world))
| ~ q(sk4(initial_world))
| q(sk2(initial_world))
| p(sk1(initial_world)) ),
inference(factoring,[status(thm)],[p174]) ).
cnf(p282,plain,
( p(sk3(initial_world))
| ~ q(sk4(initial_world))
| q(sk2(initial_world))
| p(sk1(initial_world)) ),
inference(factoring,[status(thm)],[p280]) ).
cnf(c20,plain,
( q(sk4(X0))
| p(sk3(X0))
| q(sk2(X0))
| p(sk1(X0))
| ~ reachable(initial_world,X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p56,plain,
( q(sk4(initial_world))
| p(sk3(initial_world))
| q(sk2(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[c0,c20]) ).
cnf(p283,plain,
( p(sk3(initial_world))
| q(sk2(initial_world))
| p(sk1(initial_world))
| p(sk3(initial_world))
| q(sk2(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p282,p56]) ).
cnf(p290,plain,
( p(sk3(initial_world))
| q(sk2(initial_world))
| p(sk3(initial_world))
| q(sk2(initial_world))
| p(sk1(initial_world)) ),
inference(factoring,[status(thm)],[p283]) ).
cnf(p293,plain,
( p(sk3(initial_world))
| p(sk3(initial_world))
| q(sk2(initial_world))
| p(sk1(initial_world)) ),
inference(factoring,[status(thm)],[p290]) ).
cnf(p295,plain,
( p(sk3(initial_world))
| q(sk2(initial_world))
| p(sk1(initial_world)) ),
inference(factoring,[status(thm)],[p293]) ).
cnf(p3427,plain,
( p(sk3(initial_world))
| p(sk1(initial_world))
| p(sk1(initial_world))
| q(sk4(initial_world))
| p(sk3(initial_world)) ),
inference(resolution,[status(thm)],[p3426,p295]) ).
cnf(p3428,plain,
( p(sk1(initial_world))
| p(sk1(initial_world))
| q(sk4(initial_world))
| p(sk3(initial_world)) ),
inference(factoring,[status(thm)],[p3427]) ).
cnf(p3430,plain,
( p(sk1(initial_world))
| q(sk4(initial_world))
| p(sk3(initial_world)) ),
inference(factoring,[status(thm)],[p3428]) ).
cnf(c4,plain,
( ~ q(X3)
| ~ reachable(X2,X3)
| ~ reachable(sk0(X0),X2)
| reachable(sk0(X0),sk1(X0))
| ~ reachable(initial_world,X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p59,plain,
( ~ q(X1)
| ~ reachable(X0,X1)
| ~ reachable(sk0(initial_world),X0)
| reachable(sk0(initial_world),sk1(initial_world)) ),
inference(resolution,[status(thm)],[c0,c4]) ).
cnf(p134,plain,
( ~ q(X0)
| ~ reachable(sk0(initial_world),X0)
| reachable(sk0(initial_world),sk1(initial_world)) ),
inference(resolution,[status(thm)],[p59,c0]) ).
cnf(c7,plain,
( reachable(sk0(X0),sk4(X0))
| p(sk3(X0))
| reachable(sk0(X0),sk1(X0))
| ~ reachable(initial_world,X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p55,plain,
( reachable(sk0(initial_world),sk4(initial_world))
| p(sk3(initial_world))
| reachable(sk0(initial_world),sk1(initial_world)) ),
inference(resolution,[status(thm)],[c0,c7]) ).
cnf(p139,plain,
( p(sk3(initial_world))
| reachable(sk0(initial_world),sk1(initial_world))
| ~ q(sk4(initial_world))
| reachable(sk0(initial_world),sk1(initial_world)) ),
inference(resolution,[status(thm)],[p134,p55]) ).
cnf(p190,plain,
( p(sk3(initial_world))
| ~ q(sk4(initial_world))
| reachable(sk0(initial_world),sk1(initial_world)) ),
inference(factoring,[status(thm)],[p139]) ).
cnf(p3431,plain,
( p(sk3(initial_world))
| reachable(sk0(initial_world),sk1(initial_world))
| p(sk1(initial_world))
| p(sk3(initial_world)) ),
inference(resolution,[status(thm)],[p3430,p190]) ).
cnf(p3433,plain,
( reachable(sk0(initial_world),sk1(initial_world))
| p(sk1(initial_world))
| p(sk3(initial_world)) ),
inference(factoring,[status(thm)],[p3431]) ).
cnf(p3443,plain,
( reachable(sk0(initial_world),X0)
| ~ reachable(sk1(initial_world),X0)
| p(sk1(initial_world))
| p(sk3(initial_world)) ),
inference(resolution,[status(thm)],[p3433,c1]) ).
cnf(c13,plain,
( reachable(sk0(X0),sk4(X0))
| p(sk3(X0))
| reachable(sk1(X0),sk2(X0))
| p(sk1(X0))
| ~ reachable(initial_world,X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p68,plain,
( reachable(sk0(initial_world),sk4(initial_world))
| p(sk3(initial_world))
| reachable(sk1(initial_world),sk2(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[c0,c13]) ).
cnf(p3486,plain,
( reachable(sk0(initial_world),sk4(initial_world))
| p(sk3(initial_world))
| p(sk1(initial_world))
| reachable(sk0(initial_world),sk2(initial_world))
| p(sk1(initial_world))
| p(sk3(initial_world)) ),
inference(resolution,[status(thm)],[p3443,p68]) ).
cnf(p5238,plain,
( reachable(sk0(initial_world),sk4(initial_world))
| p(sk1(initial_world))
| reachable(sk0(initial_world),sk2(initial_world))
| p(sk1(initial_world))
| p(sk3(initial_world)) ),
inference(factoring,[status(thm)],[p3486]) ).
cnf(p5240,plain,
( reachable(sk0(initial_world),sk4(initial_world))
| reachable(sk0(initial_world),sk2(initial_world))
| p(sk1(initial_world))
| p(sk3(initial_world)) ),
inference(factoring,[status(thm)],[p5238]) ).
cnf(c28,plain,
( ~ q(X3)
| ~ reachable(X2,X3)
| ~ reachable(sk0(X0),X2)
| ~ q(X4)
| ~ reachable(sk0(X0),X4)
| ~ reachable(initial_world,X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p41,plain,
( ~ q(X2)
| ~ reachable(X1,X2)
| ~ q(X1)
| ~ reachable(sk0(X0),X1)
| ~ reachable(initial_world,X0) ),
inference(factoring,[status(thm)],[c28]) ).
cnf(p46,plain,
( ~ reachable(X1,X1)
| ~ q(X1)
| ~ reachable(sk0(X0),X1)
| ~ reachable(initial_world,X0) ),
inference(factoring,[status(thm)],[p41]) ).
cnf(p76,plain,
( ~ reachable(X0,X0)
| ~ q(X0)
| ~ reachable(sk0(initial_world),X0) ),
inference(resolution,[status(thm)],[c0,p46]) ).
cnf(p5242,plain,
( ~ reachable(sk4(initial_world),sk4(initial_world))
| ~ q(sk4(initial_world))
| reachable(sk0(initial_world),sk2(initial_world))
| p(sk1(initial_world))
| p(sk3(initial_world)) ),
inference(resolution,[status(thm)],[p5240,p76]) ).
cnf(p5269,plain,
( p(sk1(initial_world))
| p(sk3(initial_world))
| ~ reachable(sk4(initial_world),sk4(initial_world))
| reachable(sk0(initial_world),sk2(initial_world))
| p(sk1(initial_world))
| p(sk3(initial_world)) ),
inference(resolution,[status(thm)],[p5242,p3430]) ).
cnf(p6050,plain,
( p(sk1(initial_world))
| ~ reachable(sk4(initial_world),sk4(initial_world))
| reachable(sk0(initial_world),sk2(initial_world))
| p(sk1(initial_world))
| p(sk3(initial_world)) ),
inference(factoring,[status(thm)],[p5269]) ).
cnf(p6052,plain,
( ~ reachable(sk4(initial_world),sk4(initial_world))
| reachable(sk0(initial_world),sk2(initial_world))
| p(sk1(initial_world))
| p(sk3(initial_world)) ),
inference(factoring,[status(thm)],[p6050]) ).
cnf(p6053,plain,
( reachable(sk0(initial_world),sk2(initial_world))
| p(sk1(initial_world))
| p(sk3(initial_world)) ),
inference(resolution,[status(thm)],[p6052,c0]) ).
cnf(p6055,plain,
( ~ reachable(sk2(initial_world),sk2(initial_world))
| ~ q(sk2(initial_world))
| p(sk1(initial_world))
| p(sk3(initial_world)) ),
inference(resolution,[status(thm)],[p6053,p76]) ).
cnf(p6065,plain,
( p(sk3(initial_world))
| p(sk1(initial_world))
| ~ reachable(sk2(initial_world),sk2(initial_world))
| p(sk1(initial_world))
| p(sk3(initial_world)) ),
inference(resolution,[status(thm)],[p6055,p295]) ).
cnf(p6079,plain,
( p(sk1(initial_world))
| ~ reachable(sk2(initial_world),sk2(initial_world))
| p(sk1(initial_world))
| p(sk3(initial_world)) ),
inference(factoring,[status(thm)],[p6065]) ).
cnf(p6081,plain,
( ~ reachable(sk2(initial_world),sk2(initial_world))
| p(sk1(initial_world))
| p(sk3(initial_world)) ),
inference(factoring,[status(thm)],[p6079]) ).
cnf(p6082,plain,
( p(sk1(initial_world))
| p(sk3(initial_world)) ),
inference(resolution,[status(thm)],[p6081,c0]) ).
cnf(c6,plain,
( q(sk4(X0))
| reachable(sk0(X0),sk3(X0))
| reachable(sk0(X0),sk1(X0))
| ~ reachable(initial_world,X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p54,plain,
( q(sk4(initial_world))
| reachable(sk0(initial_world),sk3(initial_world))
| reachable(sk0(initial_world),sk1(initial_world)) ),
inference(resolution,[status(thm)],[c0,c6]) ).
cnf(c21,plain,
( ~ p(X2)
| ~ reachable(sk0(X0),X2)
| ~ p(X4)
| ~ reachable(sk0(X0),X4)
| ~ reachable(initial_world,X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p33,plain,
( ~ p(X1)
| ~ p(X1)
| ~ reachable(sk0(X0),X1)
| ~ reachable(initial_world,X0) ),
inference(factoring,[status(thm)],[c21]) ).
cnf(p35,plain,
( ~ p(X1)
| ~ reachable(sk0(X0),X1)
| ~ reachable(initial_world,X0) ),
inference(factoring,[status(thm)],[p33]) ).
cnf(p57,plain,
( ~ p(X0)
| ~ reachable(sk0(initial_world),X0) ),
inference(resolution,[status(thm)],[c0,p35]) ).
cnf(p124,plain,
( ~ p(sk3(initial_world))
| q(sk4(initial_world))
| reachable(sk0(initial_world),sk1(initial_world)) ),
inference(resolution,[status(thm)],[p54,p57]) ).
cnf(p6083,plain,
( q(sk4(initial_world))
| reachable(sk0(initial_world),sk1(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p6082,p124]) ).
cnf(p6096,plain,
( reachable(sk0(initial_world),X0)
| ~ reachable(sk1(initial_world),X0)
| q(sk4(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p6083,c1]) ).
cnf(c12,plain,
( q(sk4(X0))
| reachable(sk0(X0),sk3(X0))
| reachable(sk1(X0),sk2(X0))
| p(sk1(X0))
| ~ reachable(initial_world,X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p67,plain,
( q(sk4(initial_world))
| reachable(sk0(initial_world),sk3(initial_world))
| reachable(sk1(initial_world),sk2(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[c0,c12]) ).
cnf(p6234,plain,
( q(sk4(initial_world))
| reachable(sk0(initial_world),sk3(initial_world))
| p(sk1(initial_world))
| reachable(sk0(initial_world),sk2(initial_world))
| q(sk4(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p6096,p67]) ).
cnf(p7271,plain,
( q(sk4(initial_world))
| reachable(sk0(initial_world),sk3(initial_world))
| reachable(sk0(initial_world),sk2(initial_world))
| q(sk4(initial_world))
| p(sk1(initial_world)) ),
inference(factoring,[status(thm)],[p6234]) ).
cnf(p7273,plain,
( reachable(sk0(initial_world),sk3(initial_world))
| reachable(sk0(initial_world),sk2(initial_world))
| q(sk4(initial_world))
| p(sk1(initial_world)) ),
inference(factoring,[status(thm)],[p7271]) ).
cnf(p7274,plain,
( ~ p(sk3(initial_world))
| reachable(sk0(initial_world),sk2(initial_world))
| q(sk4(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p7273,p57]) ).
cnf(p7284,plain,
( p(sk1(initial_world))
| reachable(sk0(initial_world),sk2(initial_world))
| q(sk4(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p7274,p6082]) ).
cnf(p7285,plain,
( reachable(sk0(initial_world),sk2(initial_world))
| q(sk4(initial_world))
| p(sk1(initial_world)) ),
inference(factoring,[status(thm)],[p7284]) ).
cnf(p7287,plain,
( ~ reachable(sk2(initial_world),sk2(initial_world))
| ~ q(sk2(initial_world))
| q(sk4(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p7285,p76]) ).
cnf(c18,plain,
( q(sk4(X0))
| reachable(sk0(X0),sk3(X0))
| q(sk2(X0))
| p(sk1(X0))
| ~ reachable(initial_world,X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p63,plain,
( q(sk4(initial_world))
| reachable(sk0(initial_world),sk3(initial_world))
| q(sk2(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[c0,c18]) ).
cnf(p146,plain,
( ~ p(sk3(initial_world))
| q(sk4(initial_world))
| q(sk2(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p63,p57]) ).
cnf(p6084,plain,
( q(sk4(initial_world))
| q(sk2(initial_world))
| p(sk1(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p6082,p146]) ).
cnf(p6182,plain,
( q(sk4(initial_world))
| q(sk2(initial_world))
| p(sk1(initial_world)) ),
inference(factoring,[status(thm)],[p6084]) ).
cnf(c17,plain,
( reachable(sk0(X0),sk4(X0))
| reachable(sk0(X0),sk3(X0))
| q(sk2(X0))
| p(sk1(X0))
| ~ reachable(initial_world,X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p71,plain,
( reachable(sk0(initial_world),sk4(initial_world))
| reachable(sk0(initial_world),sk3(initial_world))
| q(sk2(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[c0,c17]) ).
cnf(p181,plain,
( ~ q(sk4(initial_world))
| q(sk2(initial_world))
| p(sk1(initial_world))
| reachable(sk0(initial_world),sk3(initial_world))
| q(sk2(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p71,p167]) ).
cnf(p323,plain,
( ~ q(sk4(initial_world))
| q(sk2(initial_world))
| reachable(sk0(initial_world),sk3(initial_world))
| q(sk2(initial_world))
| p(sk1(initial_world)) ),
inference(factoring,[status(thm)],[p181]) ).
cnf(p325,plain,
( ~ q(sk4(initial_world))
| reachable(sk0(initial_world),sk3(initial_world))
| q(sk2(initial_world))
| p(sk1(initial_world)) ),
inference(factoring,[status(thm)],[p323]) ).
cnf(p6184,plain,
( reachable(sk0(initial_world),sk3(initial_world))
| q(sk2(initial_world))
| p(sk1(initial_world))
| q(sk2(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p6182,p325]) ).
cnf(p6317,plain,
( reachable(sk0(initial_world),sk3(initial_world))
| q(sk2(initial_world))
| q(sk2(initial_world))
| p(sk1(initial_world)) ),
inference(factoring,[status(thm)],[p6184]) ).
cnf(p6319,plain,
( reachable(sk0(initial_world),sk3(initial_world))
| q(sk2(initial_world))
| p(sk1(initial_world)) ),
inference(factoring,[status(thm)],[p6317]) ).
cnf(p6320,plain,
( ~ p(sk3(initial_world))
| q(sk2(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p6319,p57]) ).
cnf(p6330,plain,
( p(sk1(initial_world))
| q(sk2(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p6320,p6082]) ).
cnf(p6331,plain,
( q(sk2(initial_world))
| p(sk1(initial_world)) ),
inference(factoring,[status(thm)],[p6330]) ).
cnf(p7297,plain,
( p(sk1(initial_world))
| ~ reachable(sk2(initial_world),sk2(initial_world))
| q(sk4(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p7287,p6331]) ).
cnf(p7304,plain,
( ~ reachable(sk2(initial_world),sk2(initial_world))
| q(sk4(initial_world))
| p(sk1(initial_world)) ),
inference(factoring,[status(thm)],[p7297]) ).
cnf(p7305,plain,
( q(sk4(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p7304,c0]) ).
cnf(c5,plain,
( reachable(sk0(X0),sk4(X0))
| reachable(sk0(X0),sk3(X0))
| reachable(sk0(X0),sk1(X0))
| ~ reachable(initial_world,X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p61,plain,
( reachable(sk0(initial_world),sk4(initial_world))
| reachable(sk0(initial_world),sk3(initial_world))
| reachable(sk0(initial_world),sk1(initial_world)) ),
inference(resolution,[status(thm)],[c0,c5]) ).
cnf(p145,plain,
( ~ q(sk4(initial_world))
| reachable(sk0(initial_world),sk1(initial_world))
| reachable(sk0(initial_world),sk3(initial_world))
| reachable(sk0(initial_world),sk1(initial_world)) ),
inference(resolution,[status(thm)],[p61,p134]) ).
cnf(p229,plain,
( ~ q(sk4(initial_world))
| reachable(sk0(initial_world),sk3(initial_world))
| reachable(sk0(initial_world),sk1(initial_world)) ),
inference(factoring,[status(thm)],[p145]) ).
cnf(p7306,plain,
( reachable(sk0(initial_world),sk3(initial_world))
| reachable(sk0(initial_world),sk1(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p7305,p229]) ).
cnf(p7307,plain,
( ~ p(sk3(initial_world))
| reachable(sk0(initial_world),sk1(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p7306,p57]) ).
cnf(p7317,plain,
( p(sk1(initial_world))
| reachable(sk0(initial_world),sk1(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p7307,p6082]) ).
cnf(p7318,plain,
( reachable(sk0(initial_world),sk1(initial_world))
| p(sk1(initial_world)) ),
inference(factoring,[status(thm)],[p7317]) ).
cnf(p7327,plain,
( reachable(sk0(initial_world),X0)
| ~ reachable(sk1(initial_world),X0)
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p7318,c1]) ).
cnf(c11,plain,
( reachable(sk0(X0),sk4(X0))
| reachable(sk0(X0),sk3(X0))
| reachable(sk1(X0),sk2(X0))
| p(sk1(X0))
| ~ reachable(initial_world,X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p82,plain,
( reachable(sk0(initial_world),sk4(initial_world))
| reachable(sk0(initial_world),sk3(initial_world))
| reachable(sk1(initial_world),sk2(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[c0,c11]) ).
cnf(p7369,plain,
( reachable(sk0(initial_world),sk4(initial_world))
| reachable(sk0(initial_world),sk3(initial_world))
| p(sk1(initial_world))
| reachable(sk0(initial_world),sk2(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p7327,p82]) ).
cnf(p8724,plain,
( reachable(sk0(initial_world),sk4(initial_world))
| reachable(sk0(initial_world),sk3(initial_world))
| reachable(sk0(initial_world),sk2(initial_world))
| p(sk1(initial_world)) ),
inference(factoring,[status(thm)],[p7369]) ).
cnf(p8726,plain,
( ~ reachable(sk4(initial_world),sk4(initial_world))
| ~ q(sk4(initial_world))
| reachable(sk0(initial_world),sk3(initial_world))
| reachable(sk0(initial_world),sk2(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p8724,p76]) ).
cnf(p9397,plain,
( p(sk1(initial_world))
| ~ reachable(sk4(initial_world),sk4(initial_world))
| reachable(sk0(initial_world),sk3(initial_world))
| reachable(sk0(initial_world),sk2(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p8726,p7305]) ).
cnf(p9460,plain,
( ~ reachable(sk4(initial_world),sk4(initial_world))
| reachable(sk0(initial_world),sk3(initial_world))
| reachable(sk0(initial_world),sk2(initial_world))
| p(sk1(initial_world)) ),
inference(factoring,[status(thm)],[p9397]) ).
cnf(p9461,plain,
( reachable(sk0(initial_world),sk3(initial_world))
| reachable(sk0(initial_world),sk2(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p9460,c0]) ).
cnf(p9462,plain,
( ~ p(sk3(initial_world))
| reachable(sk0(initial_world),sk2(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p9461,p57]) ).
cnf(p9472,plain,
( p(sk1(initial_world))
| reachable(sk0(initial_world),sk2(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p9462,p6082]) ).
cnf(p9473,plain,
( reachable(sk0(initial_world),sk2(initial_world))
| p(sk1(initial_world)) ),
inference(factoring,[status(thm)],[p9472]) ).
cnf(p9475,plain,
( ~ reachable(sk2(initial_world),sk2(initial_world))
| ~ q(sk2(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p9473,p76]) ).
cnf(p9484,plain,
( p(sk1(initial_world))
| ~ reachable(sk2(initial_world),sk2(initial_world))
| p(sk1(initial_world)) ),
inference(resolution,[status(thm)],[p9475,p6331]) ).
cnf(p9495,plain,
( ~ reachable(sk2(initial_world),sk2(initial_world))
| p(sk1(initial_world)) ),
inference(factoring,[status(thm)],[p9484]) ).
cnf(p9496,plain,
p(sk1(initial_world)),
inference(resolution,[status(thm)],[p9495,c0]) ).
cnf(p120,plain,
( ~ p(sk1(initial_world))
| q(sk4(initial_world))
| p(sk3(initial_world)) ),
inference(resolution,[status(thm)],[p53,p57]) ).
cnf(p9497,plain,
( q(sk4(initial_world))
| p(sk3(initial_world)) ),
inference(resolution,[status(thm)],[p9496,p120]) ).
cnf(p9501,plain,
( p(sk3(initial_world))
| reachable(sk0(initial_world),sk1(initial_world))
| p(sk3(initial_world)) ),
inference(resolution,[status(thm)],[p9497,p190]) ).
cnf(p9621,plain,
( reachable(sk0(initial_world),sk1(initial_world))
| p(sk3(initial_world)) ),
inference(factoring,[status(thm)],[p9501]) ).
cnf(p9622,plain,
( ~ p(sk1(initial_world))
| p(sk3(initial_world)) ),
inference(resolution,[status(thm)],[p9621,p57]) ).
cnf(p9632,plain,
p(sk3(initial_world)),
inference(resolution,[status(thm)],[p9622,p9496]) ).
cnf(p9633,plain,
( q(sk4(initial_world))
| reachable(sk0(initial_world),sk1(initial_world)) ),
inference(resolution,[status(thm)],[p9632,p124]) ).
cnf(p9635,plain,
( ~ p(sk1(initial_world))
| q(sk4(initial_world)) ),
inference(resolution,[status(thm)],[p9633,p57]) ).
cnf(p9645,plain,
q(sk4(initial_world)),
inference(resolution,[status(thm)],[p9635,p9496]) ).
cnf(p9646,plain,
( reachable(sk0(initial_world),sk3(initial_world))
| reachable(sk0(initial_world),sk1(initial_world)) ),
inference(resolution,[status(thm)],[p9645,p229]) ).
cnf(p9804,plain,
( ~ p(sk3(initial_world))
| reachable(sk0(initial_world),sk1(initial_world)) ),
inference(resolution,[status(thm)],[p9646,p57]) ).
cnf(p9812,plain,
reachable(sk0(initial_world),sk1(initial_world)),
inference(resolution,[status(thm)],[p9804,p9632]) ).
cnf(p9813,plain,
~ p(sk1(initial_world)),
inference(resolution,[status(thm)],[p9812,p57]) ).
cnf(p9822,plain,
$false,
inference(resolution,[status(thm)],[p9813,p9496]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN549+1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.36 % Computer : n020.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Fri Sep 25 01:44:20 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 41.13/5.68 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 41.13/5.68 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------