%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SYN548+1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /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 : Thu Sep 24 03:16:46 PM UTC 2026
% Result : Theorem 15.48s 2.47s
% Output : CNFRefutation 15.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 77
% Syntax : Number of formulae : 382 ( 8 unt; 74 def)
% Number of atoms : 1373 ( 0 equ)
% Maximal formula atoms : 12 ( 3 avg)
% Number of connectives : 1712 ( 721 ~; 875 |; 27 &)
% ( 76 <=>; 11 =>; 0 <=; 2 <~>)
% Maximal formula depth : 20 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 78 ( 77 usr; 74 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 1 con; 0-2 aty)
% Number of variables : 320 ( 310 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] : reachable(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y,Z] :
( ( reachable(Y,Z)
& reachable(X,Y) )
=> reachable(X,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,conjecture,
? [X] :
( ! [Y] :
( reachable(X,Y)
=> ( ! [Z] :
( reachable(Y,Z)
=> ( ! [V] :
( reachable(Z,V)
=> q(V) )
| p(Z) ) )
<=> ( ! [W] :
( reachable(Y,W)
=> q(W) )
| ! [W] :
( reachable(Y,W)
=> p(W) ) ) ) )
& reachable(initial_world,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,negated_conjecture,
~ ? [X] :
( ! [Y] :
( reachable(X,Y)
=> ( ! [Z] :
( reachable(Y,Z)
=> ( ! [V] :
( reachable(Z,V)
=> q(V) )
| p(Z) ) )
<=> ( ! [W] :
( reachable(Y,W)
=> q(W) )
| ! [W] :
( reachable(Y,W)
=> p(W) ) ) ) )
& reachable(initial_world,X) ),
inference(negated_conjecture,[status(cth)],[f3]) ).
fof(f5,plain,
! [X0] : reachable(X0,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f6,plain,
! [X,Y,Z] :
( reachable(X,Z)
| ~ reachable(Y,Z)
| ~ reachable(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f7,plain,
! [X,Z] :
( reachable(X,Z)
| ! [Y] :
( ~ reachable(Y,Z)
| ~ reachable(X,Y) ) ),
inference(miniscoping,[status(thm)],[f6]) ).
fof(f8,plain,
! [X0,X1,X2] :
( reachable(X0,X2)
| ~ reachable(X1,X2)
| ~ reachable(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f9,plain,
! [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(X,Y) )
| ~ reachable(initial_world,X) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f10,definition,
! [Y,Z] :
( sP0_prd(Z,Y)
<=> ( ! [V] :
( q(V)
| ~ reachable(Z,V) )
| p(Z)
| ~ reachable(Y,Z) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f11,plain,
! [X] :
( ? [Y] :
( ( ! [Z] : sP0_prd(Z,Y)
<~> ( ! [W] :
( q(W)
| ~ reachable(Y,W) )
| ! [W] :
( p(W)
| ~ reachable(Y,W) ) ) )
& reachable(X,Y) )
| ~ reachable(initial_world,X) ),
inference(formula_renaming,[status(thm)],[f9,f10]) ).
fof(f12,plain,
! [X] :
( ? [Y] :
( ( ( ? [W] :
( ~ q(W)
& reachable(Y,W) )
& ? [W] :
( ~ p(W)
& reachable(Y,W) ) )
| ? [Z] : ~ sP0_prd(Z,Y) )
& ( ! [W] :
( q(W)
| ~ reachable(Y,W) )
| ! [W] :
( p(W)
| ~ reachable(Y,W) )
| ! [Z] : sP0_prd(Z,Y) )
& reachable(X,Y) )
| ~ reachable(initial_world,X) ),
inference(NNF_transformation,[status(thm)],[f11]) ).
fof(f13,plain,
! [X] :
( ( ( ( ~ q(sK3_skl(X))
& reachable(sK0_skl(X),sK3_skl(X))
& ~ p(sK2_skl(X))
& reachable(sK0_skl(X),sK2_skl(X)) )
| ~ sP0_prd(sK1_skl(X),sK0_skl(X)) )
& ( ! [W] :
( q(W)
| ~ reachable(sK0_skl(X),W) )
| ! [W] :
( p(W)
| ~ reachable(sK0_skl(X),W) )
| ! [Z] : sP0_prd(Z,sK0_skl(X)) )
& reachable(X,sK0_skl(X)) )
| ~ reachable(initial_world,X) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl]),skolemize(Y,sK0_skl(X)),skolemize(Z,sK1_skl(X)),skolemize(W,sK2_skl(X)),skolemize(W,sK3_skl(X))],[f12]) ).
fof(f14,plain,
! [X0] :
( reachable(X0,sK0_skl(X0))
| ~ reachable(initial_world,X0) ),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f15,plain,
! [X0,X1,X2,X3] :
( q(X3)
| ~ reachable(sK0_skl(X0),X3)
| p(X2)
| ~ reachable(sK0_skl(X0),X2)
| sP0_prd(X1,sK0_skl(X0))
| ~ reachable(initial_world,X0) ),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f16,plain,
! [X0] :
( reachable(sK0_skl(X0),sK2_skl(X0))
| ~ sP0_prd(sK1_skl(X0),sK0_skl(X0))
| ~ reachable(initial_world,X0) ),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f17,plain,
! [X0] :
( ~ p(sK2_skl(X0))
| ~ sP0_prd(sK1_skl(X0),sK0_skl(X0))
| ~ reachable(initial_world,X0) ),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f18,plain,
! [X0] :
( reachable(sK0_skl(X0),sK3_skl(X0))
| ~ sP0_prd(sK1_skl(X0),sK0_skl(X0))
| ~ reachable(initial_world,X0) ),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f19,plain,
! [X0] :
( ~ q(sK3_skl(X0))
| ~ sP0_prd(sK1_skl(X0),sK0_skl(X0))
| ~ reachable(initial_world,X0) ),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f20,plain,
! [Y,Z] :
( ( ( ? [V] :
( ~ q(V)
& reachable(Z,V) )
& ~ p(Z)
& reachable(Y,Z) )
| sP0_prd(Z,Y) )
& ( ! [V] :
( q(V)
| ~ reachable(Z,V) )
| p(Z)
| ~ reachable(Y,Z)
| ~ sP0_prd(Z,Y) ) ),
inference(NNF_transformation,[status(thm)],[f10]) ).
fof(f21,plain,
( ! [Y,Z] :
( ( ? [V] :
( ~ q(V)
& reachable(Z,V) )
& ~ p(Z)
& reachable(Y,Z) )
| sP0_prd(Z,Y) )
& ! [Y,Z] :
( ! [V] :
( q(V)
| ~ reachable(Z,V) )
| p(Z)
| ~ reachable(Y,Z)
| ~ sP0_prd(Z,Y) ) ),
inference(miniscoping,[status(thm)],[f20]) ).
fof(f22,plain,
( ! [Y,Z] :
( ( ~ q(sK4_skl(Z,Y))
& reachable(Z,sK4_skl(Z,Y))
& ~ p(Z)
& reachable(Y,Z) )
| sP0_prd(Z,Y) )
& ! [Y,Z] :
( ! [V] :
( q(V)
| ~ reachable(Z,V) )
| p(Z)
| ~ reachable(Y,Z)
| ~ sP0_prd(Z,Y) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(V,sK4_skl(Z,Y))],[f21]) ).
fof(f23,plain,
! [X0,X1,X2] :
( q(X2)
| ~ reachable(X0,X2)
| p(X0)
| ~ reachable(X1,X0)
| ~ sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f24,plain,
! [X0,X1] :
( reachable(X1,X0)
| sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f25,plain,
! [X0,X1] :
( ~ p(X0)
| sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f26,plain,
! [X0,X1] :
( reachable(X0,sK4_skl(X0,X1))
| sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f27,plain,
! [X0,X1] :
( ~ q(sK4_skl(X0,X1))
| sP0_prd(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f28,plain,
reachable(initial_world,sK0_skl(initial_world)),
inference(resolution,[status(thm)],[f5,f14]) ).
fof(f29,plain,
reachable(sK0_skl(initial_world),sK0_skl(sK0_skl(initial_world))),
inference(resolution,[status(thm)],[f28,f14]) ).
fof(f31,plain,
! [X0,X1] :
( reachable(X1,sK0_skl(X1))
| ~ reachable(X0,X1)
| ~ reachable(initial_world,X0) ),
inference(resolution,[status(thm)],[f8,f14]) ).
fof(f32,plain,
! [X0] :
( reachable(sK0_skl(initial_world),sK0_skl(sK0_skl(initial_world)))
| ~ reachable(X0,initial_world)
| ~ reachable(initial_world,X0) ),
inference(resolution,[status(thm)],[f31,f14]) ).
fof(f33,definition,
! [X0] :
( sQ0_spl
<=> ( ~ reachable(X0,initial_world)
| ~ reachable(initial_world,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f34,plain,
! [X0] :
( ~ sQ0_spl
| ~ reachable(X0,initial_world)
| ~ reachable(initial_world,X0) ),
inference(component_clause,[status(thm)],[f33]) ).
fof(f36,definition,
( sQ1_spl
<=> reachable(sK0_skl(initial_world),sK0_skl(sK0_skl(initial_world))) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f39,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f32,f33,f36]) ).
fof(f40,plain,
! [X0,X1,X2] :
( q(X2)
| ~ reachable(sK0_skl(X0),X2)
| p(X1)
| ~ reachable(sK0_skl(X0),X1)
| ~ reachable(initial_world,X0)
| reachable(sK0_skl(X0),sK2_skl(X0))
| ~ reachable(initial_world,X0) ),
inference(resolution,[status(thm)],[f16,f15]) ).
fof(f41,plain,
! [X0] :
( reachable(sK0_skl(X0),sK1_skl(X0))
| reachable(sK0_skl(X0),sK2_skl(X0))
| ~ reachable(initial_world,X0) ),
inference(resolution,[status(thm)],[f16,f24]) ).
fof(f42,plain,
! [X0,X1,X2] :
( q(X2)
| ~ reachable(sK0_skl(X0),X2)
| p(X1)
| ~ reachable(sK0_skl(X0),X1)
| reachable(sK0_skl(X0),sK2_skl(X0))
| ~ reachable(initial_world,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f40]) ).
fof(f44,plain,
( ~ sQ0_spl
| ~ reachable(initial_world,initial_world) ),
inference(resolution,[status(thm)],[f34,f5]) ).
fof(f45,plain,
( ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f44,f5]) ).
fof(f46,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f45]) ).
fof(f47,plain,
! [X0,X1,X2,X3,X4] :
( q(X4)
| ~ reachable(sK0_skl(X0),X4)
| p(X3)
| ~ reachable(sK0_skl(X0),X3)
| ~ reachable(initial_world,X0)
| q(X2)
| ~ reachable(X1,X2)
| p(X1)
| ~ reachable(sK0_skl(X0),X1) ),
inference(resolution,[status(thm)],[f23,f15]) ).
fof(f49,plain,
! [X0,X1,X2] :
( q(X2)
| ~ reachable(sK0_skl(X0),X2)
| p(X1)
| ~ reachable(sK0_skl(X0),X1)
| ~ reachable(initial_world,X0)
| reachable(sK0_skl(X0),sK3_skl(X0))
| ~ reachable(initial_world,X0) ),
inference(resolution,[status(thm)],[f18,f15]) ).
fof(f50,plain,
! [X0] :
( reachable(sK0_skl(X0),sK1_skl(X0))
| reachable(sK0_skl(X0),sK3_skl(X0))
| ~ reachable(initial_world,X0) ),
inference(resolution,[status(thm)],[f18,f24]) ).
fof(f51,plain,
! [X0,X1,X2] :
( q(X2)
| ~ reachable(sK0_skl(X0),X2)
| p(X1)
| ~ reachable(sK0_skl(X0),X1)
| reachable(sK0_skl(X0),sK3_skl(X0))
| ~ reachable(initial_world,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f49]) ).
fof(f52,plain,
! [X0,X1,X2,X3] :
( q(X3)
| ~ reachable(sK0_skl(sK0_skl(initial_world)),X3)
| p(X2)
| ~ reachable(sK0_skl(sK0_skl(initial_world)),X2)
| q(X1)
| ~ reachable(X0,X1)
| p(X0)
| ~ reachable(sK0_skl(sK0_skl(initial_world)),X0) ),
inference(resolution,[status(thm)],[f47,f28]) ).
fof(f55,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ reachable(X5,X0)
| ~ reachable(initial_world,X5)
| q(X4)
| ~ reachable(sK0_skl(X0),X4)
| p(X3)
| ~ reachable(sK0_skl(X0),X3)
| q(X2)
| ~ reachable(X1,X2)
| p(X1)
| ~ reachable(sK0_skl(X0),X1) ),
inference(resolution,[status(thm)],[f47,f8]) ).
fof(f56,plain,
! [X0,X1,X2,X3] :
( q(X3)
| ~ reachable(sK0_skl(initial_world),X3)
| p(X2)
| ~ reachable(sK0_skl(initial_world),X2)
| q(X1)
| ~ reachable(X0,X1)
| p(X0)
| ~ reachable(sK0_skl(initial_world),X0) ),
inference(resolution,[status(thm)],[f47,f5]) ).
fof(f57,definition,
! [X0,X1] :
( sQ2_spl
<=> ( q(X1)
| ~ reachable(X0,X1)
| p(X0)
| ~ reachable(sK0_skl(sK0_skl(initial_world)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f58,plain,
! [X0,X1] :
( ~ sQ2_spl
| q(X1)
| ~ reachable(X0,X1)
| p(X0)
| ~ reachable(sK0_skl(sK0_skl(initial_world)),X0) ),
inference(component_clause,[status(thm)],[f57]) ).
fof(f60,definition,
! [X2] :
( sQ3_spl
<=> ( p(X2)
| ~ reachable(sK0_skl(sK0_skl(initial_world)),X2) ) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f61,plain,
! [X0] :
( ~ sQ3_spl
| p(X0)
| ~ reachable(sK0_skl(sK0_skl(initial_world)),X0) ),
inference(component_clause,[status(thm)],[f60]) ).
fof(f63,definition,
! [X3] :
( sQ4_spl
<=> ( q(X3)
| ~ reachable(sK0_skl(sK0_skl(initial_world)),X3) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f64,plain,
! [X0] :
( ~ sQ4_spl
| q(X0)
| ~ reachable(sK0_skl(sK0_skl(initial_world)),X0) ),
inference(component_clause,[status(thm)],[f63]) ).
fof(f66,plain,
( sQ4_spl
| sQ3_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f52,f57,f60,f63]) ).
fof(f68,definition,
! [X0,X1] :
( sQ5_spl
<=> ( q(X1)
| ~ reachable(X0,X1)
| p(X0)
| ~ reachable(sK0_skl(initial_world),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f69,plain,
! [X0,X1] :
( ~ sQ5_spl
| q(X1)
| ~ reachable(X0,X1)
| p(X0)
| ~ reachable(sK0_skl(initial_world),X0) ),
inference(component_clause,[status(thm)],[f68]) ).
fof(f71,definition,
! [X2] :
( sQ6_spl
<=> ( p(X2)
| ~ reachable(sK0_skl(initial_world),X2) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f72,plain,
! [X0] :
( ~ sQ6_spl
| p(X0)
| ~ reachable(sK0_skl(initial_world),X0) ),
inference(component_clause,[status(thm)],[f71]) ).
fof(f74,definition,
! [X3] :
( sQ7_spl
<=> ( q(X3)
| ~ reachable(sK0_skl(initial_world),X3) ) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f75,plain,
! [X0] :
( ~ sQ7_spl
| q(X0)
| ~ reachable(sK0_skl(initial_world),X0) ),
inference(component_clause,[status(thm)],[f74]) ).
fof(f77,plain,
( sQ7_spl
| sQ6_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f56,f68,f71,f74]) ).
fof(f115,plain,
! [X0,X1] :
( ~ sQ7_spl
| ~ reachable(X1,X0)
| ~ reachable(sK0_skl(initial_world),X1)
| q(X0) ),
inference(resolution,[status(thm)],[f75,f8]) ).
fof(f120,definition,
( sQ9_spl
<=> reachable(initial_world,initial_world) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f122,plain,
( sQ9_spl
| ~ reachable(initial_world,initial_world) ),
inference(component_clause,[status(thm)],[f120]) ).
fof(f131,definition,
( sQ12_spl
<=> reachable(sK0_skl(initial_world),sK3_skl(initial_world)) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f132,plain,
( ~ sQ12_spl
| reachable(sK0_skl(initial_world),sK3_skl(initial_world)) ),
inference(component_clause,[status(thm)],[f131]) ).
fof(f135,definition,
( sQ13_spl
<=> reachable(sK0_skl(initial_world),sK2_skl(initial_world)) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f136,plain,
( ~ sQ13_spl
| reachable(sK0_skl(initial_world),sK2_skl(initial_world)) ),
inference(component_clause,[status(thm)],[f135]) ).
fof(f142,definition,
! [X0] :
( sQ15_spl
<=> ( ~ reachable(X0,sK0_skl(initial_world))
| ~ reachable(initial_world,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f143,plain,
! [X0] :
( ~ sQ15_spl
| ~ reachable(X0,sK0_skl(initial_world))
| ~ reachable(initial_world,X0) ),
inference(component_clause,[status(thm)],[f142]) ).
fof(f147,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f122,f5]) ).
fof(f148,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f147]) ).
fof(f149,plain,
! [X0,X1,X2,X3,X4] :
( ~ reachable(sK0_skl(initial_world),X0)
| q(X4)
| ~ reachable(sK0_skl(X0),X4)
| p(X3)
| ~ reachable(sK0_skl(X0),X3)
| q(X2)
| ~ reachable(X1,X2)
| p(X1)
| ~ reachable(sK0_skl(X0),X1) ),
inference(resolution,[status(thm)],[f55,f28]) ).
fof(f150,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ reachable(X5,initial_world)
| ~ reachable(initial_world,X5)
| ~ reachable(sK0_skl(initial_world),X0)
| q(X4)
| ~ reachable(sK0_skl(X0),X4)
| p(X3)
| ~ reachable(sK0_skl(X0),X3)
| q(X2)
| ~ reachable(X1,X2)
| p(X1)
| ~ reachable(sK0_skl(X0),X1) ),
inference(resolution,[status(thm)],[f55,f31]) ).
fof(f152,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ reachable(X6,X5)
| ~ reachable(initial_world,X6)
| ~ reachable(X5,X0)
| q(X4)
| ~ reachable(sK0_skl(X0),X4)
| p(X3)
| ~ reachable(sK0_skl(X0),X3)
| q(X2)
| ~ reachable(X1,X2)
| p(X1)
| ~ reachable(sK0_skl(X0),X1) ),
inference(resolution,[status(thm)],[f55,f8]) ).
fof(f154,definition,
! [X0,X1,X2,X3,X4] :
( sQ16_spl
<=> ( ~ reachable(sK0_skl(initial_world),X0)
| q(X4)
| ~ reachable(sK0_skl(X0),X4)
| p(X3)
| ~ reachable(sK0_skl(X0),X3)
| q(X2)
| ~ reachable(X1,X2)
| p(X1)
| ~ reachable(sK0_skl(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f157,plain,
( sQ0_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f150,f154,f33]) ).
fof(f161,plain,
( ~ sQ6_spl
| reachable(sK0_skl(initial_world),sK3_skl(initial_world))
| ~ reachable(initial_world,initial_world)
| p(sK1_skl(initial_world)) ),
inference(resolution,[status(thm)],[f72,f50]) ).
fof(f162,plain,
( ~ sQ6_spl
| reachable(sK0_skl(initial_world),sK2_skl(initial_world))
| ~ reachable(initial_world,initial_world)
| p(sK1_skl(initial_world)) ),
inference(resolution,[status(thm)],[f72,f41]) ).
fof(f163,plain,
! [X0] :
( ~ sQ6_spl
| ~ reachable(X0,sK0_skl(initial_world))
| ~ reachable(initial_world,X0)
| p(sK0_skl(sK0_skl(initial_world))) ),
inference(resolution,[status(thm)],[f72,f31]) ).
fof(f167,definition,
( sQ17_spl
<=> p(sK3_skl(initial_world)) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f171,definition,
( sQ18_spl
<=> p(sK2_skl(initial_world)) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f172,plain,
( ~ sQ18_spl
| p(sK2_skl(initial_world)) ),
inference(component_clause,[status(thm)],[f171]) ).
fof(f175,definition,
( sQ19_spl
<=> p(sK1_skl(initial_world)) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f176,plain,
( ~ sQ19_spl
| p(sK1_skl(initial_world)) ),
inference(component_clause,[status(thm)],[f175]) ).
fof(f178,plain,
( ~ sQ6_spl
| sQ12_spl
| ~ sQ9_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f161,f175,f120,f131,f71]) ).
fof(f179,plain,
( ~ sQ6_spl
| sQ13_spl
| ~ sQ9_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f162,f175,f120,f135,f71]) ).
fof(f180,definition,
( sQ20_spl
<=> p(sK0_skl(sK0_skl(initial_world))) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f183,plain,
( ~ sQ6_spl
| sQ15_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f163,f180,f142,f71]) ).
fof(f184,plain,
! [X0] :
( ~ sQ19_spl
| sP0_prd(sK1_skl(initial_world),X0) ),
inference(resolution,[status(thm)],[f176,f25]) ).
fof(f185,plain,
( ~ sQ19_spl
| reachable(sK0_skl(initial_world),sK3_skl(initial_world))
| ~ reachable(initial_world,initial_world) ),
inference(resolution,[status(thm)],[f184,f18]) ).
fof(f186,plain,
( ~ sQ19_spl
| reachable(sK0_skl(initial_world),sK2_skl(initial_world))
| ~ reachable(initial_world,initial_world) ),
inference(resolution,[status(thm)],[f184,f16]) ).
fof(f188,plain,
( ~ sQ19_spl
| sQ12_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f185,f120,f131,f175]) ).
fof(f189,plain,
( ~ sQ19_spl
| sQ13_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f186,f120,f135,f175]) ).
fof(f209,plain,
! [X0,X1] :
( ~ sQ4_spl
| ~ reachable(X1,X0)
| ~ reachable(sK0_skl(sK0_skl(initial_world)),X1)
| q(X0) ),
inference(resolution,[status(thm)],[f64,f8]) ).
fof(f214,definition,
( sQ25_spl
<=> reachable(initial_world,sK0_skl(initial_world)) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f216,plain,
( sQ25_spl
| ~ reachable(initial_world,sK0_skl(initial_world)) ),
inference(component_clause,[status(thm)],[f214]) ).
fof(f225,definition,
( sQ28_spl
<=> reachable(sK0_skl(sK0_skl(initial_world)),sK3_skl(sK0_skl(initial_world))) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f226,plain,
( ~ sQ28_spl
| reachable(sK0_skl(sK0_skl(initial_world)),sK3_skl(sK0_skl(initial_world))) ),
inference(component_clause,[status(thm)],[f225]) ).
fof(f229,definition,
( sQ29_spl
<=> reachable(sK0_skl(sK0_skl(initial_world)),sK2_skl(sK0_skl(initial_world))) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f230,plain,
( ~ sQ29_spl
| reachable(sK0_skl(sK0_skl(initial_world)),sK2_skl(sK0_skl(initial_world))) ),
inference(component_clause,[status(thm)],[f229]) ).
fof(f236,definition,
! [X0] :
( sQ31_spl
<=> ( ~ reachable(X0,sK0_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f237,plain,
! [X0] :
( ~ sQ31_spl
| ~ reachable(X0,sK0_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,X0) ),
inference(component_clause,[status(thm)],[f236]) ).
fof(f240,plain,
( sQ25_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f216,f28]) ).
fof(f241,plain,
sQ25_spl,
inference(contradiction_clause,[status(thm)],[f240]) ).
fof(f243,plain,
! [X0] :
( ~ sQ5_spl
| q(X0)
| ~ reachable(sK0_skl(sK0_skl(initial_world)),X0)
| p(sK0_skl(sK0_skl(initial_world))) ),
inference(resolution,[status(thm)],[f69,f29]) ).
fof(f245,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| q(X2)
| ~ reachable(sK0_skl(initial_world),X2)
| p(X1)
| ~ reachable(sK0_skl(initial_world),X1)
| ~ reachable(initial_world,initial_world)
| q(X0)
| ~ reachable(sK2_skl(initial_world),X0)
| p(sK2_skl(initial_world)) ),
inference(resolution,[status(thm)],[f69,f42]) ).
fof(f250,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ reachable(X2,X0)
| ~ reachable(sK0_skl(initial_world),X2)
| q(X1)
| ~ reachable(X0,X1)
| p(X0) ),
inference(resolution,[status(thm)],[f69,f8]) ).
fof(f251,plain,
! [X0] :
( ~ sQ5_spl
| q(X0)
| ~ reachable(sK0_skl(initial_world),X0)
| p(sK0_skl(initial_world)) ),
inference(resolution,[status(thm)],[f69,f5]) ).
fof(f252,definition,
! [X0] :
( sQ32_spl
<=> ( q(X0)
| ~ reachable(sK2_skl(initial_world),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f253,plain,
! [X0] :
( ~ sQ32_spl
| q(X0)
| ~ reachable(sK2_skl(initial_world),X0) ),
inference(component_clause,[status(thm)],[f252]) ).
fof(f256,plain,
( ~ sQ5_spl
| sQ4_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f243,f180,f63,f68]) ).
fof(f257,definition,
! [X0] :
( sQ33_spl
<=> ( q(X0)
| ~ reachable(sK3_skl(initial_world),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f258,plain,
! [X0] :
( ~ sQ33_spl
| q(X0)
| ~ reachable(sK3_skl(initial_world),X0) ),
inference(component_clause,[status(thm)],[f257]) ).
fof(f261,plain,
( ~ sQ5_spl
| sQ7_spl
| sQ6_spl
| ~ sQ9_spl
| sQ32_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f245,f171,f252,f120,f71,f74,f68]) ).
fof(f265,definition,
( sQ34_spl
<=> p(sK0_skl(initial_world)) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f268,plain,
( ~ sQ5_spl
| sQ7_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f251,f265,f74,f68]) ).
fof(f269,plain,
( ~ sQ18_spl
| ~ sP0_prd(sK1_skl(initial_world),sK0_skl(initial_world))
| ~ reachable(initial_world,initial_world) ),
inference(resolution,[status(thm)],[f172,f17]) ).
fof(f271,definition,
( sQ35_spl
<=> sP0_prd(sK1_skl(initial_world),sK0_skl(initial_world)) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f272,plain,
( ~ sQ35_spl
| sP0_prd(sK1_skl(initial_world),sK0_skl(initial_world)) ),
inference(component_clause,[status(thm)],[f271]) ).
fof(f273,plain,
( sQ35_spl
| ~ sP0_prd(sK1_skl(initial_world),sK0_skl(initial_world)) ),
inference(component_clause,[status(thm)],[f271]) ).
fof(f274,plain,
( ~ sQ18_spl
| ~ sQ35_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f269,f120,f271,f171]) ).
fof(f289,plain,
( ~ sQ3_spl
| reachable(sK0_skl(sK0_skl(initial_world)),sK3_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,sK0_skl(initial_world))
| p(sK1_skl(sK0_skl(initial_world))) ),
inference(resolution,[status(thm)],[f61,f50]) ).
fof(f290,plain,
( ~ sQ3_spl
| reachable(sK0_skl(sK0_skl(initial_world)),sK2_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,sK0_skl(initial_world))
| p(sK1_skl(sK0_skl(initial_world))) ),
inference(resolution,[status(thm)],[f61,f41]) ).
fof(f291,plain,
! [X0] :
( ~ sQ3_spl
| ~ reachable(X0,sK0_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,X0)
| p(sK0_skl(sK0_skl(sK0_skl(initial_world)))) ),
inference(resolution,[status(thm)],[f61,f31]) ).
fof(f293,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ reachable(X1,X0)
| ~ reachable(sK0_skl(sK0_skl(initial_world)),X1)
| p(X0) ),
inference(resolution,[status(thm)],[f61,f8]) ).
fof(f295,definition,
( sQ38_spl
<=> p(sK3_skl(sK0_skl(initial_world))) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f299,definition,
( sQ39_spl
<=> p(sK2_skl(sK0_skl(initial_world))) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f300,plain,
( ~ sQ39_spl
| p(sK2_skl(sK0_skl(initial_world))) ),
inference(component_clause,[status(thm)],[f299]) ).
fof(f303,definition,
( sQ40_spl
<=> p(sK1_skl(sK0_skl(initial_world))) ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f304,plain,
( ~ sQ40_spl
| p(sK1_skl(sK0_skl(initial_world))) ),
inference(component_clause,[status(thm)],[f303]) ).
fof(f306,plain,
( ~ sQ3_spl
| sQ28_spl
| ~ sQ25_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f289,f303,f214,f225,f60]) ).
fof(f307,plain,
( ~ sQ3_spl
| sQ29_spl
| ~ sQ25_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f290,f303,f214,f229,f60]) ).
fof(f308,definition,
( sQ41_spl
<=> p(sK0_skl(sK0_skl(sK0_skl(initial_world)))) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f311,plain,
( ~ sQ3_spl
| sQ31_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f291,f308,f236,f60]) ).
fof(f312,plain,
( ~ sQ12_spl
| ~ sQ7_spl
| q(sK3_skl(initial_world)) ),
inference(resolution,[status(thm)],[f75,f132]) ).
fof(f329,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| q(X2)
| ~ reachable(sK0_skl(sK0_skl(initial_world)),X2)
| p(X1)
| ~ reachable(sK0_skl(sK0_skl(initial_world)),X1)
| ~ reachable(initial_world,sK0_skl(initial_world))
| q(X0)
| ~ reachable(sK2_skl(sK0_skl(initial_world)),X0)
| p(sK2_skl(sK0_skl(initial_world))) ),
inference(resolution,[status(thm)],[f58,f42]) ).
fof(f330,plain,
! [X0] :
( ~ sQ2_spl
| reachable(sK0_skl(sK0_skl(initial_world)),sK3_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,sK0_skl(initial_world))
| q(X0)
| ~ reachable(sK1_skl(sK0_skl(initial_world)),X0)
| p(sK1_skl(sK0_skl(initial_world))) ),
inference(resolution,[status(thm)],[f58,f50]) ).
fof(f331,plain,
! [X0] :
( ~ sQ2_spl
| reachable(sK0_skl(sK0_skl(initial_world)),sK2_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,sK0_skl(initial_world))
| q(X0)
| ~ reachable(sK1_skl(sK0_skl(initial_world)),X0)
| p(sK1_skl(sK0_skl(initial_world))) ),
inference(resolution,[status(thm)],[f58,f41]) ).
fof(f332,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ reachable(X1,sK0_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,X1)
| q(X0)
| ~ reachable(sK0_skl(sK0_skl(sK0_skl(initial_world))),X0)
| p(sK0_skl(sK0_skl(sK0_skl(initial_world)))) ),
inference(resolution,[status(thm)],[f58,f31]) ).
fof(f334,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| ~ reachable(X2,X0)
| ~ reachable(sK0_skl(sK0_skl(initial_world)),X2)
| q(X1)
| ~ reachable(X0,X1)
| p(X0) ),
inference(resolution,[status(thm)],[f58,f8]) ).
fof(f335,plain,
! [X0] :
( ~ sQ2_spl
| q(X0)
| ~ reachable(sK0_skl(sK0_skl(initial_world)),X0)
| p(sK0_skl(sK0_skl(initial_world))) ),
inference(resolution,[status(thm)],[f58,f5]) ).
fof(f336,definition,
! [X0] :
( sQ42_spl
<=> ( q(X0)
| ~ reachable(sK3_skl(sK0_skl(initial_world)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f337,plain,
! [X0] :
( ~ sQ42_spl
| q(X0)
| ~ reachable(sK3_skl(sK0_skl(initial_world)),X0) ),
inference(component_clause,[status(thm)],[f336]) ).
fof(f340,definition,
! [X0] :
( sQ43_spl
<=> ( q(X0)
| ~ reachable(sK2_skl(sK0_skl(initial_world)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f341,plain,
! [X0] :
( ~ sQ43_spl
| q(X0)
| ~ reachable(sK2_skl(sK0_skl(initial_world)),X0) ),
inference(component_clause,[status(thm)],[f340]) ).
fof(f343,plain,
( ~ sQ2_spl
| sQ4_spl
| sQ3_spl
| ~ sQ25_spl
| sQ43_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f329,f299,f340,f214,f60,f63,f57]) ).
fof(f344,definition,
! [X0] :
( sQ44_spl
<=> ( q(X0)
| ~ reachable(sK1_skl(sK0_skl(initial_world)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f345,plain,
! [X0] :
( ~ sQ44_spl
| q(X0)
| ~ reachable(sK1_skl(sK0_skl(initial_world)),X0) ),
inference(component_clause,[status(thm)],[f344]) ).
fof(f347,plain,
( ~ sQ2_spl
| sQ28_spl
| ~ sQ25_spl
| sQ44_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f330,f303,f344,f214,f225,f57]) ).
fof(f348,plain,
( ~ sQ2_spl
| sQ29_spl
| ~ sQ25_spl
| sQ44_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f331,f303,f344,f214,f229,f57]) ).
fof(f349,definition,
! [X0] :
( sQ45_spl
<=> ( q(X0)
| ~ reachable(sK0_skl(sK0_skl(sK0_skl(initial_world))),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f350,plain,
! [X0] :
( ~ sQ45_spl
| q(X0)
| ~ reachable(sK0_skl(sK0_skl(sK0_skl(initial_world))),X0) ),
inference(component_clause,[status(thm)],[f349]) ).
fof(f352,plain,
( ~ sQ2_spl
| sQ31_spl
| sQ45_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f332,f308,f349,f236,f57]) ).
fof(f353,plain,
( ~ sQ2_spl
| sQ4_spl
| sQ20_spl ),
inference(split_clause,[status(thm)],[f335,f180,f63,f57]) ).
fof(f354,plain,
( ~ sQ12_spl
| ~ sQ7_spl
| ~ sP0_prd(sK1_skl(initial_world),sK0_skl(initial_world))
| ~ reachable(initial_world,initial_world) ),
inference(resolution,[status(thm)],[f312,f19]) ).
fof(f355,plain,
( ~ sQ12_spl
| ~ sQ7_spl
| ~ sQ35_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f354,f120,f271,f74,f131]) ).
fof(f358,plain,
! [X0] :
( ~ sQ40_spl
| sP0_prd(sK1_skl(sK0_skl(initial_world)),X0) ),
inference(resolution,[status(thm)],[f304,f25]) ).
fof(f372,plain,
( ~ sQ39_spl
| ~ sP0_prd(sK1_skl(sK0_skl(initial_world)),sK0_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,sK0_skl(initial_world)) ),
inference(resolution,[status(thm)],[f300,f17]) ).
fof(f374,definition,
( sQ46_spl
<=> sP0_prd(sK1_skl(sK0_skl(initial_world)),sK0_skl(sK0_skl(initial_world))) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f376,plain,
( sQ46_spl
| ~ sP0_prd(sK1_skl(sK0_skl(initial_world)),sK0_skl(sK0_skl(initial_world))) ),
inference(component_clause,[status(thm)],[f374]) ).
fof(f377,plain,
( ~ sQ39_spl
| ~ sQ46_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f372,f214,f374,f299]) ).
fof(f378,plain,
( sQ46_spl
| ~ sQ40_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f376,f358]) ).
fof(f379,plain,
( sQ46_spl
| ~ sQ40_spl ),
inference(contradiction_clause,[status(thm)],[f378]) ).
fof(f401,plain,
( ~ sQ13_spl
| ~ sQ6_spl
| p(sK2_skl(initial_world)) ),
inference(resolution,[status(thm)],[f72,f136]) ).
fof(f424,plain,
( ~ sQ13_spl
| ~ sQ6_spl
| ~ sP0_prd(sK1_skl(initial_world),sK0_skl(initial_world))
| ~ reachable(initial_world,initial_world) ),
inference(resolution,[status(thm)],[f401,f17]) ).
fof(f426,plain,
( ~ sQ13_spl
| ~ sQ6_spl
| ~ sQ35_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f424,f120,f271,f71,f135]) ).
fof(f436,plain,
! [X0,X1] :
( ~ sQ32_spl
| ~ reachable(X1,X0)
| ~ reachable(sK2_skl(initial_world),X1)
| q(X0) ),
inference(resolution,[status(thm)],[f253,f8]) ).
fof(f441,definition,
! [X0] :
( sQ52_spl
<=> ( ~ reachable(X0,sK2_skl(initial_world))
| ~ reachable(initial_world,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f442,plain,
! [X0] :
( ~ sQ52_spl
| ~ reachable(X0,sK2_skl(initial_world))
| ~ reachable(initial_world,X0) ),
inference(component_clause,[status(thm)],[f441]) ).
fof(f451,plain,
! [X0] :
( ~ sQ33_spl
| ~ reachable(X0,sK3_skl(initial_world))
| ~ reachable(initial_world,X0)
| q(sK0_skl(sK3_skl(initial_world))) ),
inference(resolution,[status(thm)],[f258,f31]) ).
fof(f454,plain,
( ~ sQ33_spl
| q(sK3_skl(initial_world)) ),
inference(resolution,[status(thm)],[f258,f5]) ).
fof(f455,definition,
( sQ53_spl
<=> q(sK0_skl(sK3_skl(initial_world))) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f458,definition,
! [X0] :
( sQ54_spl
<=> ( ~ reachable(X0,sK3_skl(initial_world))
| ~ reachable(initial_world,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f459,plain,
! [X0] :
( ~ sQ54_spl
| ~ reachable(X0,sK3_skl(initial_world))
| ~ reachable(initial_world,X0) ),
inference(component_clause,[status(thm)],[f458]) ).
fof(f461,plain,
( ~ sQ33_spl
| sQ54_spl
| sQ53_spl ),
inference(split_clause,[status(thm)],[f451,f455,f458,f257]) ).
fof(f462,plain,
! [X0] :
( ~ sQ12_spl
| ~ sQ5_spl
| q(X0)
| ~ reachable(sK3_skl(initial_world),X0)
| p(sK3_skl(initial_world)) ),
inference(resolution,[status(thm)],[f69,f132]) ).
fof(f472,plain,
( ~ sQ12_spl
| ~ sQ5_spl
| sQ33_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f462,f167,f257,f68,f131]) ).
fof(f495,plain,
! [X0,X1] :
( sQ35_spl
| q(X1)
| ~ reachable(sK0_skl(initial_world),X1)
| p(X0)
| ~ reachable(sK0_skl(initial_world),X0)
| ~ reachable(initial_world,initial_world) ),
inference(resolution,[status(thm)],[f273,f15]) ).
fof(f496,plain,
( sQ35_spl
| reachable(sK0_skl(initial_world),sK1_skl(initial_world)) ),
inference(resolution,[status(thm)],[f273,f24]) ).
fof(f497,plain,
( sQ35_spl
| sQ7_spl
| sQ6_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f495,f120,f71,f74,f271]) ).
fof(f498,plain,
( sQ35_spl
| ~ sQ19_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f273,f184]) ).
fof(f499,plain,
( sQ35_spl
| ~ sQ19_spl ),
inference(contradiction_clause,[status(thm)],[f498]) ).
fof(f516,plain,
( ~ sQ6_spl
| sQ35_spl
| p(sK1_skl(initial_world)) ),
inference(resolution,[status(thm)],[f496,f72]) ).
fof(f517,plain,
( ~ sQ6_spl
| sQ35_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f516,f175,f271,f71]) ).
fof(f551,plain,
( ~ sQ15_spl
| ~ reachable(initial_world,initial_world) ),
inference(resolution,[status(thm)],[f143,f28]) ).
fof(f555,plain,
( ~ sQ15_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f551,f120,f142]) ).
fof(f559,plain,
! [X0] :
( ~ sQ44_spl
| sP0_prd(sK1_skl(sK0_skl(initial_world)),X0)
| q(sK4_skl(sK1_skl(sK0_skl(initial_world)),X0)) ),
inference(resolution,[status(thm)],[f345,f26]) ).
fof(f569,plain,
( sQ46_spl
| ~ sQ44_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f376,f570]) ).
fof(f570,plain,
! [X0] :
( ~ sQ44_spl
| sP0_prd(sK1_skl(sK0_skl(initial_world)),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f559,f27]) ).
fof(f571,plain,
( sQ46_spl
| ~ sQ44_spl ),
inference(contradiction_clause,[status(thm)],[f569]) ).
fof(f572,plain,
! [X0,X1] :
( ~ sQ52_spl
| q(X1)
| ~ reachable(sK0_skl(initial_world),X1)
| p(X0)
| ~ reachable(sK0_skl(initial_world),X0)
| ~ reachable(initial_world,initial_world)
| ~ reachable(initial_world,sK0_skl(initial_world)) ),
inference(resolution,[status(thm)],[f442,f42]) ).
fof(f575,plain,
( ~ sQ52_spl
| sQ7_spl
| sQ6_spl
| ~ sQ9_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f572,f214,f120,f71,f74,f441]) ).
fof(f688,plain,
( ~ sQ31_spl
| ~ reachable(initial_world,sK0_skl(initial_world)) ),
inference(resolution,[status(thm)],[f237,f29]) ).
fof(f692,plain,
( ~ sQ31_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f688,f214,f236]) ).
fof(f723,plain,
( ~ sQ12_spl
| ~ sQ54_spl
| ~ reachable(initial_world,sK0_skl(initial_world)) ),
inference(resolution,[status(thm)],[f459,f132]) ).
fof(f727,plain,
( ~ sQ12_spl
| ~ sQ54_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f723,f214,f458,f131]) ).
fof(f730,plain,
( ~ sQ35_spl
| reachable(sK0_skl(initial_world),sK2_skl(initial_world))
| ~ reachable(initial_world,initial_world) ),
inference(resolution,[status(thm)],[f272,f16]) ).
fof(f733,plain,
( ~ sQ35_spl
| sQ13_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f730,f120,f135,f271]) ).
fof(f809,plain,
! [X0] :
( ~ sQ43_spl
| ~ reachable(X0,sK2_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,X0)
| q(sK0_skl(sK2_skl(sK0_skl(initial_world)))) ),
inference(resolution,[status(thm)],[f341,f31]) ).
fof(f813,definition,
( sQ59_spl
<=> q(sK0_skl(sK2_skl(sK0_skl(initial_world)))) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f816,definition,
! [X0] :
( sQ60_spl
<=> ( ~ reachable(X0,sK2_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f817,plain,
! [X0] :
( ~ sQ60_spl
| ~ reachable(X0,sK2_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,X0) ),
inference(component_clause,[status(thm)],[f816]) ).
fof(f819,plain,
( ~ sQ43_spl
| sQ60_spl
| sQ59_spl ),
inference(split_clause,[status(thm)],[f809,f813,f816,f340]) ).
fof(f821,plain,
( ~ sQ33_spl
| ~ sP0_prd(sK1_skl(initial_world),sK0_skl(initial_world))
| ~ reachable(initial_world,initial_world) ),
inference(resolution,[status(thm)],[f454,f19]) ).
fof(f822,plain,
( ~ sQ33_spl
| ~ sQ35_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f821,f120,f271,f257]) ).
fof(f836,plain,
! [X0] :
( ~ sQ42_spl
| ~ reachable(X0,sK3_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,X0)
| q(sK0_skl(sK3_skl(sK0_skl(initial_world)))) ),
inference(resolution,[status(thm)],[f337,f31]) ).
fof(f839,plain,
( ~ sQ42_spl
| q(sK3_skl(sK0_skl(initial_world))) ),
inference(resolution,[status(thm)],[f337,f5]) ).
fof(f840,definition,
( sQ62_spl
<=> q(sK0_skl(sK3_skl(sK0_skl(initial_world)))) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f843,definition,
! [X0] :
( sQ63_spl
<=> ( ~ reachable(X0,sK3_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f844,plain,
! [X0] :
( ~ sQ63_spl
| ~ reachable(X0,sK3_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,X0) ),
inference(component_clause,[status(thm)],[f843]) ).
fof(f846,plain,
( ~ sQ42_spl
| sQ63_spl
| sQ62_spl ),
inference(split_clause,[status(thm)],[f836,f840,f843,f336]) ).
fof(f919,plain,
( ~ sQ42_spl
| ~ sP0_prd(sK1_skl(sK0_skl(initial_world)),sK0_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,sK0_skl(initial_world)) ),
inference(resolution,[status(thm)],[f839,f19]) ).
fof(f920,plain,
( ~ sQ42_spl
| ~ sQ46_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f919,f214,f374,f336]) ).
fof(f921,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ29_spl
| q(X0)
| ~ reachable(sK2_skl(sK0_skl(initial_world)),X0)
| p(sK2_skl(sK0_skl(initial_world))) ),
inference(resolution,[status(thm)],[f230,f58]) ).
fof(f922,plain,
( ~ sQ2_spl
| ~ sQ29_spl
| sQ43_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f921,f299,f340,f229,f57]) ).
fof(f923,plain,
! [X0] :
( ~ sQ2_spl
| ~ sQ28_spl
| q(X0)
| ~ reachable(sK3_skl(sK0_skl(initial_world)),X0)
| p(sK3_skl(sK0_skl(initial_world))) ),
inference(resolution,[status(thm)],[f226,f58]) ).
fof(f924,plain,
( ~ sQ2_spl
| ~ sQ28_spl
| sQ42_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f923,f295,f336,f225,f57]) ).
fof(f925,plain,
! [X0,X1] :
( ~ sQ32_spl
| ~ reachable(X1,sK2_skl(initial_world))
| ~ reachable(initial_world,X1)
| ~ reachable(sK0_skl(sK2_skl(initial_world)),X0)
| q(X0) ),
inference(resolution,[status(thm)],[f436,f31]) ).
fof(f929,definition,
! [X0] :
( sQ64_spl
<=> ( ~ reachable(sK0_skl(sK2_skl(initial_world)),X0)
| q(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f930,plain,
! [X0] :
( ~ sQ64_spl
| ~ reachable(sK0_skl(sK2_skl(initial_world)),X0)
| q(X0) ),
inference(component_clause,[status(thm)],[f929]) ).
fof(f932,plain,
( ~ sQ32_spl
| sQ52_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f925,f929,f441,f252]) ).
fof(f939,plain,
! [X0,X1] :
( ~ sQ64_spl
| ~ reachable(X1,X0)
| ~ reachable(sK0_skl(sK2_skl(initial_world)),X1)
| q(X0) ),
inference(resolution,[status(thm)],[f930,f8]) ).
fof(f944,definition,
( sQ66_spl
<=> reachable(initial_world,sK2_skl(initial_world)) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f946,plain,
( sQ66_spl
| ~ reachable(initial_world,sK2_skl(initial_world)) ),
inference(component_clause,[status(thm)],[f944]) ).
fof(f958,definition,
( sQ70_spl
<=> reachable(sK0_skl(sK2_skl(initial_world)),sK3_skl(sK2_skl(initial_world))) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f959,plain,
( ~ sQ70_spl
| reachable(sK0_skl(sK2_skl(initial_world)),sK3_skl(sK2_skl(initial_world))) ),
inference(component_clause,[status(thm)],[f958]) ).
fof(f974,plain,
! [X0] :
( sQ66_spl
| ~ reachable(X0,sK2_skl(initial_world))
| ~ reachable(initial_world,X0) ),
inference(resolution,[status(thm)],[f946,f8]) ).
fof(f975,plain,
( sQ66_spl
| sQ52_spl ),
inference(split_clause,[status(thm)],[f974,f441,f944]) ).
fof(f977,plain,
! [X0,X1,X2,X3] :
( ~ sQ12_spl
| q(X3)
| ~ reachable(sK0_skl(sK3_skl(initial_world)),X3)
| p(X2)
| ~ reachable(sK0_skl(sK3_skl(initial_world)),X2)
| q(X1)
| ~ reachable(X0,X1)
| p(X0)
| ~ reachable(sK0_skl(sK3_skl(initial_world)),X0) ),
inference(resolution,[status(thm)],[f149,f132]) ).
fof(f991,definition,
! [X0,X1] :
( sQ75_spl
<=> ( q(X1)
| ~ reachable(X0,X1)
| p(X0)
| ~ reachable(sK0_skl(sK3_skl(initial_world)),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f994,definition,
! [X2] :
( sQ76_spl
<=> ( p(X2)
| ~ reachable(sK0_skl(sK3_skl(initial_world)),X2) ) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f995,plain,
! [X0] :
( ~ sQ76_spl
| p(X0)
| ~ reachable(sK0_skl(sK3_skl(initial_world)),X0) ),
inference(component_clause,[status(thm)],[f994]) ).
fof(f997,definition,
! [X3] :
( sQ77_spl
<=> ( q(X3)
| ~ reachable(sK0_skl(sK3_skl(initial_world)),X3) ) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f998,plain,
! [X0] :
( ~ sQ77_spl
| q(X0)
| ~ reachable(sK0_skl(sK3_skl(initial_world)),X0) ),
inference(component_clause,[status(thm)],[f997]) ).
fof(f1000,plain,
( ~ sQ12_spl
| sQ77_spl
| sQ76_spl
| sQ75_spl ),
inference(split_clause,[status(thm)],[f977,f991,f994,f997,f131]) ).
fof(f1001,definition,
! [X0,X1] :
( sQ78_spl
<=> ( q(X1)
| ~ reachable(X0,X1)
| p(X0)
| ~ reachable(sK0_skl(sK0_skl(sK0_skl(initial_world))),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f1004,definition,
! [X2] :
( sQ79_spl
<=> ( p(X2)
| ~ reachable(sK0_skl(sK0_skl(sK0_skl(initial_world))),X2) ) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f1005,plain,
! [X0] :
( ~ sQ79_spl
| p(X0)
| ~ reachable(sK0_skl(sK0_skl(sK0_skl(initial_world))),X0) ),
inference(component_clause,[status(thm)],[f1004]) ).
fof(f1030,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ reachable(X6,initial_world)
| ~ reachable(initial_world,X6)
| ~ reachable(sK0_skl(initial_world),X5)
| ~ reachable(X5,X0)
| q(X4)
| ~ reachable(sK0_skl(X0),X4)
| p(X3)
| ~ reachable(sK0_skl(X0),X3)
| q(X2)
| ~ reachable(X1,X2)
| p(X1)
| ~ reachable(sK0_skl(X0),X1) ),
inference(resolution,[status(thm)],[f152,f31]) ).
fof(f1034,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ83_spl
<=> ( ~ reachable(sK0_skl(initial_world),X5)
| ~ reachable(X5,X0)
| q(X4)
| ~ reachable(sK0_skl(X0),X4)
| p(X3)
| ~ reachable(sK0_skl(X0),X3)
| q(X2)
| ~ reachable(X1,X2)
| p(X1)
| ~ reachable(sK0_skl(X0),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f1037,plain,
( sQ0_spl
| sQ83_spl ),
inference(split_clause,[status(thm)],[f1030,f1034,f33]) ).
fof(f1058,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ reachable(X2,sK0_skl(initial_world))
| ~ reachable(initial_world,X2)
| ~ reachable(sK0_skl(sK0_skl(initial_world)),X0)
| q(X1)
| ~ reachable(X0,X1)
| p(X0) ),
inference(resolution,[status(thm)],[f250,f31]) ).
fof(f1075,plain,
( ~ sQ5_spl
| sQ15_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f1058,f57,f142,f68]) ).
fof(f1143,plain,
( ~ sQ45_spl
| reachable(sK0_skl(sK0_skl(sK0_skl(initial_world))),sK3_skl(sK0_skl(sK0_skl(initial_world))))
| ~ reachable(initial_world,sK0_skl(sK0_skl(initial_world)))
| q(sK1_skl(sK0_skl(sK0_skl(initial_world)))) ),
inference(resolution,[status(thm)],[f350,f50]) ).
fof(f1144,plain,
( ~ sQ45_spl
| reachable(sK0_skl(sK0_skl(sK0_skl(initial_world))),sK2_skl(sK0_skl(sK0_skl(initial_world))))
| ~ reachable(initial_world,sK0_skl(sK0_skl(initial_world)))
| q(sK1_skl(sK0_skl(sK0_skl(initial_world)))) ),
inference(resolution,[status(thm)],[f350,f41]) ).
fof(f1145,plain,
! [X0] :
( ~ sQ45_spl
| ~ reachable(X0,sK0_skl(sK0_skl(sK0_skl(initial_world))))
| ~ reachable(initial_world,X0)
| q(sK0_skl(sK0_skl(sK0_skl(sK0_skl(initial_world))))) ),
inference(resolution,[status(thm)],[f350,f31]) ).
fof(f1152,definition,
( sQ102_spl
<=> reachable(initial_world,sK0_skl(sK0_skl(initial_world))) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f1154,plain,
( sQ102_spl
| ~ reachable(initial_world,sK0_skl(sK0_skl(initial_world))) ),
inference(component_clause,[status(thm)],[f1152]) ).
fof(f1160,definition,
( sQ104_spl
<=> q(sK1_skl(sK0_skl(sK0_skl(initial_world)))) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f1163,definition,
( sQ105_spl
<=> reachable(sK0_skl(sK0_skl(sK0_skl(initial_world))),sK3_skl(sK0_skl(sK0_skl(initial_world)))) ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f1166,plain,
( ~ sQ45_spl
| sQ105_spl
| ~ sQ102_spl
| sQ104_spl ),
inference(split_clause,[status(thm)],[f1143,f1160,f1152,f1163,f349]) ).
fof(f1167,definition,
( sQ106_spl
<=> reachable(sK0_skl(sK0_skl(sK0_skl(initial_world))),sK2_skl(sK0_skl(sK0_skl(initial_world)))) ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f1170,plain,
( ~ sQ45_spl
| sQ106_spl
| ~ sQ102_spl
| sQ104_spl ),
inference(split_clause,[status(thm)],[f1144,f1160,f1152,f1167,f349]) ).
fof(f1171,definition,
( sQ107_spl
<=> q(sK0_skl(sK0_skl(sK0_skl(sK0_skl(initial_world))))) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f1174,definition,
! [X0] :
( sQ108_spl
<=> ( ~ reachable(X0,sK0_skl(sK0_skl(sK0_skl(initial_world))))
| ~ reachable(initial_world,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f1177,plain,
( ~ sQ45_spl
| sQ108_spl
| sQ107_spl ),
inference(split_clause,[status(thm)],[f1145,f1171,f1174,f349]) ).
fof(f1180,plain,
! [X0,X1,X2,X3] :
( ~ sQ2_spl
| q(X3)
| ~ reachable(sK0_skl(sK0_skl(initial_world)),X3)
| p(X2)
| ~ reachable(sK0_skl(sK0_skl(initial_world)),X2)
| ~ reachable(initial_world,sK0_skl(initial_world))
| ~ reachable(sK3_skl(sK0_skl(initial_world)),X0)
| q(X1)
| ~ reachable(X0,X1)
| p(X0) ),
inference(resolution,[status(thm)],[f334,f51]) ).
fof(f1181,plain,
! [X0,X1,X2,X3] :
( ~ sQ2_spl
| q(X3)
| ~ reachable(sK0_skl(sK0_skl(initial_world)),X3)
| p(X2)
| ~ reachable(sK0_skl(sK0_skl(initial_world)),X2)
| ~ reachable(initial_world,sK0_skl(initial_world))
| ~ reachable(sK2_skl(sK0_skl(initial_world)),X0)
| q(X1)
| ~ reachable(X0,X1)
| p(X0) ),
inference(resolution,[status(thm)],[f334,f42]) ).
fof(f1184,plain,
! [X0,X1,X2] :
( ~ sQ2_spl
| ~ reachable(X2,sK0_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,X2)
| ~ reachable(sK0_skl(sK0_skl(sK0_skl(initial_world))),X0)
| q(X1)
| ~ reachable(X0,X1)
| p(X0) ),
inference(resolution,[status(thm)],[f334,f31]) ).
fof(f1188,definition,
! [X0,X1] :
( sQ109_spl
<=> ( ~ reachable(sK3_skl(sK0_skl(initial_world)),X0)
| q(X1)
| ~ reachable(X0,X1)
| p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f1191,plain,
( ~ sQ2_spl
| sQ4_spl
| sQ3_spl
| ~ sQ25_spl
| sQ109_spl ),
inference(split_clause,[status(thm)],[f1180,f1188,f214,f60,f63,f57]) ).
fof(f1192,definition,
! [X0,X1] :
( sQ110_spl
<=> ( ~ reachable(sK2_skl(sK0_skl(initial_world)),X0)
| q(X1)
| ~ reachable(X0,X1)
| p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f1195,plain,
( ~ sQ2_spl
| sQ4_spl
| sQ3_spl
| ~ sQ25_spl
| sQ110_spl ),
inference(split_clause,[status(thm)],[f1181,f1192,f214,f60,f63,f57]) ).
fof(f1201,plain,
( ~ sQ2_spl
| sQ31_spl
| sQ78_spl ),
inference(split_clause,[status(thm)],[f1184,f1001,f236,f57]) ).
fof(f1215,plain,
( ~ sQ40_spl
| reachable(sK0_skl(sK0_skl(initial_world)),sK3_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,sK0_skl(initial_world)) ),
inference(resolution,[status(thm)],[f358,f18]) ).
fof(f1216,plain,
( ~ sQ40_spl
| reachable(sK0_skl(sK0_skl(initial_world)),sK2_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,sK0_skl(initial_world)) ),
inference(resolution,[status(thm)],[f358,f16]) ).
fof(f1218,plain,
( ~ sQ40_spl
| sQ28_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f1215,f214,f225,f303]) ).
fof(f1219,plain,
( ~ sQ40_spl
| sQ29_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f1216,f214,f229,f303]) ).
fof(f1230,plain,
! [X0] :
( sQ102_spl
| ~ reachable(X0,sK0_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,X0) ),
inference(resolution,[status(thm)],[f1154,f8]) ).
fof(f1231,plain,
( sQ102_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f1230,f236,f1152]) ).
fof(f1249,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ reachable(X1,sK0_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,X1)
| ~ reachable(sK0_skl(sK0_skl(sK0_skl(initial_world))),X0)
| p(X0) ),
inference(resolution,[status(thm)],[f293,f31]) ).
fof(f1261,definition,
! [X0] :
( sQ117_spl
<=> ( ~ reachable(sK1_skl(sK0_skl(initial_world)),X0)
| p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition]) ).
fof(f1262,plain,
! [X0] :
( ~ sQ117_spl
| ~ reachable(sK1_skl(sK0_skl(initial_world)),X0)
| p(X0) ),
inference(component_clause,[status(thm)],[f1261]) ).
fof(f1266,plain,
( ~ sQ3_spl
| sQ31_spl
| sQ79_spl ),
inference(split_clause,[status(thm)],[f1249,f1004,f236,f60]) ).
fof(f1330,definition,
! [X1] :
( sQ125_spl
<=> ( q(X1)
| ~ reachable(sK1_skl(sK2_skl(initial_world)),X1) ) ),
introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition]) ).
fof(f1331,plain,
! [X0] :
( ~ sQ125_spl
| q(X0)
| ~ reachable(sK1_skl(sK2_skl(initial_world)),X0) ),
inference(component_clause,[status(thm)],[f1330]) ).
fof(f1345,plain,
( ~ sQ77_spl
| reachable(sK0_skl(sK3_skl(initial_world)),sK3_skl(sK3_skl(initial_world)))
| ~ reachable(initial_world,sK3_skl(initial_world))
| q(sK1_skl(sK3_skl(initial_world))) ),
inference(resolution,[status(thm)],[f998,f50]) ).
fof(f1346,plain,
( ~ sQ77_spl
| reachable(sK0_skl(sK3_skl(initial_world)),sK2_skl(sK3_skl(initial_world)))
| ~ reachable(initial_world,sK3_skl(initial_world))
| q(sK1_skl(sK3_skl(initial_world))) ),
inference(resolution,[status(thm)],[f998,f41]) ).
fof(f1347,plain,
! [X0] :
( ~ sQ77_spl
| ~ reachable(X0,sK0_skl(sK3_skl(initial_world)))
| ~ reachable(initial_world,X0)
| q(sK0_skl(sK0_skl(sK3_skl(initial_world)))) ),
inference(resolution,[status(thm)],[f998,f31]) ).
fof(f1354,definition,
( sQ129_spl
<=> reachable(initial_world,sK3_skl(initial_world)) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f1355,plain,
( ~ sQ129_spl
| reachable(initial_world,sK3_skl(initial_world)) ),
inference(component_clause,[status(thm)],[f1354]) ).
fof(f1356,plain,
( sQ129_spl
| ~ reachable(initial_world,sK3_skl(initial_world)) ),
inference(component_clause,[status(thm)],[f1354]) ).
fof(f1362,definition,
( sQ131_spl
<=> q(sK1_skl(sK3_skl(initial_world))) ),
introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition]) ).
fof(f1365,definition,
( sQ132_spl
<=> reachable(sK0_skl(sK3_skl(initial_world)),sK3_skl(sK3_skl(initial_world))) ),
introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition]) ).
fof(f1368,plain,
( ~ sQ77_spl
| sQ132_spl
| ~ sQ129_spl
| sQ131_spl ),
inference(split_clause,[status(thm)],[f1345,f1362,f1354,f1365,f997]) ).
fof(f1369,definition,
( sQ133_spl
<=> reachable(sK0_skl(sK3_skl(initial_world)),sK2_skl(sK3_skl(initial_world))) ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f1372,plain,
( ~ sQ77_spl
| sQ133_spl
| ~ sQ129_spl
| sQ131_spl ),
inference(split_clause,[status(thm)],[f1346,f1362,f1354,f1369,f997]) ).
fof(f1373,definition,
( sQ134_spl
<=> q(sK0_skl(sK0_skl(sK3_skl(initial_world)))) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f1376,definition,
! [X0] :
( sQ135_spl
<=> ( ~ reachable(X0,sK0_skl(sK3_skl(initial_world)))
| ~ reachable(initial_world,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ135_spl])],[split_symbol_definition]) ).
fof(f1377,plain,
! [X0] :
( ~ sQ135_spl
| ~ reachable(X0,sK0_skl(sK3_skl(initial_world)))
| ~ reachable(initial_world,X0) ),
inference(component_clause,[status(thm)],[f1376]) ).
fof(f1379,plain,
( ~ sQ77_spl
| sQ135_spl
| sQ134_spl ),
inference(split_clause,[status(thm)],[f1347,f1373,f1376,f997]) ).
fof(f1381,plain,
! [X0] :
( sQ129_spl
| ~ reachable(X0,sK3_skl(initial_world))
| ~ reachable(initial_world,X0) ),
inference(resolution,[status(thm)],[f1356,f8]) ).
fof(f1382,plain,
( sQ129_spl
| sQ54_spl ),
inference(split_clause,[status(thm)],[f1381,f458,f1354]) ).
fof(f1403,plain,
( ~ sQ129_spl
| reachable(sK3_skl(initial_world),sK0_skl(sK3_skl(initial_world))) ),
inference(resolution,[status(thm)],[f1355,f14]) ).
fof(f1407,plain,
( ~ sQ76_spl
| reachable(sK0_skl(sK3_skl(initial_world)),sK3_skl(sK3_skl(initial_world)))
| ~ reachable(initial_world,sK3_skl(initial_world))
| p(sK1_skl(sK3_skl(initial_world))) ),
inference(resolution,[status(thm)],[f995,f50]) ).
fof(f1408,plain,
( ~ sQ76_spl
| reachable(sK0_skl(sK3_skl(initial_world)),sK2_skl(sK3_skl(initial_world)))
| ~ reachable(initial_world,sK3_skl(initial_world))
| p(sK1_skl(sK3_skl(initial_world))) ),
inference(resolution,[status(thm)],[f995,f41]) ).
fof(f1409,plain,
! [X0] :
( ~ sQ76_spl
| ~ reachable(X0,sK0_skl(sK3_skl(initial_world)))
| ~ reachable(initial_world,X0)
| p(sK0_skl(sK0_skl(sK3_skl(initial_world)))) ),
inference(resolution,[status(thm)],[f995,f31]) ).
fof(f1421,definition,
( sQ138_spl
<=> p(sK1_skl(sK3_skl(initial_world))) ),
introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition]) ).
fof(f1422,plain,
( ~ sQ138_spl
| p(sK1_skl(sK3_skl(initial_world))) ),
inference(component_clause,[status(thm)],[f1421]) ).
fof(f1424,plain,
( ~ sQ76_spl
| sQ132_spl
| ~ sQ129_spl
| sQ138_spl ),
inference(split_clause,[status(thm)],[f1407,f1421,f1354,f1365,f994]) ).
fof(f1425,plain,
( ~ sQ76_spl
| sQ133_spl
| ~ sQ129_spl
| sQ138_spl ),
inference(split_clause,[status(thm)],[f1408,f1421,f1354,f1369,f994]) ).
fof(f1426,definition,
( sQ139_spl
<=> p(sK0_skl(sK0_skl(sK3_skl(initial_world)))) ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f1429,plain,
( ~ sQ76_spl
| sQ135_spl
| sQ139_spl ),
inference(split_clause,[status(thm)],[f1409,f1426,f1376,f994]) ).
fof(f1430,plain,
! [X0] :
( ~ sQ138_spl
| sP0_prd(sK1_skl(sK3_skl(initial_world)),X0) ),
inference(resolution,[status(thm)],[f1422,f25]) ).
fof(f1431,plain,
( ~ sQ138_spl
| reachable(sK0_skl(sK3_skl(initial_world)),sK3_skl(sK3_skl(initial_world)))
| ~ reachable(initial_world,sK3_skl(initial_world)) ),
inference(resolution,[status(thm)],[f1430,f18]) ).
fof(f1432,plain,
( ~ sQ138_spl
| reachable(sK0_skl(sK3_skl(initial_world)),sK2_skl(sK3_skl(initial_world)))
| ~ reachable(initial_world,sK3_skl(initial_world)) ),
inference(resolution,[status(thm)],[f1430,f16]) ).
fof(f1434,plain,
( ~ sQ138_spl
| sQ132_spl
| ~ sQ129_spl ),
inference(split_clause,[status(thm)],[f1431,f1354,f1365,f1421]) ).
fof(f1435,plain,
( ~ sQ138_spl
| sQ133_spl
| ~ sQ129_spl ),
inference(split_clause,[status(thm)],[f1432,f1354,f1369,f1421]) ).
fof(f1522,plain,
( ~ sQ117_spl
| p(sK1_skl(sK0_skl(initial_world))) ),
inference(resolution,[status(thm)],[f1262,f5]) ).
fof(f1527,plain,
( ~ sQ117_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f1522,f303,f1261]) ).
fof(f1561,plain,
( ~ sQ29_spl
| ~ sQ60_spl
| ~ reachable(initial_world,sK0_skl(sK0_skl(initial_world))) ),
inference(resolution,[status(thm)],[f817,f230]) ).
fof(f1562,plain,
! [X0,X1] :
( ~ sQ60_spl
| q(X1)
| ~ reachable(sK0_skl(sK0_skl(initial_world)),X1)
| p(X0)
| ~ reachable(sK0_skl(sK0_skl(initial_world)),X0)
| ~ reachable(initial_world,sK0_skl(initial_world))
| ~ reachable(initial_world,sK0_skl(sK0_skl(initial_world))) ),
inference(resolution,[status(thm)],[f817,f42]) ).
fof(f1565,plain,
( ~ sQ29_spl
| ~ sQ60_spl
| ~ sQ102_spl ),
inference(split_clause,[status(thm)],[f1561,f1152,f816,f229]) ).
fof(f1566,plain,
( ~ sQ60_spl
| sQ4_spl
| sQ3_spl
| ~ sQ25_spl
| ~ sQ102_spl ),
inference(split_clause,[status(thm)],[f1562,f1152,f214,f60,f63,f816]) ).
fof(f1567,plain,
( ~ sQ28_spl
| ~ sQ63_spl
| ~ reachable(initial_world,sK0_skl(sK0_skl(initial_world))) ),
inference(resolution,[status(thm)],[f844,f226]) ).
fof(f1571,plain,
( ~ sQ28_spl
| ~ sQ63_spl
| ~ sQ102_spl ),
inference(split_clause,[status(thm)],[f1567,f1152,f843,f225]) ).
fof(f1586,plain,
( ~ sQ64_spl
| ~ sQ70_spl
| q(sK3_skl(sK2_skl(initial_world))) ),
inference(resolution,[status(thm)],[f959,f930]) ).
fof(f1587,plain,
( ~ sQ64_spl
| ~ sQ70_spl
| ~ sP0_prd(sK1_skl(sK2_skl(initial_world)),sK0_skl(sK2_skl(initial_world)))
| ~ reachable(initial_world,sK2_skl(initial_world)) ),
inference(resolution,[status(thm)],[f1586,f19]) ).
fof(f1588,definition,
( sQ147_spl
<=> sP0_prd(sK1_skl(sK2_skl(initial_world)),sK0_skl(sK2_skl(initial_world))) ),
introduced(definition,[new_symbols(definition,[sQ147_spl])],[split_symbol_definition]) ).
fof(f1590,plain,
( sQ147_spl
| ~ sP0_prd(sK1_skl(sK2_skl(initial_world)),sK0_skl(sK2_skl(initial_world))) ),
inference(component_clause,[status(thm)],[f1588]) ).
fof(f1591,plain,
( ~ sQ64_spl
| ~ sQ70_spl
| ~ sQ147_spl
| ~ sQ66_spl ),
inference(split_clause,[status(thm)],[f1587,f944,f1588,f958,f929]) ).
fof(f1594,plain,
( ~ sQ79_spl
| reachable(sK0_skl(sK0_skl(sK0_skl(initial_world))),sK3_skl(sK0_skl(sK0_skl(initial_world))))
| ~ reachable(initial_world,sK0_skl(sK0_skl(initial_world)))
| p(sK1_skl(sK0_skl(sK0_skl(initial_world)))) ),
inference(resolution,[status(thm)],[f1005,f50]) ).
fof(f1595,plain,
( ~ sQ79_spl
| reachable(sK0_skl(sK0_skl(sK0_skl(initial_world))),sK2_skl(sK0_skl(sK0_skl(initial_world))))
| ~ reachable(initial_world,sK0_skl(sK0_skl(initial_world)))
| p(sK1_skl(sK0_skl(sK0_skl(initial_world)))) ),
inference(resolution,[status(thm)],[f1005,f41]) ).
fof(f1596,plain,
! [X0] :
( ~ sQ79_spl
| ~ reachable(X0,sK0_skl(sK0_skl(sK0_skl(initial_world))))
| ~ reachable(initial_world,X0)
| p(sK0_skl(sK0_skl(sK0_skl(sK0_skl(initial_world))))) ),
inference(resolution,[status(thm)],[f1005,f31]) ).
fof(f1608,definition,
( sQ150_spl
<=> p(sK1_skl(sK0_skl(sK0_skl(initial_world)))) ),
introduced(definition,[new_symbols(definition,[sQ150_spl])],[split_symbol_definition]) ).
fof(f1609,plain,
( ~ sQ150_spl
| p(sK1_skl(sK0_skl(sK0_skl(initial_world)))) ),
inference(component_clause,[status(thm)],[f1608]) ).
fof(f1611,plain,
( ~ sQ79_spl
| sQ105_spl
| ~ sQ102_spl
| sQ150_spl ),
inference(split_clause,[status(thm)],[f1594,f1608,f1152,f1163,f1004]) ).
fof(f1612,plain,
( ~ sQ79_spl
| sQ106_spl
| ~ sQ102_spl
| sQ150_spl ),
inference(split_clause,[status(thm)],[f1595,f1608,f1152,f1167,f1004]) ).
fof(f1613,definition,
( sQ151_spl
<=> p(sK0_skl(sK0_skl(sK0_skl(sK0_skl(initial_world))))) ),
introduced(definition,[new_symbols(definition,[sQ151_spl])],[split_symbol_definition]) ).
fof(f1616,plain,
( ~ sQ79_spl
| sQ108_spl
| sQ151_spl ),
inference(split_clause,[status(thm)],[f1596,f1613,f1174,f1004]) ).
fof(f1617,plain,
! [X0] :
( ~ sQ150_spl
| sP0_prd(sK1_skl(sK0_skl(sK0_skl(initial_world))),X0) ),
inference(resolution,[status(thm)],[f1609,f25]) ).
fof(f1618,plain,
( ~ sQ150_spl
| reachable(sK0_skl(sK0_skl(sK0_skl(initial_world))),sK3_skl(sK0_skl(sK0_skl(initial_world))))
| ~ reachable(initial_world,sK0_skl(sK0_skl(initial_world))) ),
inference(resolution,[status(thm)],[f1617,f18]) ).
fof(f1619,plain,
( ~ sQ150_spl
| reachable(sK0_skl(sK0_skl(sK0_skl(initial_world))),sK2_skl(sK0_skl(sK0_skl(initial_world))))
| ~ reachable(initial_world,sK0_skl(sK0_skl(initial_world))) ),
inference(resolution,[status(thm)],[f1617,f16]) ).
fof(f1621,plain,
( ~ sQ150_spl
| sQ105_spl
| ~ sQ102_spl ),
inference(split_clause,[status(thm)],[f1618,f1152,f1163,f1608]) ).
fof(f1622,plain,
( ~ sQ150_spl
| sQ106_spl
| ~ sQ102_spl ),
inference(split_clause,[status(thm)],[f1619,f1152,f1167,f1608]) ).
fof(f1671,plain,
! [X0,X1] :
( sQ46_spl
| q(X1)
| ~ reachable(sK0_skl(sK0_skl(initial_world)),X1)
| p(X0)
| ~ reachable(sK0_skl(sK0_skl(initial_world)),X0)
| ~ reachable(initial_world,sK0_skl(initial_world)) ),
inference(resolution,[status(thm)],[f376,f15]) ).
fof(f1672,plain,
( sQ46_spl
| reachable(sK0_skl(sK0_skl(initial_world)),sK1_skl(sK0_skl(initial_world))) ),
inference(resolution,[status(thm)],[f376,f24]) ).
fof(f1673,plain,
( sQ46_spl
| sQ4_spl
| sQ3_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f1671,f214,f60,f63,f374]) ).
fof(f1689,plain,
( ~ sQ129_spl
| ~ sQ135_spl
| ~ reachable(initial_world,sK3_skl(initial_world)) ),
inference(resolution,[status(thm)],[f1377,f1403]) ).
fof(f1693,plain,
( ~ sQ135_spl
| ~ sQ129_spl ),
inference(split_clause,[status(thm)],[f1689,f1354,f1376]) ).
fof(f1695,plain,
! [X0] :
( ~ sQ29_spl
| ~ sQ3_spl
| ~ reachable(sK2_skl(sK0_skl(initial_world)),X0)
| p(X0) ),
inference(resolution,[status(thm)],[f293,f230]) ).
fof(f1696,plain,
! [X0] :
( ~ sQ28_spl
| ~ sQ3_spl
| ~ reachable(sK3_skl(sK0_skl(initial_world)),X0)
| p(X0) ),
inference(resolution,[status(thm)],[f293,f226]) ).
fof(f1726,plain,
! [X0] :
( ~ sQ29_spl
| ~ sQ3_spl
| ~ reachable(X0,sK2_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,X0)
| p(sK0_skl(sK2_skl(sK0_skl(initial_world)))) ),
inference(resolution,[status(thm)],[f1695,f31]) ).
fof(f1730,definition,
( sQ156_spl
<=> p(sK0_skl(sK2_skl(sK0_skl(initial_world)))) ),
introduced(definition,[new_symbols(definition,[sQ156_spl])],[split_symbol_definition]) ).
fof(f1733,plain,
( ~ sQ29_spl
| ~ sQ3_spl
| sQ60_spl
| sQ156_spl ),
inference(split_clause,[status(thm)],[f1726,f1730,f816,f60,f229]) ).
fof(f1743,plain,
! [X0] :
( ~ sQ28_spl
| ~ sQ3_spl
| ~ reachable(X0,sK3_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,X0)
| p(sK0_skl(sK3_skl(sK0_skl(initial_world)))) ),
inference(resolution,[status(thm)],[f1696,f31]) ).
fof(f1747,definition,
( sQ159_spl
<=> p(sK0_skl(sK3_skl(sK0_skl(initial_world)))) ),
introduced(definition,[new_symbols(definition,[sQ159_spl])],[split_symbol_definition]) ).
fof(f1750,plain,
( ~ sQ28_spl
| ~ sQ3_spl
| sQ63_spl
| sQ159_spl ),
inference(split_clause,[status(thm)],[f1743,f1747,f843,f60,f225]) ).
fof(f1761,plain,
( sQ147_spl
| reachable(sK0_skl(sK2_skl(initial_world)),sK1_skl(sK2_skl(initial_world))) ),
inference(resolution,[status(thm)],[f1590,f24]) ).
fof(f1787,plain,
! [X0] :
( ~ sQ3_spl
| sQ46_spl
| ~ reachable(sK1_skl(sK0_skl(initial_world)),X0)
| p(X0) ),
inference(resolution,[status(thm)],[f1672,f293]) ).
fof(f1788,plain,
( ~ sQ3_spl
| sQ46_spl
| p(sK1_skl(sK0_skl(initial_world))) ),
inference(resolution,[status(thm)],[f1672,f61]) ).
fof(f1789,plain,
( ~ sQ3_spl
| sQ46_spl
| sQ117_spl ),
inference(split_clause,[status(thm)],[f1787,f1261,f374,f60]) ).
fof(f1790,plain,
( ~ sQ3_spl
| sQ46_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f1788,f303,f374,f60]) ).
fof(f1793,plain,
( ~ sQ28_spl
| ~ sQ4_spl
| q(sK3_skl(sK0_skl(initial_world))) ),
inference(resolution,[status(thm)],[f64,f226]) ).
fof(f1807,plain,
! [X0] :
( sQ46_spl
| ~ sQ4_spl
| ~ reachable(sK1_skl(sK0_skl(initial_world)),X0)
| q(X0) ),
inference(resolution,[status(thm)],[f209,f1672]) ).
fof(f1812,plain,
! [X0] :
( ~ sQ4_spl
| reachable(sK0_skl(sK0_skl(initial_world)),sK3_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,sK0_skl(initial_world))
| ~ reachable(sK1_skl(sK0_skl(initial_world)),X0)
| q(X0) ),
inference(resolution,[status(thm)],[f209,f50]) ).
fof(f1814,plain,
! [X0,X1] :
( ~ sQ4_spl
| ~ reachable(X1,sK0_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,X1)
| ~ reachable(sK0_skl(sK0_skl(sK0_skl(initial_world))),X0)
| q(X0) ),
inference(resolution,[status(thm)],[f209,f31]) ).
fof(f1818,plain,
( sQ46_spl
| ~ sQ4_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f1807,f344,f63,f374]) ).
fof(f1821,plain,
( ~ sQ4_spl
| sQ28_spl
| ~ sQ25_spl
| sQ44_spl ),
inference(split_clause,[status(thm)],[f1812,f344,f214,f225,f63]) ).
fof(f1823,plain,
( ~ sQ4_spl
| sQ31_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f1814,f349,f236,f63]) ).
fof(f1824,plain,
( ~ sQ28_spl
| ~ sQ4_spl
| ~ sP0_prd(sK1_skl(sK0_skl(initial_world)),sK0_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,sK0_skl(initial_world)) ),
inference(resolution,[status(thm)],[f1793,f19]) ).
fof(f1825,plain,
( ~ sQ28_spl
| ~ sQ4_spl
| ~ sQ46_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f1824,f214,f374,f63,f225]) ).
fof(f1859,plain,
! [X0] :
( sQ147_spl
| ~ sQ64_spl
| ~ reachable(sK1_skl(sK2_skl(initial_world)),X0)
| q(X0) ),
inference(resolution,[status(thm)],[f939,f1761]) ).
fof(f1864,plain,
! [X0] :
( ~ sQ64_spl
| reachable(sK0_skl(sK2_skl(initial_world)),sK3_skl(sK2_skl(initial_world)))
| ~ reachable(initial_world,sK2_skl(initial_world))
| ~ reachable(sK1_skl(sK2_skl(initial_world)),X0)
| q(X0) ),
inference(resolution,[status(thm)],[f939,f50]) ).
fof(f1878,plain,
( ~ sQ64_spl
| sQ70_spl
| ~ sQ66_spl
| sQ125_spl ),
inference(split_clause,[status(thm)],[f1864,f1330,f944,f958,f929]) ).
fof(f1882,plain,
! [X0] :
( sQ147_spl
| ~ sQ64_spl
| sP0_prd(sK1_skl(sK2_skl(initial_world)),X0)
| q(sK4_skl(sK1_skl(sK2_skl(initial_world)),X0)) ),
inference(resolution,[status(thm)],[f1859,f26]) ).
fof(f1892,plain,
( sQ147_spl
| ~ sQ64_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1590,f1893]) ).
fof(f1893,plain,
! [X0] :
( sQ147_spl
| ~ sQ64_spl
| sP0_prd(sK1_skl(sK2_skl(initial_world)),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1882,f27]) ).
fof(f1894,plain,
( sQ147_spl
| ~ sQ64_spl ),
inference(contradiction_clause,[status(thm)],[f1892]) ).
fof(f1908,plain,
! [X0] :
( ~ sQ125_spl
| sP0_prd(sK1_skl(sK2_skl(initial_world)),X0)
| q(sK4_skl(sK1_skl(sK2_skl(initial_world)),X0)) ),
inference(resolution,[status(thm)],[f1331,f26]) ).
fof(f1912,plain,
! [X0] :
( ~ sQ125_spl
| sP0_prd(sK1_skl(sK2_skl(initial_world)),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1908,f27]) ).
fof(f1913,plain,
( ~ sQ125_spl
| reachable(sK0_skl(sK2_skl(initial_world)),sK3_skl(sK2_skl(initial_world)))
| ~ reachable(initial_world,sK2_skl(initial_world)) ),
inference(resolution,[status(thm)],[f1912,f18]) ).
fof(f1916,plain,
( ~ sQ125_spl
| sQ70_spl
| ~ sQ66_spl ),
inference(split_clause,[status(thm)],[f1913,f944,f958,f1330]) ).
fof(f1953,plain,
! [X0] :
( ~ sQ7_spl
| ~ reachable(sK0_skl(sK0_skl(initial_world)),X0)
| q(X0) ),
inference(resolution,[status(thm)],[f115,f29]) ).
fof(f1963,plain,
( ~ sQ7_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f1953,f63,f74]) ).
fof(f1991,plain,
( ~ sQ44_spl
| reachable(sK0_skl(sK0_skl(initial_world)),sK3_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,sK0_skl(initial_world)) ),
inference(resolution,[status(thm)],[f570,f18]) ).
fof(f1992,plain,
( ~ sQ44_spl
| reachable(sK0_skl(sK0_skl(initial_world)),sK2_skl(sK0_skl(initial_world)))
| ~ reachable(initial_world,sK0_skl(initial_world)) ),
inference(resolution,[status(thm)],[f570,f16]) ).
fof(f1994,plain,
( ~ sQ44_spl
| sQ28_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f1991,f214,f225,f344]) ).
fof(f1995,plain,
( ~ sQ44_spl
| sQ29_spl
| ~ sQ25_spl ),
inference(split_clause,[status(thm)],[f1992,f214,f229,f344]) ).
fof(f1997,plain,
$false,
inference(sat_refutation,[status(thm)],[f39,f46,f66,f77,f148,f157,f178,f179,f183,f188,f189,f241,f256,f261,f268,f274,f306,f307,f311,f343,f347,f348,f352,f353,f355,f377,f379,f426,f461,f472,f497,f499,f517,f555,f571,f575,f692,f727,f733,f819,f822,f846,f920,f922,f924,f932,f975,f1000,f1037,f1075,f1166,f1170,f1177,f1191,f1195,f1201,f1218,f1219,f1231,f1266,f1368,f1372,f1379,f1382,f1424,f1425,f1429,f1434,f1435,f1527,f1565,f1566,f1571,f1591,f1611,f1612,f1616,f1621,f1622,f1673,f1693,f1733,f1750,f1789,f1790,f1818,f1821,f1823,f1825,f1878,f1894,f1916,f1963,f1994,f1995]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SYN548+1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n017.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.43 % CPULimit : 300
% 0.15/0.43 % WCLimit : 300
% 0.15/0.43 % DateTime : Mon Sep 21 11:02:42 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.44 % Drodi V4.1.1
% 15.48/2.47 % Refutation found
% 15.48/2.47 % SZS status Theorem for theBenchmark: Theorem is valid
% 15.48/2.47 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 15.48/2.50 % Elapsed time: 2.062072 seconds
% 15.48/2.50 % CPU time: 15.967372 seconds
% 15.48/2.50 % Total memory used: 62.707 MB
% 15.48/2.50 % Net memory used: 51.280 MB
%------------------------------------------------------------------------------