%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYN550+1 : TPTP v9.0.0. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 10:03:53 PM UTC 2025
% Result : Theorem 9.02s 3.19s
% Output : CNFRefutation 9.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 3
% Syntax : Number of formulae : 354 ( 105 unt; 0 typ; 0 def)
% Number of atoms : 777 ( 0 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 911 ( 488 ~; 414 |; 4 &)
% ( 1 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 297 ( 294 !; 3 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ reachable > p > #nlpp > initial_world > #skF_5 > #skF_2 > #skF_3 > #skF_1 > #skF_4 > #skF_6
%Foreground sorts:
%Background operators:
%Foreground operators:
tff('#skF_5',type,
'#skF_5': $i > $i ).
tff('#skF_2',type,
'#skF_2': $i > $i ).
tff('#skF_3',type,
'#skF_3': ( $i * $i ) > $i ).
tff(p,type,
p: $i > $o ).
tff('#skF_1',type,
'#skF_1': $i ).
tff(initial_world,type,
initial_world: $i ).
tff(reachable,type,
reachable: ( $i * $i ) > $o ).
tff('#skF_4',type,
'#skF_4': $i ).
tff('#skF_6',type,
'#skF_6': $i > $i ).
tff(f_36,axiom,
! [X] : reachable(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_of_reachable) ).
tff(f_67,negated_conjecture,
~ ( ? [X] :
( reachable(initial_world,X)
& ! [Y] :
( reachable(X,Y)
=> p(Y) ) )
<=> ? [X] :
( reachable(initial_world,X)
& ! [Y] :
( reachable(X,Y)
=> ? [Z] :
( reachable(Y,Z)
& ! [W] :
( reachable(Z,W)
=> p(W) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this) ).
tff(f_42,axiom,
! [X,Y,Z] :
( ( reachable(X,Y)
& reachable(Y,Z) )
=> reachable(X,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',transitivity_of_reachable) ).
tff(c_2,plain,
! [X_1] : reachable(X_1,X_1),
inference(cnfTransformation,[status(thm)],[f_36]) ).
tff(c_48,plain,
( reachable(initial_world,'#skF_1')
| reachable(initial_world,'#skF_4') ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_56,plain,
reachable(initial_world,'#skF_4'),
inference(splitLeft,[status(thm)],[c_48]) ).
tff(c_18,plain,
! [X_33] :
( reachable(initial_world,'#skF_1')
| reachable(X_33,'#skF_6'(X_33))
| ~ reachable(initial_world,X_33) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_75,plain,
reachable(initial_world,'#skF_1'),
inference(splitLeft,[status(thm)],[c_18]) ).
tff(c_20,plain,
! [X_7,X_33] :
( reachable(X_7,'#skF_2'(X_7))
| ~ reachable(initial_world,X_7)
| reachable(X_33,'#skF_6'(X_33))
| ~ reachable(initial_world,X_33) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_2185,plain,
! [X_142] :
( reachable(X_142,'#skF_6'(X_142))
| ~ reachable(initial_world,X_142) ),
inference(splitLeft,[status(thm)],[c_20]) ).
tff(c_472,plain,
! [X_84] :
( reachable(X_84,'#skF_6'(X_84))
| ~ reachable(initial_world,X_84) ),
inference(splitLeft,[status(thm)],[c_20]) ).
tff(c_16,plain,
! [Y_6,X_33] :
( p(Y_6)
| ~ reachable('#skF_1',Y_6)
| reachable(X_33,'#skF_6'(X_33))
| ~ reachable(initial_world,X_33) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_97,plain,
! [X_33] :
( reachable(X_33,'#skF_6'(X_33))
| ~ reachable(initial_world,X_33) ),
inference(splitLeft,[status(thm)],[c_16]) ).
tff(c_36,plain,
! [Y_6,Y_27] :
( p(Y_6)
| ~ reachable('#skF_1',Y_6)
| reachable(Y_27,'#skF_5'(Y_27))
| ~ reachable('#skF_4',Y_27) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_88,plain,
! [Y_42] :
( reachable(Y_42,'#skF_5'(Y_42))
| ~ reachable('#skF_4',Y_42) ),
inference(splitLeft,[status(thm)],[c_36]) ).
tff(c_4,plain,
! [X_2,Z_4,Y_3] :
( reachable(X_2,Z_4)
| ~ reachable(Y_3,Z_4)
| ~ reachable(X_2,Y_3) ),
inference(cnfTransformation,[status(thm)],[f_42]) ).
tff(c_92,plain,
! [X_43,Y_44] :
( reachable(X_43,'#skF_5'(Y_44))
| ~ reachable(X_43,Y_44)
| ~ reachable('#skF_4',Y_44) ),
inference(resolution,[status(thm)],[c_88,c_4]) ).
tff(c_106,plain,
! [X_48,Y_49,X_50] :
( reachable(X_48,'#skF_5'(Y_49))
| ~ reachable(X_48,X_50)
| ~ reachable(X_50,Y_49)
| ~ reachable('#skF_4',Y_49) ),
inference(resolution,[status(thm)],[c_92,c_4]) ).
tff(c_126,plain,
! [Y_49] :
( reachable(initial_world,'#skF_5'(Y_49))
| ~ reachable('#skF_4',Y_49) ),
inference(resolution,[status(thm)],[c_56,c_106]) ).
tff(c_26,plain,
! [Y_6,W_32,Y_27] :
( p(Y_6)
| ~ reachable('#skF_1',Y_6)
| p(W_32)
| ~ reachable('#skF_5'(Y_27),W_32)
| ~ reachable('#skF_4',Y_27) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_252,plain,
! [W_66,Y_67] :
( p(W_66)
| ~ reachable('#skF_5'(Y_67),W_66)
| ~ reachable('#skF_4',Y_67) ),
inference(splitLeft,[status(thm)],[c_26]) ).
tff(c_294,plain,
! [Y_69] :
( p('#skF_6'('#skF_5'(Y_69)))
| ~ reachable('#skF_4',Y_69)
| ~ reachable(initial_world,'#skF_5'(Y_69)) ),
inference(resolution,[status(thm)],[c_97,c_252]) ).
tff(c_8,plain,
! [X_33] :
( reachable(initial_world,'#skF_1')
| ~ p('#skF_6'(X_33))
| ~ reachable(initial_world,X_33) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_58,plain,
! [X_33] :
( ~ p('#skF_6'(X_33))
| ~ reachable(initial_world,X_33) ),
inference(splitLeft,[status(thm)],[c_8]) ).
tff(c_299,plain,
! [Y_70] :
( ~ reachable('#skF_4',Y_70)
| ~ reachable(initial_world,'#skF_5'(Y_70)) ),
inference(resolution,[status(thm)],[c_294,c_58]) ).
tff(c_321,plain,
! [Y_71] : ~ reachable('#skF_4',Y_71),
inference(resolution,[status(thm)],[c_126,c_299]) ).
tff(c_333,plain,
~ reachable(initial_world,'#skF_4'),
inference(resolution,[status(thm)],[c_97,c_321]) ).
tff(c_342,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_56,c_333]) ).
tff(c_344,plain,
! [Y_72] :
( p(Y_72)
| ~ reachable('#skF_1',Y_72) ),
inference(splitRight,[status(thm)],[c_26]) ).
tff(c_364,plain,
( p('#skF_6'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_97,c_344]) ).
tff(c_383,plain,
p('#skF_6'('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_75,c_364]) ).
tff(c_389,plain,
~ reachable(initial_world,'#skF_1'),
inference(resolution,[status(thm)],[c_383,c_58]) ).
tff(c_393,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_75,c_389]) ).
tff(c_394,plain,
! [Y_6] :
( p(Y_6)
| ~ reachable('#skF_1',Y_6) ),
inference(splitRight,[status(thm)],[c_16]) ).
tff(c_480,plain,
( p('#skF_6'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_472,c_394]) ).
tff(c_487,plain,
p('#skF_6'('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_75,c_480]) ).
tff(c_491,plain,
~ reachable(initial_world,'#skF_1'),
inference(resolution,[status(thm)],[c_487,c_58]) ).
tff(c_495,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_75,c_491]) ).
tff(c_497,plain,
! [X_85] :
( reachable(X_85,'#skF_2'(X_85))
| ~ reachable(initial_world,X_85) ),
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_514,plain,
! [X_86,X_87] :
( reachable(X_86,'#skF_2'(X_87))
| ~ reachable(X_86,X_87)
| ~ reachable(initial_world,X_87) ),
inference(resolution,[status(thm)],[c_497,c_4]) ).
tff(c_530,plain,
! [X_89,X_90,X_91] :
( reachable(X_89,'#skF_2'(X_90))
| ~ reachable(X_89,X_91)
| ~ reachable(X_91,X_90)
| ~ reachable(initial_world,X_90) ),
inference(resolution,[status(thm)],[c_514,c_4]) ).
tff(c_558,plain,
! [X_92] :
( reachable(initial_world,'#skF_2'(X_92))
| ~ reachable('#skF_1',X_92)
| ~ reachable(initial_world,X_92) ),
inference(resolution,[status(thm)],[c_75,c_530]) ).
tff(c_570,plain,
! [X_2,X_92] :
( reachable(X_2,'#skF_2'(X_92))
| ~ reachable(X_2,initial_world)
| ~ reachable('#skF_1',X_92)
| ~ reachable(initial_world,X_92) ),
inference(resolution,[status(thm)],[c_558,c_4]) ).
tff(c_496,plain,
! [X_7] :
( reachable(X_7,'#skF_2'(X_7))
| ~ reachable(initial_world,X_7) ),
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_760,plain,
! [X_104,X_105] :
( reachable(X_104,'#skF_2'(X_105))
| ~ reachable('#skF_2'(X_104),X_105)
| ~ reachable(initial_world,X_105)
| ~ reachable(initial_world,X_104) ),
inference(resolution,[status(thm)],[c_496,c_530]) ).
tff(c_811,plain,
! [X_106] :
( reachable(X_106,'#skF_2'('#skF_2'(X_106)))
| ~ reachable(initial_world,'#skF_2'(X_106))
| ~ reachable(initial_world,X_106) ),
inference(resolution,[status(thm)],[c_2,c_760]) ).
tff(c_833,plain,
( p('#skF_2'('#skF_2'('#skF_1')))
| ~ reachable(initial_world,'#skF_2'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_811,c_394]) ).
tff(c_844,plain,
( p('#skF_2'('#skF_2'('#skF_1')))
| ~ reachable(initial_world,'#skF_2'('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_75,c_833]) ).
tff(c_846,plain,
~ reachable(initial_world,'#skF_2'('#skF_1')),
inference(splitLeft,[status(thm)],[c_844]) ).
tff(c_852,plain,
( ~ reachable(initial_world,initial_world)
| ~ reachable('#skF_1','#skF_1')
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_570,c_846]) ).
tff(c_868,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_75,c_2,c_2,c_852]) ).
tff(c_870,plain,
reachable(initial_world,'#skF_2'('#skF_1')),
inference(splitRight,[status(thm)],[c_844]) ).
tff(c_810,plain,
! [X_104] :
( reachable(X_104,'#skF_2'('#skF_2'(X_104)))
| ~ reachable(initial_world,'#skF_2'(X_104))
| ~ reachable(initial_world,X_104) ),
inference(resolution,[status(thm)],[c_2,c_760]) ).
tff(c_24,plain,
! [Z_18,X_7,X_33] :
( reachable(Z_18,'#skF_3'(X_7,Z_18))
| ~ reachable('#skF_2'(X_7),Z_18)
| ~ reachable(initial_world,X_7)
| reachable(X_33,'#skF_6'(X_33))
| ~ reachable(initial_world,X_33) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_1389,plain,
! [X_121] :
( reachable(X_121,'#skF_6'(X_121))
| ~ reachable(initial_world,X_121) ),
inference(splitLeft,[status(thm)],[c_24]) ).
tff(c_1423,plain,
( p('#skF_6'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_1389,c_394]) ).
tff(c_1440,plain,
p('#skF_6'('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_75,c_1423]) ).
tff(c_1444,plain,
~ reachable(initial_world,'#skF_1'),
inference(resolution,[status(thm)],[c_1440,c_58]) ).
tff(c_1448,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_75,c_1444]) ).
tff(c_1450,plain,
! [Z_122,X_123] :
( reachable(Z_122,'#skF_3'(X_123,Z_122))
| ~ reachable('#skF_2'(X_123),Z_122)
| ~ reachable(initial_world,X_123) ),
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_1511,plain,
! [X_124] :
( reachable('#skF_2'(X_124),'#skF_3'(X_124,'#skF_2'(X_124)))
| ~ reachable(initial_world,X_124) ),
inference(resolution,[status(thm)],[c_2,c_1450]) ).
tff(c_1925,plain,
! [X_135,X_136] :
( reachable(X_135,'#skF_3'(X_136,'#skF_2'(X_136)))
| ~ reachable(X_135,'#skF_2'(X_136))
| ~ reachable(initial_world,X_136) ),
inference(resolution,[status(thm)],[c_1511,c_4]) ).
tff(c_1986,plain,
! [X_137] :
( p('#skF_3'(X_137,'#skF_2'(X_137)))
| ~ reachable('#skF_1','#skF_2'(X_137))
| ~ reachable(initial_world,X_137) ),
inference(resolution,[status(thm)],[c_1925,c_394]) ).
tff(c_22,plain,
! [X_7,Z_18,X_33] :
( ~ p('#skF_3'(X_7,Z_18))
| ~ reachable('#skF_2'(X_7),Z_18)
| ~ reachable(initial_world,X_7)
| reachable(X_33,'#skF_6'(X_33))
| ~ reachable(initial_world,X_33) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_1184,plain,
! [X_114,Z_115] :
( ~ p('#skF_3'(X_114,Z_115))
| ~ reachable('#skF_2'(X_114),Z_115)
| ~ reachable(initial_world,X_114) ),
inference(splitLeft,[status(thm)],[c_22]) ).
tff(c_1254,plain,
! [X_114] :
( ~ p('#skF_3'(X_114,'#skF_2'(X_114)))
| ~ reachable(initial_world,X_114) ),
inference(resolution,[status(thm)],[c_2,c_1184]) ).
tff(c_1998,plain,
! [X_138] :
( ~ reachable('#skF_1','#skF_2'(X_138))
| ~ reachable(initial_world,X_138) ),
inference(resolution,[status(thm)],[c_1986,c_1254]) ).
tff(c_2026,plain,
( ~ reachable(initial_world,'#skF_2'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_810,c_1998]) ).
tff(c_2068,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_75,c_870,c_2026]) ).
tff(c_2124,plain,
! [X_140] :
( reachable(X_140,'#skF_6'(X_140))
| ~ reachable(initial_world,X_140) ),
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_2152,plain,
( p('#skF_6'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_2124,c_394]) ).
tff(c_2167,plain,
p('#skF_6'('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_75,c_2152]) ).
tff(c_2171,plain,
~ reachable(initial_world,'#skF_1'),
inference(resolution,[status(thm)],[c_2167,c_58]) ).
tff(c_2175,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_75,c_2171]) ).
tff(c_2176,plain,
! [Y_6] :
( p(Y_6)
| ~ reachable('#skF_1',Y_6) ),
inference(splitRight,[status(thm)],[c_36]) ).
tff(c_2189,plain,
( p('#skF_6'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_2185,c_2176]) ).
tff(c_2194,plain,
p('#skF_6'('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_75,c_2189]) ).
tff(c_2198,plain,
~ reachable(initial_world,'#skF_1'),
inference(resolution,[status(thm)],[c_2194,c_58]) ).
tff(c_2202,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_75,c_2198]) ).
tff(c_2204,plain,
! [X_143] :
( reachable(X_143,'#skF_2'(X_143))
| ~ reachable(initial_world,X_143) ),
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_2216,plain,
! [X_144,X_145] :
( reachable(X_144,'#skF_2'(X_145))
| ~ reachable(X_144,X_145)
| ~ reachable(initial_world,X_145) ),
inference(resolution,[status(thm)],[c_2204,c_4]) ).
tff(c_2226,plain,
! [X_147,X_148,X_149] :
( reachable(X_147,'#skF_2'(X_148))
| ~ reachable(X_147,X_149)
| ~ reachable(X_149,X_148)
| ~ reachable(initial_world,X_148) ),
inference(resolution,[status(thm)],[c_2216,c_4]) ).
tff(c_2242,plain,
! [X_150] :
( reachable(initial_world,'#skF_2'(X_150))
| ~ reachable('#skF_1',X_150)
| ~ reachable(initial_world,X_150) ),
inference(resolution,[status(thm)],[c_75,c_2226]) ).
tff(c_2248,plain,
! [X_2,X_150] :
( reachable(X_2,'#skF_2'(X_150))
| ~ reachable(X_2,initial_world)
| ~ reachable('#skF_1',X_150)
| ~ reachable(initial_world,X_150) ),
inference(resolution,[status(thm)],[c_2242,c_4]) ).
tff(c_2203,plain,
! [X_7] :
( reachable(X_7,'#skF_2'(X_7))
| ~ reachable(initial_world,X_7) ),
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_2282,plain,
! [X_156,X_157] :
( reachable(X_156,'#skF_2'(X_157))
| ~ reachable('#skF_2'(X_156),X_157)
| ~ reachable(initial_world,X_157)
| ~ reachable(initial_world,X_156) ),
inference(resolution,[status(thm)],[c_2203,c_2226]) ).
tff(c_2308,plain,
! [X_158] :
( reachable(X_158,'#skF_2'('#skF_2'(X_158)))
| ~ reachable(initial_world,'#skF_2'(X_158))
| ~ reachable(initial_world,X_158) ),
inference(resolution,[status(thm)],[c_2,c_2282]) ).
tff(c_2318,plain,
( p('#skF_2'('#skF_2'('#skF_1')))
| ~ reachable(initial_world,'#skF_2'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_2308,c_2176]) ).
tff(c_2325,plain,
( p('#skF_2'('#skF_2'('#skF_1')))
| ~ reachable(initial_world,'#skF_2'('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_75,c_2318]) ).
tff(c_2327,plain,
~ reachable(initial_world,'#skF_2'('#skF_1')),
inference(splitLeft,[status(thm)],[c_2325]) ).
tff(c_2333,plain,
( ~ reachable(initial_world,initial_world)
| ~ reachable('#skF_1','#skF_1')
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_2248,c_2327]) ).
tff(c_2349,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_75,c_2,c_2,c_2333]) ).
tff(c_2351,plain,
reachable(initial_world,'#skF_2'('#skF_1')),
inference(splitRight,[status(thm)],[c_2325]) ).
tff(c_2307,plain,
! [X_156] :
( reachable(X_156,'#skF_2'('#skF_2'(X_156)))
| ~ reachable(initial_world,'#skF_2'(X_156))
| ~ reachable(initial_world,X_156) ),
inference(resolution,[status(thm)],[c_2,c_2282]) ).
tff(c_3808,plain,
! [X_216] :
( reachable(X_216,'#skF_6'(X_216))
| ~ reachable(initial_world,X_216) ),
inference(splitLeft,[status(thm)],[c_24]) ).
tff(c_3834,plain,
( p('#skF_6'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_3808,c_2176]) ).
tff(c_3850,plain,
p('#skF_6'('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_75,c_3834]) ).
tff(c_3854,plain,
~ reachable(initial_world,'#skF_1'),
inference(resolution,[status(thm)],[c_3850,c_58]) ).
tff(c_3858,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_75,c_3854]) ).
tff(c_3904,plain,
! [Z_218,X_219] :
( reachable(Z_218,'#skF_3'(X_219,Z_218))
| ~ reachable('#skF_2'(X_219),Z_218)
| ~ reachable(initial_world,X_219) ),
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_3957,plain,
! [X_220] :
( reachable('#skF_2'(X_220),'#skF_3'(X_220,'#skF_2'(X_220)))
| ~ reachable(initial_world,X_220) ),
inference(resolution,[status(thm)],[c_2,c_3904]) ).
tff(c_4126,plain,
! [X_227,X_228] :
( reachable(X_227,'#skF_3'(X_228,'#skF_2'(X_228)))
| ~ reachable(X_227,'#skF_2'(X_228))
| ~ reachable(initial_world,X_228) ),
inference(resolution,[status(thm)],[c_3957,c_4]) ).
tff(c_4171,plain,
! [X_229] :
( p('#skF_3'(X_229,'#skF_2'(X_229)))
| ~ reachable('#skF_1','#skF_2'(X_229))
| ~ reachable(initial_world,X_229) ),
inference(resolution,[status(thm)],[c_4126,c_2176]) ).
tff(c_3557,plain,
! [X_206,Z_207] :
( ~ p('#skF_3'(X_206,Z_207))
| ~ reachable('#skF_2'(X_206),Z_207)
| ~ reachable(initial_world,X_206) ),
inference(splitLeft,[status(thm)],[c_22]) ).
tff(c_3612,plain,
! [X_206] :
( ~ p('#skF_3'(X_206,'#skF_2'(X_206)))
| ~ reachable(initial_world,X_206) ),
inference(resolution,[status(thm)],[c_2,c_3557]) ).
tff(c_4183,plain,
! [X_230] :
( ~ reachable('#skF_1','#skF_2'(X_230))
| ~ reachable(initial_world,X_230) ),
inference(resolution,[status(thm)],[c_4171,c_3612]) ).
tff(c_4211,plain,
( ~ reachable(initial_world,'#skF_2'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_2307,c_4183]) ).
tff(c_4249,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_75,c_2351,c_4211]) ).
tff(c_4252,plain,
! [X_231] :
( reachable(X_231,'#skF_6'(X_231))
| ~ reachable(initial_world,X_231) ),
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_4268,plain,
( p('#skF_6'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_4252,c_2176]) ).
tff(c_4279,plain,
p('#skF_6'('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_75,c_4268]) ).
tff(c_4283,plain,
~ reachable(initial_world,'#skF_1'),
inference(resolution,[status(thm)],[c_4279,c_58]) ).
tff(c_4287,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_75,c_4283]) ).
tff(c_4289,plain,
~ reachable(initial_world,'#skF_1'),
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_38,plain,
! [Y_27] :
( reachable(initial_world,'#skF_1')
| reachable(Y_27,'#skF_5'(Y_27))
| ~ reachable('#skF_4',Y_27) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_4295,plain,
! [Y_233] :
( reachable(Y_233,'#skF_5'(Y_233))
| ~ reachable('#skF_4',Y_233) ),
inference(negUnitSimplification,[status(thm)],[c_4289,c_38]) ).
tff(c_4298,plain,
! [X_2,Y_233] :
( reachable(X_2,'#skF_5'(Y_233))
| ~ reachable(X_2,Y_233)
| ~ reachable('#skF_4',Y_233) ),
inference(resolution,[status(thm)],[c_4295,c_4]) ).
tff(c_4288,plain,
! [X_33] :
( reachable(X_33,'#skF_6'(X_33))
| ~ reachable(initial_world,X_33) ),
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_28,plain,
! [W_32,Y_27] :
( reachable(initial_world,'#skF_1')
| p(W_32)
| ~ reachable('#skF_5'(Y_27),W_32)
| ~ reachable('#skF_4',Y_27) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_4308,plain,
! [W_238,Y_239] :
( p(W_238)
| ~ reachable('#skF_5'(Y_239),W_238)
| ~ reachable('#skF_4',Y_239) ),
inference(negUnitSimplification,[status(thm)],[c_4289,c_28]) ).
tff(c_4335,plain,
! [Y_241] :
( p('#skF_6'('#skF_5'(Y_241)))
| ~ reachable('#skF_4',Y_241)
| ~ reachable(initial_world,'#skF_5'(Y_241)) ),
inference(resolution,[status(thm)],[c_4288,c_4308]) ).
tff(c_4340,plain,
! [Y_242] :
( ~ reachable('#skF_4',Y_242)
| ~ reachable(initial_world,'#skF_5'(Y_242)) ),
inference(resolution,[status(thm)],[c_4335,c_58]) ).
tff(c_4351,plain,
! [Y_243] :
( ~ reachable(initial_world,Y_243)
| ~ reachable('#skF_4',Y_243) ),
inference(resolution,[status(thm)],[c_4298,c_4340]) ).
tff(c_4370,plain,
~ reachable('#skF_4','#skF_4'),
inference(resolution,[status(thm)],[c_56,c_4351]) ).
tff(c_4384,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4370]) ).
tff(c_4385,plain,
reachable(initial_world,'#skF_1'),
inference(splitRight,[status(thm)],[c_8]) ).
tff(c_7847,plain,
! [X_404] :
( reachable(X_404,'#skF_6'(X_404))
| ~ reachable(initial_world,X_404) ),
inference(splitLeft,[status(thm)],[c_20]) ).
tff(c_6330,plain,
! [X_340] :
( reachable(X_340,'#skF_6'(X_340))
| ~ reachable(initial_world,X_340) ),
inference(splitLeft,[status(thm)],[c_20]) ).
tff(c_4648,plain,
! [X_276] :
( reachable(X_276,'#skF_6'(X_276))
| ~ reachable(initial_world,X_276) ),
inference(splitLeft,[status(thm)],[c_20]) ).
tff(c_4425,plain,
! [X_33] :
( reachable(X_33,'#skF_6'(X_33))
| ~ reachable(initial_world,X_33) ),
inference(splitLeft,[status(thm)],[c_16]) ).
tff(c_4417,plain,
! [Y_250] :
( reachable(Y_250,'#skF_5'(Y_250))
| ~ reachable('#skF_4',Y_250) ),
inference(splitLeft,[status(thm)],[c_36]) ).
tff(c_4420,plain,
! [X_2,Y_250] :
( reachable(X_2,'#skF_5'(Y_250))
| ~ reachable(X_2,Y_250)
| ~ reachable('#skF_4',Y_250) ),
inference(resolution,[status(thm)],[c_4417,c_4]) ).
tff(c_4457,plain,
! [W_259,Y_260] :
( p(W_259)
| ~ reachable('#skF_5'(Y_260),W_259)
| ~ reachable('#skF_4',Y_260) ),
inference(splitLeft,[status(thm)],[c_26]) ).
tff(c_4498,plain,
! [Y_264] :
( p('#skF_6'('#skF_5'(Y_264)))
| ~ reachable('#skF_4',Y_264)
| ~ reachable(initial_world,'#skF_5'(Y_264)) ),
inference(resolution,[status(thm)],[c_4425,c_4457]) ).
tff(c_6,plain,
! [Y_6,X_33] :
( p(Y_6)
| ~ reachable('#skF_1',Y_6)
| ~ p('#skF_6'(X_33))
| ~ reachable(initial_world,X_33) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_4413,plain,
! [X_33] :
( ~ p('#skF_6'(X_33))
| ~ reachable(initial_world,X_33) ),
inference(splitLeft,[status(thm)],[c_6]) ).
tff(c_4503,plain,
! [Y_265] :
( ~ reachable('#skF_4',Y_265)
| ~ reachable(initial_world,'#skF_5'(Y_265)) ),
inference(resolution,[status(thm)],[c_4498,c_4413]) ).
tff(c_4514,plain,
! [Y_266] :
( ~ reachable(initial_world,Y_266)
| ~ reachable('#skF_4',Y_266) ),
inference(resolution,[status(thm)],[c_4420,c_4503]) ).
tff(c_4539,plain,
~ reachable('#skF_4','#skF_4'),
inference(resolution,[status(thm)],[c_56,c_4514]) ).
tff(c_4555,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2,c_4539]) ).
tff(c_4557,plain,
! [Y_267] :
( p(Y_267)
| ~ reachable('#skF_1',Y_267) ),
inference(splitRight,[status(thm)],[c_26]) ).
tff(c_4565,plain,
( p('#skF_6'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_4425,c_4557]) ).
tff(c_4581,plain,
p('#skF_6'('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_4565]) ).
tff(c_4587,plain,
~ reachable(initial_world,'#skF_1'),
inference(resolution,[status(thm)],[c_4581,c_4413]) ).
tff(c_4591,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_4587]) ).
tff(c_4592,plain,
! [Y_6] :
( p(Y_6)
| ~ reachable('#skF_1',Y_6) ),
inference(splitRight,[status(thm)],[c_16]) ).
tff(c_4654,plain,
( p('#skF_6'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_4648,c_4592]) ).
tff(c_4660,plain,
p('#skF_6'('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_4654]) ).
tff(c_4664,plain,
~ reachable(initial_world,'#skF_1'),
inference(resolution,[status(thm)],[c_4660,c_4413]) ).
tff(c_4668,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_4664]) ).
tff(c_4671,plain,
! [X_277] :
( reachable(X_277,'#skF_2'(X_277))
| ~ reachable(initial_world,X_277) ),
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_4685,plain,
! [X_278,X_279] :
( reachable(X_278,'#skF_2'(X_279))
| ~ reachable(X_278,X_279)
| ~ reachable(initial_world,X_279) ),
inference(resolution,[status(thm)],[c_4671,c_4]) ).
tff(c_4698,plain,
! [X_281,X_282,X_283] :
( reachable(X_281,'#skF_2'(X_282))
| ~ reachable(X_281,X_283)
| ~ reachable(X_283,X_282)
| ~ reachable(initial_world,X_282) ),
inference(resolution,[status(thm)],[c_4685,c_4]) ).
tff(c_4726,plain,
! [X_284] :
( reachable(initial_world,'#skF_2'(X_284))
| ~ reachable('#skF_1',X_284)
| ~ reachable(initial_world,X_284) ),
inference(resolution,[status(thm)],[c_4385,c_4698]) ).
tff(c_4735,plain,
! [X_2,X_284] :
( reachable(X_2,'#skF_2'(X_284))
| ~ reachable(X_2,initial_world)
| ~ reachable('#skF_1',X_284)
| ~ reachable(initial_world,X_284) ),
inference(resolution,[status(thm)],[c_4726,c_4]) ).
tff(c_4669,plain,
! [X_7] :
( reachable(X_7,'#skF_2'(X_7))
| ~ reachable(initial_world,X_7) ),
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_4976,plain,
! [X_299,X_300] :
( reachable(X_299,'#skF_2'(X_300))
| ~ reachable('#skF_2'(X_299),X_300)
| ~ reachable(initial_world,X_300)
| ~ reachable(initial_world,X_299) ),
inference(resolution,[status(thm)],[c_4669,c_4698]) ).
tff(c_5027,plain,
! [X_301] :
( reachable(X_301,'#skF_2'('#skF_2'(X_301)))
| ~ reachable(initial_world,'#skF_2'(X_301))
| ~ reachable(initial_world,X_301) ),
inference(resolution,[status(thm)],[c_2,c_4976]) ).
tff(c_5049,plain,
( p('#skF_2'('#skF_2'('#skF_1')))
| ~ reachable(initial_world,'#skF_2'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_5027,c_4592]) ).
tff(c_5060,plain,
( p('#skF_2'('#skF_2'('#skF_1')))
| ~ reachable(initial_world,'#skF_2'('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_5049]) ).
tff(c_5062,plain,
~ reachable(initial_world,'#skF_2'('#skF_1')),
inference(splitLeft,[status(thm)],[c_5060]) ).
tff(c_5069,plain,
( ~ reachable(initial_world,initial_world)
| ~ reachable('#skF_1','#skF_1')
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_4735,c_5062]) ).
tff(c_5085,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_2,c_2,c_5069]) ).
tff(c_5087,plain,
reachable(initial_world,'#skF_2'('#skF_1')),
inference(splitRight,[status(thm)],[c_5060]) ).
tff(c_5026,plain,
! [X_299] :
( reachable(X_299,'#skF_2'('#skF_2'(X_299)))
| ~ reachable(initial_world,'#skF_2'(X_299))
| ~ reachable(initial_world,X_299) ),
inference(resolution,[status(thm)],[c_2,c_4976]) ).
tff(c_5474,plain,
! [X_312] :
( reachable(X_312,'#skF_6'(X_312))
| ~ reachable(initial_world,X_312) ),
inference(splitLeft,[status(thm)],[c_24]) ).
tff(c_5506,plain,
( p('#skF_6'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_5474,c_4592]) ).
tff(c_5522,plain,
p('#skF_6'('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_5506]) ).
tff(c_5526,plain,
~ reachable(initial_world,'#skF_1'),
inference(resolution,[status(thm)],[c_5522,c_4413]) ).
tff(c_5530,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_5526]) ).
tff(c_5608,plain,
! [Z_316,X_317] :
( reachable(Z_316,'#skF_3'(X_317,Z_316))
| ~ reachable('#skF_2'(X_317),Z_316)
| ~ reachable(initial_world,X_317) ),
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_5665,plain,
! [X_318] :
( reachable('#skF_2'(X_318),'#skF_3'(X_318,'#skF_2'(X_318)))
| ~ reachable(initial_world,X_318) ),
inference(resolution,[status(thm)],[c_2,c_5608]) ).
tff(c_6109,plain,
! [X_329,X_330] :
( reachable(X_329,'#skF_3'(X_330,'#skF_2'(X_330)))
| ~ reachable(X_329,'#skF_2'(X_330))
| ~ reachable(initial_world,X_330) ),
inference(resolution,[status(thm)],[c_5665,c_4]) ).
tff(c_6170,plain,
! [X_331] :
( p('#skF_3'(X_331,'#skF_2'(X_331)))
| ~ reachable('#skF_1','#skF_2'(X_331))
| ~ reachable(initial_world,X_331) ),
inference(resolution,[status(thm)],[c_6109,c_4592]) ).
tff(c_5202,plain,
! [X_305,Z_306] :
( ~ p('#skF_3'(X_305,Z_306))
| ~ reachable('#skF_2'(X_305),Z_306)
| ~ reachable(initial_world,X_305) ),
inference(splitLeft,[status(thm)],[c_22]) ).
tff(c_5262,plain,
! [X_305] :
( ~ p('#skF_3'(X_305,'#skF_2'(X_305)))
| ~ reachable(initial_world,X_305) ),
inference(resolution,[status(thm)],[c_2,c_5202]) ).
tff(c_6190,plain,
! [X_333] :
( ~ reachable('#skF_1','#skF_2'(X_333))
| ~ reachable(initial_world,X_333) ),
inference(resolution,[status(thm)],[c_6170,c_5262]) ).
tff(c_6218,plain,
( ~ reachable(initial_world,'#skF_2'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_5026,c_6190]) ).
tff(c_6256,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_5087,c_6218]) ).
tff(c_6258,plain,
! [X_334] :
( reachable(X_334,'#skF_6'(X_334))
| ~ reachable(initial_world,X_334) ),
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_6280,plain,
( p('#skF_6'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_6258,c_4592]) ).
tff(c_6291,plain,
p('#skF_6'('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_6280]) ).
tff(c_6295,plain,
~ reachable(initial_world,'#skF_1'),
inference(resolution,[status(thm)],[c_6291,c_4413]) ).
tff(c_6299,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_6295]) ).
tff(c_6300,plain,
! [Y_6] :
( p(Y_6)
| ~ reachable('#skF_1',Y_6) ),
inference(splitRight,[status(thm)],[c_36]) ).
tff(c_6334,plain,
( p('#skF_6'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_6330,c_6300]) ).
tff(c_6339,plain,
p('#skF_6'('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_6334]) ).
tff(c_6343,plain,
~ reachable(initial_world,'#skF_1'),
inference(resolution,[status(thm)],[c_6339,c_4413]) ).
tff(c_6347,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_6343]) ).
tff(c_6349,plain,
! [X_341] :
( reachable(X_341,'#skF_2'(X_341))
| ~ reachable(initial_world,X_341) ),
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_6361,plain,
! [X_342,X_343] :
( reachable(X_342,'#skF_2'(X_343))
| ~ reachable(X_342,X_343)
| ~ reachable(initial_world,X_343) ),
inference(resolution,[status(thm)],[c_6349,c_4]) ).
tff(c_6413,plain,
! [X_351,X_352,X_353] :
( reachable(X_351,'#skF_2'(X_352))
| ~ reachable(X_351,X_353)
| ~ reachable(X_353,X_352)
| ~ reachable(initial_world,X_352) ),
inference(resolution,[status(thm)],[c_6361,c_4]) ).
tff(c_6441,plain,
! [X_354] :
( reachable(initial_world,'#skF_2'(X_354))
| ~ reachable('#skF_1',X_354)
| ~ reachable(initial_world,X_354) ),
inference(resolution,[status(thm)],[c_4385,c_6413]) ).
tff(c_6450,plain,
! [X_2,X_354] :
( reachable(X_2,'#skF_2'(X_354))
| ~ reachable(X_2,initial_world)
| ~ reachable('#skF_1',X_354)
| ~ reachable(initial_world,X_354) ),
inference(resolution,[status(thm)],[c_6441,c_4]) ).
tff(c_6348,plain,
! [X_7] :
( reachable(X_7,'#skF_2'(X_7))
| ~ reachable(initial_world,X_7) ),
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_6645,plain,
! [X_371,X_372] :
( reachable(X_371,'#skF_2'(X_372))
| ~ reachable('#skF_2'(X_371),X_372)
| ~ reachable(initial_world,X_372)
| ~ reachable(initial_world,X_371) ),
inference(resolution,[status(thm)],[c_6348,c_6413]) ).
tff(c_6691,plain,
! [X_373] :
( reachable(X_373,'#skF_2'('#skF_2'(X_373)))
| ~ reachable(initial_world,'#skF_2'(X_373))
| ~ reachable(initial_world,X_373) ),
inference(resolution,[status(thm)],[c_2,c_6645]) ).
tff(c_6713,plain,
( p('#skF_2'('#skF_2'('#skF_1')))
| ~ reachable(initial_world,'#skF_2'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_6691,c_6300]) ).
tff(c_6724,plain,
( p('#skF_2'('#skF_2'('#skF_1')))
| ~ reachable(initial_world,'#skF_2'('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_6713]) ).
tff(c_6726,plain,
~ reachable(initial_world,'#skF_2'('#skF_1')),
inference(splitLeft,[status(thm)],[c_6724]) ).
tff(c_6733,plain,
( ~ reachable(initial_world,initial_world)
| ~ reachable('#skF_1','#skF_1')
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_6450,c_6726]) ).
tff(c_6749,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_2,c_2,c_6733]) ).
tff(c_6751,plain,
reachable(initial_world,'#skF_2'('#skF_1')),
inference(splitRight,[status(thm)],[c_6724]) ).
tff(c_6690,plain,
! [X_371] :
( reachable(X_371,'#skF_2'('#skF_2'(X_371)))
| ~ reachable(initial_world,'#skF_2'(X_371))
| ~ reachable(initial_world,X_371) ),
inference(resolution,[status(thm)],[c_2,c_6645]) ).
tff(c_6859,plain,
! [X_377] :
( reachable(X_377,'#skF_6'(X_377))
| ~ reachable(initial_world,X_377) ),
inference(splitLeft,[status(thm)],[c_24]) ).
tff(c_6883,plain,
( p('#skF_6'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_6859,c_6300]) ).
tff(c_6895,plain,
p('#skF_6'('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_6883]) ).
tff(c_6899,plain,
~ reachable(initial_world,'#skF_1'),
inference(resolution,[status(thm)],[c_6895,c_4413]) ).
tff(c_6903,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_6899]) ).
tff(c_7033,plain,
! [Z_380,X_381] :
( reachable(Z_380,'#skF_3'(X_381,Z_380))
| ~ reachable('#skF_2'(X_381),Z_380)
| ~ reachable(initial_world,X_381) ),
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_7082,plain,
! [X_382] :
( reachable('#skF_2'(X_382),'#skF_3'(X_382,'#skF_2'(X_382)))
| ~ reachable(initial_world,X_382) ),
inference(resolution,[status(thm)],[c_2,c_7033]) ).
tff(c_7636,plain,
! [X_396,X_397] :
( reachable(X_396,'#skF_3'(X_397,'#skF_2'(X_397)))
| ~ reachable(X_396,'#skF_2'(X_397))
| ~ reachable(initial_world,X_397) ),
inference(resolution,[status(thm)],[c_7082,c_4]) ).
tff(c_7732,plain,
! [X_399] :
( p('#skF_3'(X_399,'#skF_2'(X_399)))
| ~ reachable('#skF_1','#skF_2'(X_399))
| ~ reachable(initial_world,X_399) ),
inference(resolution,[status(thm)],[c_7636,c_6300]) ).
tff(c_6477,plain,
! [X_358,Z_359] :
( ~ p('#skF_3'(X_358,Z_359))
| ~ reachable('#skF_2'(X_358),Z_359)
| ~ reachable(initial_world,X_358) ),
inference(splitLeft,[status(thm)],[c_22]) ).
tff(c_6512,plain,
! [X_358] :
( ~ p('#skF_3'(X_358,'#skF_2'(X_358)))
| ~ reachable(initial_world,X_358) ),
inference(resolution,[status(thm)],[c_2,c_6477]) ).
tff(c_7744,plain,
! [X_400] :
( ~ reachable('#skF_1','#skF_2'(X_400))
| ~ reachable(initial_world,X_400) ),
inference(resolution,[status(thm)],[c_7732,c_6512]) ).
tff(c_7772,plain,
( ~ reachable(initial_world,'#skF_2'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_6690,c_7744]) ).
tff(c_7810,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_6751,c_7772]) ).
tff(c_7812,plain,
! [X_401] :
( reachable(X_401,'#skF_6'(X_401))
| ~ reachable(initial_world,X_401) ),
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_7820,plain,
( p('#skF_6'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_7812,c_6300]) ).
tff(c_7827,plain,
p('#skF_6'('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_7820]) ).
tff(c_7831,plain,
~ reachable(initial_world,'#skF_1'),
inference(resolution,[status(thm)],[c_7827,c_4413]) ).
tff(c_7835,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_7831]) ).
tff(c_7836,plain,
! [Y_6] :
( p(Y_6)
| ~ reachable('#skF_1',Y_6) ),
inference(splitRight,[status(thm)],[c_6]) ).
tff(c_7851,plain,
( p('#skF_6'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_7847,c_7836]) ).
tff(c_7856,plain,
p('#skF_6'('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_7851]) ).
tff(c_10,plain,
! [X_7,X_33] :
( reachable(X_7,'#skF_2'(X_7))
| ~ reachable(initial_world,X_7)
| ~ p('#skF_6'(X_33))
| ~ reachable(initial_world,X_33) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_7844,plain,
! [X_33] :
( ~ p('#skF_6'(X_33))
| ~ reachable(initial_world,X_33) ),
inference(splitLeft,[status(thm)],[c_10]) ).
tff(c_7860,plain,
~ reachable(initial_world,'#skF_1'),
inference(resolution,[status(thm)],[c_7856,c_7844]) ).
tff(c_7864,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_7860]) ).
tff(c_7866,plain,
! [X_405] :
( reachable(X_405,'#skF_2'(X_405))
| ~ reachable(initial_world,X_405) ),
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_7877,plain,
! [X_406,X_407] :
( reachable(X_406,'#skF_2'(X_407))
| ~ reachable(X_406,X_407)
| ~ reachable(initial_world,X_407) ),
inference(resolution,[status(thm)],[c_7866,c_4]) ).
tff(c_7887,plain,
! [X_409,X_410,X_411] :
( reachable(X_409,'#skF_2'(X_410))
| ~ reachable(X_409,X_411)
| ~ reachable(X_411,X_410)
| ~ reachable(initial_world,X_410) ),
inference(resolution,[status(thm)],[c_7877,c_4]) ).
tff(c_7903,plain,
! [X_412] :
( reachable(initial_world,'#skF_2'(X_412))
| ~ reachable('#skF_1',X_412)
| ~ reachable(initial_world,X_412) ),
inference(resolution,[status(thm)],[c_4385,c_7887]) ).
tff(c_7909,plain,
! [X_2,X_412] :
( reachable(X_2,'#skF_2'(X_412))
| ~ reachable(X_2,initial_world)
| ~ reachable('#skF_1',X_412)
| ~ reachable(initial_world,X_412) ),
inference(resolution,[status(thm)],[c_7903,c_4]) ).
tff(c_7865,plain,
! [X_7] :
( reachable(X_7,'#skF_2'(X_7))
| ~ reachable(initial_world,X_7) ),
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_7944,plain,
! [X_418,X_419] :
( reachable(X_418,'#skF_2'(X_419))
| ~ reachable('#skF_2'(X_418),X_419)
| ~ reachable(initial_world,X_419)
| ~ reachable(initial_world,X_418) ),
inference(resolution,[status(thm)],[c_7865,c_7887]) ).
tff(c_7970,plain,
! [X_420] :
( reachable(X_420,'#skF_2'('#skF_2'(X_420)))
| ~ reachable(initial_world,'#skF_2'(X_420))
| ~ reachable(initial_world,X_420) ),
inference(resolution,[status(thm)],[c_2,c_7944]) ).
tff(c_7980,plain,
( p('#skF_2'('#skF_2'('#skF_1')))
| ~ reachable(initial_world,'#skF_2'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_7970,c_7836]) ).
tff(c_7987,plain,
( p('#skF_2'('#skF_2'('#skF_1')))
| ~ reachable(initial_world,'#skF_2'('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_7980]) ).
tff(c_7989,plain,
~ reachable(initial_world,'#skF_2'('#skF_1')),
inference(splitLeft,[status(thm)],[c_7987]) ).
tff(c_7995,plain,
( ~ reachable(initial_world,initial_world)
| ~ reachable('#skF_1','#skF_1')
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_7909,c_7989]) ).
tff(c_8011,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_2,c_2,c_7995]) ).
tff(c_8013,plain,
reachable(initial_world,'#skF_2'('#skF_1')),
inference(splitRight,[status(thm)],[c_7987]) ).
tff(c_7969,plain,
! [X_418] :
( reachable(X_418,'#skF_2'('#skF_2'(X_418)))
| ~ reachable(initial_world,'#skF_2'(X_418))
| ~ reachable(initial_world,X_418) ),
inference(resolution,[status(thm)],[c_2,c_7944]) ).
tff(c_8630,plain,
! [X_443] :
( reachable(X_443,'#skF_6'(X_443))
| ~ reachable(initial_world,X_443) ),
inference(splitLeft,[status(thm)],[c_24]) ).
tff(c_8658,plain,
( p('#skF_6'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_8630,c_7836]) ).
tff(c_8675,plain,
p('#skF_6'('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_8658]) ).
tff(c_8679,plain,
~ reachable(initial_world,'#skF_1'),
inference(resolution,[status(thm)],[c_8675,c_7844]) ).
tff(c_8683,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_8679]) ).
tff(c_8686,plain,
! [Z_445,X_446] :
( reachable(Z_445,'#skF_3'(X_446,Z_445))
| ~ reachable('#skF_2'(X_446),Z_445)
| ~ reachable(initial_world,X_446) ),
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_8739,plain,
! [X_447] :
( reachable('#skF_2'(X_447),'#skF_3'(X_447,'#skF_2'(X_447)))
| ~ reachable(initial_world,X_447) ),
inference(resolution,[status(thm)],[c_2,c_8686]) ).
tff(c_8975,plain,
! [X_458,X_459] :
( reachable(X_458,'#skF_3'(X_459,'#skF_2'(X_459)))
| ~ reachable(X_458,'#skF_2'(X_459))
| ~ reachable(initial_world,X_459) ),
inference(resolution,[status(thm)],[c_8739,c_4]) ).
tff(c_9060,plain,
! [X_461] :
( p('#skF_3'(X_461,'#skF_2'(X_461)))
| ~ reachable('#skF_1','#skF_2'(X_461))
| ~ reachable(initial_world,X_461) ),
inference(resolution,[status(thm)],[c_8975,c_7836]) ).
tff(c_8301,plain,
! [X_431,Z_432] :
( ~ p('#skF_3'(X_431,Z_432))
| ~ reachable('#skF_2'(X_431),Z_432)
| ~ reachable(initial_world,X_431) ),
inference(splitLeft,[status(thm)],[c_22]) ).
tff(c_8351,plain,
! [X_431] :
( ~ p('#skF_3'(X_431,'#skF_2'(X_431)))
| ~ reachable(initial_world,X_431) ),
inference(resolution,[status(thm)],[c_2,c_8301]) ).
tff(c_9072,plain,
! [X_462] :
( ~ reachable('#skF_1','#skF_2'(X_462))
| ~ reachable(initial_world,X_462) ),
inference(resolution,[status(thm)],[c_9060,c_8351]) ).
tff(c_9100,plain,
( ~ reachable(initial_world,'#skF_2'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_7969,c_9072]) ).
tff(c_9138,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_8013,c_9100]) ).
tff(c_9140,plain,
! [X_463] :
( reachable(X_463,'#skF_6'(X_463))
| ~ reachable(initial_world,X_463) ),
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_9158,plain,
( p('#skF_6'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_9140,c_7836]) ).
tff(c_9170,plain,
p('#skF_6'('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_9158]) ).
tff(c_9175,plain,
~ reachable(initial_world,'#skF_1'),
inference(resolution,[status(thm)],[c_9170,c_7844]) ).
tff(c_9179,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_9175]) ).
tff(c_9181,plain,
! [X_464] :
( reachable(X_464,'#skF_2'(X_464))
| ~ reachable(initial_world,X_464) ),
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_9192,plain,
! [X_465,X_466] :
( reachable(X_465,'#skF_2'(X_466))
| ~ reachable(X_465,X_466)
| ~ reachable(initial_world,X_466) ),
inference(resolution,[status(thm)],[c_9181,c_4]) ).
tff(c_9202,plain,
! [X_468,X_469,X_470] :
( reachable(X_468,'#skF_2'(X_469))
| ~ reachable(X_468,X_470)
| ~ reachable(X_470,X_469)
| ~ reachable(initial_world,X_469) ),
inference(resolution,[status(thm)],[c_9192,c_4]) ).
tff(c_9218,plain,
! [X_471] :
( reachable(initial_world,'#skF_2'(X_471))
| ~ reachable('#skF_1',X_471)
| ~ reachable(initial_world,X_471) ),
inference(resolution,[status(thm)],[c_4385,c_9202]) ).
tff(c_9224,plain,
! [X_2,X_471] :
( reachable(X_2,'#skF_2'(X_471))
| ~ reachable(X_2,initial_world)
| ~ reachable('#skF_1',X_471)
| ~ reachable(initial_world,X_471) ),
inference(resolution,[status(thm)],[c_9218,c_4]) ).
tff(c_9180,plain,
! [X_7] :
( reachable(X_7,'#skF_2'(X_7))
| ~ reachable(initial_world,X_7) ),
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_9258,plain,
! [X_477,X_478] :
( reachable(X_477,'#skF_2'(X_478))
| ~ reachable('#skF_2'(X_477),X_478)
| ~ reachable(initial_world,X_478)
| ~ reachable(initial_world,X_477) ),
inference(resolution,[status(thm)],[c_9180,c_9202]) ).
tff(c_9284,plain,
! [X_479] :
( reachable(X_479,'#skF_2'('#skF_2'(X_479)))
| ~ reachable(initial_world,'#skF_2'(X_479))
| ~ reachable(initial_world,X_479) ),
inference(resolution,[status(thm)],[c_2,c_9258]) ).
tff(c_9294,plain,
( p('#skF_2'('#skF_2'('#skF_1')))
| ~ reachable(initial_world,'#skF_2'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_9284,c_7836]) ).
tff(c_9301,plain,
( p('#skF_2'('#skF_2'('#skF_1')))
| ~ reachable(initial_world,'#skF_2'('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_9294]) ).
tff(c_9303,plain,
~ reachable(initial_world,'#skF_2'('#skF_1')),
inference(splitLeft,[status(thm)],[c_9301]) ).
tff(c_9310,plain,
( ~ reachable(initial_world,initial_world)
| ~ reachable('#skF_1','#skF_1')
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_9224,c_9303]) ).
tff(c_9326,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_2,c_2,c_9310]) ).
tff(c_9328,plain,
reachable(initial_world,'#skF_2'('#skF_1')),
inference(splitRight,[status(thm)],[c_9301]) ).
tff(c_9283,plain,
! [X_477] :
( reachable(X_477,'#skF_2'('#skF_2'(X_477)))
| ~ reachable(initial_world,'#skF_2'(X_477))
| ~ reachable(initial_world,X_477) ),
inference(resolution,[status(thm)],[c_2,c_9258]) ).
tff(c_11586,plain,
! [X_565] :
( reachable(X_565,'#skF_6'(X_565))
| ~ reachable(initial_world,X_565) ),
inference(splitLeft,[status(thm)],[c_24]) ).
tff(c_11614,plain,
( p('#skF_6'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_11586,c_7836]) ).
tff(c_11631,plain,
p('#skF_6'('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_11614]) ).
tff(c_14,plain,
! [Z_18,X_7,X_33] :
( reachable(Z_18,'#skF_3'(X_7,Z_18))
| ~ reachable('#skF_2'(X_7),Z_18)
| ~ reachable(initial_world,X_7)
| ~ p('#skF_6'(X_33))
| ~ reachable(initial_world,X_33) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_11268,plain,
! [X_33] :
( ~ p('#skF_6'(X_33))
| ~ reachable(initial_world,X_33) ),
inference(splitLeft,[status(thm)],[c_14]) ).
tff(c_11635,plain,
~ reachable(initial_world,'#skF_1'),
inference(resolution,[status(thm)],[c_11631,c_11268]) ).
tff(c_11639,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_11635]) ).
tff(c_11642,plain,
! [Z_567,X_568] :
( reachable(Z_567,'#skF_3'(X_568,Z_567))
| ~ reachable('#skF_2'(X_568),Z_567)
| ~ reachable(initial_world,X_568) ),
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_11695,plain,
! [X_569] :
( reachable('#skF_2'(X_569),'#skF_3'(X_569,'#skF_2'(X_569)))
| ~ reachable(initial_world,X_569) ),
inference(resolution,[status(thm)],[c_2,c_11642]) ).
tff(c_11931,plain,
! [X_580,X_581] :
( reachable(X_580,'#skF_3'(X_581,'#skF_2'(X_581)))
| ~ reachable(X_580,'#skF_2'(X_581))
| ~ reachable(initial_world,X_581) ),
inference(resolution,[status(thm)],[c_11695,c_4]) ).
tff(c_12016,plain,
! [X_583] :
( p('#skF_3'(X_583,'#skF_2'(X_583)))
| ~ reachable('#skF_1','#skF_2'(X_583))
| ~ reachable(initial_world,X_583) ),
inference(resolution,[status(thm)],[c_11931,c_7836]) ).
tff(c_10777,plain,
! [X_534] :
( reachable(X_534,'#skF_6'(X_534))
| ~ reachable(initial_world,X_534) ),
inference(splitLeft,[status(thm)],[c_24]) ).
tff(c_10805,plain,
( p('#skF_6'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_10777,c_7836]) ).
tff(c_10822,plain,
p('#skF_6'('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_10805]) ).
tff(c_12,plain,
! [X_7,Z_18,X_33] :
( ~ p('#skF_3'(X_7,Z_18))
| ~ reachable('#skF_2'(X_7),Z_18)
| ~ reachable(initial_world,X_7)
| ~ p('#skF_6'(X_33))
| ~ reachable(initial_world,X_33) ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_9525,plain,
! [X_33] :
( ~ p('#skF_6'(X_33))
| ~ reachable(initial_world,X_33) ),
inference(splitLeft,[status(thm)],[c_12]) ).
tff(c_10826,plain,
~ reachable(initial_world,'#skF_1'),
inference(resolution,[status(thm)],[c_10822,c_9525]) ).
tff(c_10830,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_10826]) ).
tff(c_10832,plain,
! [Z_535,X_536] :
( reachable(Z_535,'#skF_3'(X_536,Z_535))
| ~ reachable('#skF_2'(X_536),Z_535)
| ~ reachable(initial_world,X_536) ),
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_10885,plain,
! [X_537] :
( reachable('#skF_2'(X_537),'#skF_3'(X_537,'#skF_2'(X_537)))
| ~ reachable(initial_world,X_537) ),
inference(resolution,[status(thm)],[c_2,c_10832]) ).
tff(c_10981,plain,
! [X_542,X_543] :
( reachable(X_542,'#skF_3'(X_543,'#skF_2'(X_543)))
| ~ reachable(X_542,'#skF_2'(X_543))
| ~ reachable(initial_world,X_543) ),
inference(resolution,[status(thm)],[c_10885,c_4]) ).
tff(c_11026,plain,
! [X_544] :
( p('#skF_3'(X_544,'#skF_2'(X_544)))
| ~ reachable('#skF_1','#skF_2'(X_544))
| ~ reachable(initial_world,X_544) ),
inference(resolution,[status(thm)],[c_10981,c_7836]) ).
tff(c_10706,plain,
! [X_529,Z_530] :
( ~ p('#skF_3'(X_529,Z_530))
| ~ reachable('#skF_2'(X_529),Z_530)
| ~ reachable(initial_world,X_529) ),
inference(splitLeft,[status(thm)],[c_22]) ).
tff(c_10771,plain,
! [X_529] :
( ~ p('#skF_3'(X_529,'#skF_2'(X_529)))
| ~ reachable(initial_world,X_529) ),
inference(resolution,[status(thm)],[c_2,c_10706]) ).
tff(c_11046,plain,
! [X_546] :
( ~ reachable('#skF_1','#skF_2'(X_546))
| ~ reachable(initial_world,X_546) ),
inference(resolution,[status(thm)],[c_11026,c_10771]) ).
tff(c_11074,plain,
( ~ reachable(initial_world,'#skF_2'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_9283,c_11046]) ).
tff(c_11112,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_9328,c_11074]) ).
tff(c_11114,plain,
! [X_547] :
( reachable(X_547,'#skF_6'(X_547))
| ~ reachable(initial_world,X_547) ),
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_11138,plain,
( p('#skF_6'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_11114,c_7836]) ).
tff(c_11154,plain,
p('#skF_6'('#skF_1')),
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_11138]) ).
tff(c_11158,plain,
~ reachable(initial_world,'#skF_1'),
inference(resolution,[status(thm)],[c_11154,c_9525]) ).
tff(c_11162,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_11158]) ).
tff(c_11164,plain,
! [X_548,Z_549] :
( ~ p('#skF_3'(X_548,Z_549))
| ~ reachable('#skF_2'(X_548),Z_549)
| ~ reachable(initial_world,X_548) ),
inference(splitRight,[status(thm)],[c_12]) ).
tff(c_11209,plain,
! [X_548] :
( ~ p('#skF_3'(X_548,'#skF_2'(X_548)))
| ~ reachable(initial_world,X_548) ),
inference(resolution,[status(thm)],[c_2,c_11164]) ).
tff(c_12028,plain,
! [X_584] :
( ~ reachable('#skF_1','#skF_2'(X_584))
| ~ reachable(initial_world,X_584) ),
inference(resolution,[status(thm)],[c_12016,c_11209]) ).
tff(c_12056,plain,
( ~ reachable(initial_world,'#skF_2'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_9283,c_12028]) ).
tff(c_12094,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_9328,c_12056]) ).
tff(c_12096,plain,
! [Z_585,X_586] :
( reachable(Z_585,'#skF_3'(X_586,Z_585))
| ~ reachable('#skF_2'(X_586),Z_585)
| ~ reachable(initial_world,X_586) ),
inference(splitRight,[status(thm)],[c_14]) ).
tff(c_12133,plain,
! [X_587] :
( reachable('#skF_2'(X_587),'#skF_3'(X_587,'#skF_2'(X_587)))
| ~ reachable(initial_world,X_587) ),
inference(resolution,[status(thm)],[c_2,c_12096]) ).
tff(c_12414,plain,
! [X_596,X_597] :
( reachable(X_596,'#skF_3'(X_597,'#skF_2'(X_597)))
| ~ reachable(X_596,'#skF_2'(X_597))
| ~ reachable(initial_world,X_597) ),
inference(resolution,[status(thm)],[c_12133,c_4]) ).
tff(c_12459,plain,
! [X_598] :
( p('#skF_3'(X_598,'#skF_2'(X_598)))
| ~ reachable('#skF_1','#skF_2'(X_598))
| ~ reachable(initial_world,X_598) ),
inference(resolution,[status(thm)],[c_12414,c_7836]) ).
tff(c_12471,plain,
! [X_599] :
( ~ reachable('#skF_1','#skF_2'(X_599))
| ~ reachable(initial_world,X_599) ),
inference(resolution,[status(thm)],[c_12459,c_11209]) ).
tff(c_12495,plain,
( ~ reachable(initial_world,'#skF_2'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_9283,c_12471]) ).
tff(c_12530,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4385,c_9328,c_12495]) ).
tff(c_12531,plain,
reachable(initial_world,'#skF_1'),
inference(splitRight,[status(thm)],[c_48]) ).
tff(c_12532,plain,
~ reachable(initial_world,'#skF_4'),
inference(splitRight,[status(thm)],[c_48]) ).
tff(c_50,plain,
! [X_7] :
( reachable(X_7,'#skF_2'(X_7))
| ~ reachable(initial_world,X_7)
| reachable(initial_world,'#skF_4') ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_12556,plain,
! [X_605] :
( reachable(X_605,'#skF_2'(X_605))
| ~ reachable(initial_world,X_605) ),
inference(negUnitSimplification,[status(thm)],[c_12532,c_50]) ).
tff(c_12569,plain,
! [X_606,X_607] :
( reachable(X_606,'#skF_2'(X_607))
| ~ reachable(X_606,X_607)
| ~ reachable(initial_world,X_607) ),
inference(resolution,[status(thm)],[c_12556,c_4]) ).
tff(c_12580,plain,
! [X_609,X_610,X_611] :
( reachable(X_609,'#skF_2'(X_610))
| ~ reachable(X_609,X_611)
| ~ reachable(X_611,X_610)
| ~ reachable(initial_world,X_610) ),
inference(resolution,[status(thm)],[c_12569,c_4]) ).
tff(c_12593,plain,
! [X_612] :
( reachable(initial_world,'#skF_2'(X_612))
| ~ reachable('#skF_1',X_612)
| ~ reachable(initial_world,X_612) ),
inference(resolution,[status(thm)],[c_12531,c_12580]) ).
tff(c_12599,plain,
! [X_2,X_612] :
( reachable(X_2,'#skF_2'(X_612))
| ~ reachable(X_2,initial_world)
| ~ reachable('#skF_1',X_612)
| ~ reachable(initial_world,X_612) ),
inference(resolution,[status(thm)],[c_12593,c_4]) ).
tff(c_12555,plain,
! [X_7] :
( reachable(X_7,'#skF_2'(X_7))
| ~ reachable(initial_world,X_7) ),
inference(negUnitSimplification,[status(thm)],[c_12532,c_50]) ).
tff(c_12636,plain,
! [X_619,X_620] :
( reachable(X_619,'#skF_2'(X_620))
| ~ reachable('#skF_2'(X_619),X_620)
| ~ reachable(initial_world,X_620)
| ~ reachable(initial_world,X_619) ),
inference(resolution,[status(thm)],[c_12555,c_12580]) ).
tff(c_12694,plain,
! [X_625] :
( reachable(X_625,'#skF_2'('#skF_2'(X_625)))
| ~ reachable(initial_world,'#skF_2'(X_625))
| ~ reachable(initial_world,X_625) ),
inference(resolution,[status(thm)],[c_2,c_12636]) ).
tff(c_46,plain,
! [Y_6] :
( p(Y_6)
| ~ reachable('#skF_1',Y_6)
| reachable(initial_world,'#skF_4') ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_12533,plain,
! [Y_6] :
( p(Y_6)
| ~ reachable('#skF_1',Y_6) ),
inference(negUnitSimplification,[status(thm)],[c_12532,c_46]) ).
tff(c_12713,plain,
( p('#skF_2'('#skF_2'('#skF_1')))
| ~ reachable(initial_world,'#skF_2'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_12694,c_12533]) ).
tff(c_12721,plain,
( p('#skF_2'('#skF_2'('#skF_1')))
| ~ reachable(initial_world,'#skF_2'('#skF_1')) ),
inference(demodulation,[status(thm),theory(equality)],[c_12531,c_12713]) ).
tff(c_12722,plain,
~ reachable(initial_world,'#skF_2'('#skF_1')),
inference(splitLeft,[status(thm)],[c_12721]) ).
tff(c_12725,plain,
( ~ reachable(initial_world,initial_world)
| ~ reachable('#skF_1','#skF_1')
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_12599,c_12722]) ).
tff(c_12735,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_12531,c_2,c_2,c_12725]) ).
tff(c_12737,plain,
reachable(initial_world,'#skF_2'('#skF_1')),
inference(splitRight,[status(thm)],[c_12721]) ).
tff(c_12656,plain,
! [X_619] :
( reachable(X_619,'#skF_2'('#skF_2'(X_619)))
| ~ reachable(initial_world,'#skF_2'(X_619))
| ~ reachable(initial_world,X_619) ),
inference(resolution,[status(thm)],[c_2,c_12636]) ).
tff(c_54,plain,
! [Z_18,X_7] :
( reachable(Z_18,'#skF_3'(X_7,Z_18))
| ~ reachable('#skF_2'(X_7),Z_18)
| ~ reachable(initial_world,X_7)
| reachable(initial_world,'#skF_4') ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_12658,plain,
! [Z_621,X_622] :
( reachable(Z_621,'#skF_3'(X_622,Z_621))
| ~ reachable('#skF_2'(X_622),Z_621)
| ~ reachable(initial_world,X_622) ),
inference(negUnitSimplification,[status(thm)],[c_12532,c_54]) ).
tff(c_12675,plain,
! [X_623] :
( reachable('#skF_2'(X_623),'#skF_3'(X_623,'#skF_2'(X_623)))
| ~ reachable(initial_world,X_623) ),
inference(resolution,[status(thm)],[c_2,c_12658]) ).
tff(c_13236,plain,
! [X_641,X_642] :
( reachable(X_641,'#skF_3'(X_642,'#skF_2'(X_642)))
| ~ reachable(X_641,'#skF_2'(X_642))
| ~ reachable(initial_world,X_642) ),
inference(resolution,[status(thm)],[c_12675,c_4]) ).
tff(c_13281,plain,
! [X_643] :
( p('#skF_3'(X_643,'#skF_2'(X_643)))
| ~ reachable('#skF_1','#skF_2'(X_643))
| ~ reachable(initial_world,X_643) ),
inference(resolution,[status(thm)],[c_13236,c_12533]) ).
tff(c_52,plain,
! [X_7,Z_18] :
( ~ p('#skF_3'(X_7,Z_18))
| ~ reachable('#skF_2'(X_7),Z_18)
| ~ reachable(initial_world,X_7)
| reachable(initial_world,'#skF_4') ),
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_12613,plain,
! [X_615,Z_616] :
( ~ p('#skF_3'(X_615,Z_616))
| ~ reachable('#skF_2'(X_615),Z_616)
| ~ reachable(initial_world,X_615) ),
inference(negUnitSimplification,[status(thm)],[c_12532,c_52]) ).
tff(c_12633,plain,
! [X_615] :
( ~ p('#skF_3'(X_615,'#skF_2'(X_615)))
| ~ reachable(initial_world,X_615) ),
inference(resolution,[status(thm)],[c_2,c_12613]) ).
tff(c_13293,plain,
! [X_644] :
( ~ reachable('#skF_1','#skF_2'(X_644))
| ~ reachable(initial_world,X_644) ),
inference(resolution,[status(thm)],[c_13281,c_12633]) ).
tff(c_13317,plain,
( ~ reachable(initial_world,'#skF_2'('#skF_1'))
| ~ reachable(initial_world,'#skF_1') ),
inference(resolution,[status(thm)],[c_12656,c_13293]) ).
tff(c_13348,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_12531,c_12737,c_13317]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SYN550+1 : TPTP v9.0.0. Released v2.2.0.
% 0.12/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.34 % Computer : n026.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Apr 9 08:00:08 EDT 2025
% 0.12/0.34 % CPUTime :
% 9.02/3.19 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.27/3.24
% 9.27/3.24 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------