%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU653^1 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n019.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 : Wed Sep 30 08:30:32 AM UTC 2026
% Result : Theorem 8.18s 1.61s
% Output : Refutation 8.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 41
% Syntax : Number of formulae : 262 ( 59 unt; 0 typ; 33 def)
% Number of atoms : 4875 (1259 equ; 0 cnn)
% Maximal formula atoms : 171 ( 18 avg)
% Number of connectives : 3605 ( 361 ~; 380 |; 736 &;1386 @)
% ( 49 <=>; 693 =>; 0 <=; 0 <~>)
% Maximal formula depth : 176 ( 9 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 383 ( 380 usr; 236 con; 0-4 aty)
% Number of variables : 259 ( 0 sgn 208 !; 51 ?; 259 :)
% Comments :
%------------------------------------------------------------------------------
thf(type_def_5,type,
sTfun: ( $tType * $tType ) > $tType ).
thf(func_def_0,type,
in: $i > $i > $o ).
thf(func_def_1,type,
exu: ( $i > $o ) > $o ).
thf(func_def_3,type,
setextAx: $o ).
thf(func_def_5,type,
emptysetAx: $o ).
thf(func_def_6,type,
setadjoin: $i > $i > $i ).
thf(func_def_7,type,
setadjoinAx: $o ).
thf(func_def_8,type,
powerset: $i > $i ).
thf(func_def_9,type,
powersetAx: $o ).
thf(func_def_10,type,
setunion: $i > $i ).
thf(func_def_11,type,
setunionAx: $o ).
thf(func_def_13,type,
omega0Ax: $o ).
thf(func_def_14,type,
omegaSAx: $o ).
thf(func_def_15,type,
omegaIndAx: $o ).
thf(func_def_16,type,
replAx: $o ).
thf(func_def_17,type,
foundationAx: $o ).
thf(func_def_18,type,
wellorderingAx: $o ).
thf(func_def_19,type,
descr: ( $i > $o ) > $i ).
thf(func_def_20,type,
descrp: $o ).
thf(func_def_21,type,
dsetconstr: $i > ( $i > $o ) > $i ).
thf(func_def_22,type,
dsetconstrI: $o ).
thf(func_def_23,type,
dsetconstrEL: $o ).
thf(func_def_24,type,
dsetconstrER: $o ).
thf(func_def_25,type,
exuE1: $o ).
thf(func_def_26,type,
prop2set: $o > $i ).
thf(func_def_27,type,
prop2setE: $o ).
thf(func_def_28,type,
emptysetE: $o ).
thf(func_def_29,type,
emptysetimpfalse: $o ).
thf(func_def_30,type,
notinemptyset: $o ).
thf(func_def_31,type,
exuE3e: $o ).
thf(func_def_32,type,
setext: $o ).
thf(func_def_33,type,
emptyI: $o ).
thf(func_def_34,type,
noeltsimpempty: $o ).
thf(func_def_35,type,
setbeta: $o ).
thf(func_def_36,type,
nonempty: $i > $o ).
thf(func_def_37,type,
nonemptyE1: $o ).
thf(func_def_38,type,
nonemptyI: $o ).
thf(func_def_39,type,
nonemptyI1: $o ).
thf(func_def_40,type,
setadjoinIL: $o ).
thf(func_def_41,type,
emptyinunitempty: $o ).
thf(func_def_42,type,
setadjoinIR: $o ).
thf(func_def_43,type,
setadjoinE: $o ).
thf(func_def_44,type,
setadjoinOr: $o ).
thf(func_def_45,type,
setoftrueEq: $o ).
thf(func_def_46,type,
powersetI: $o ).
thf(func_def_47,type,
emptyinPowerset: $o ).
thf(func_def_48,type,
emptyInPowerset: $o ).
thf(func_def_49,type,
powersetE: $o ).
thf(func_def_50,type,
setunionI: $o ).
thf(func_def_51,type,
setunionE: $o ).
thf(func_def_52,type,
subPowSU: $o ).
thf(func_def_53,type,
exuE2: $o ).
thf(func_def_54,type,
nonemptyImpWitness: $o ).
thf(func_def_55,type,
uniqinunit: $o ).
thf(func_def_56,type,
notinsingleton: $o ).
thf(func_def_57,type,
eqinunit: $o ).
thf(func_def_58,type,
singletonsswitch: $o ).
thf(func_def_59,type,
upairsetE: $o ).
thf(func_def_60,type,
upairsetIL: $o ).
thf(func_def_61,type,
upairsetIR: $o ).
thf(func_def_62,type,
emptyE1: $o ).
thf(func_def_63,type,
vacuousDall: $o ).
thf(func_def_64,type,
quantDeMorgan1: $o ).
thf(func_def_65,type,
quantDeMorgan2: $o ).
thf(func_def_66,type,
quantDeMorgan3: $o ).
thf(func_def_67,type,
quantDeMorgan4: $o ).
thf(func_def_68,type,
prop2setI: $o ).
thf(func_def_69,type,
set2prop: $i > $o ).
thf(func_def_70,type,
prop2set2propI: $o ).
thf(func_def_71,type,
notdexE: $o ).
thf(func_def_72,type,
notdallE: $o ).
thf(func_def_73,type,
exuI1: $o ).
thf(func_def_74,type,
exuI3: $o ).
thf(func_def_75,type,
exuI2: $o ).
thf(func_def_76,type,
inCongP: $o ).
thf(func_def_77,type,
in__Cong: $o ).
thf(func_def_78,type,
exuE3u: $o ).
thf(func_def_79,type,
exu__Cong: $o ).
thf(func_def_80,type,
emptyset__Cong: $o ).
thf(func_def_81,type,
setadjoin__Cong: $o ).
thf(func_def_82,type,
powerset__Cong: $o ).
thf(func_def_83,type,
setunion__Cong: $o ).
thf(func_def_84,type,
omega__Cong: $o ).
thf(func_def_85,type,
exuEu: $o ).
thf(func_def_86,type,
descr__Cong: $o ).
thf(func_def_87,type,
dsetconstr__Cong: $o ).
thf(func_def_88,type,
subset: $i > $i > $o ).
thf(func_def_89,type,
disjoint: $i > $i > $o ).
thf(func_def_90,type,
setsmeet: $i > $i > $o ).
thf(func_def_91,type,
subsetI1: $o ).
thf(func_def_92,type,
eqimpsubset2: $o ).
thf(func_def_93,type,
eqimpsubset1: $o ).
thf(func_def_94,type,
subsetI2: $o ).
thf(func_def_95,type,
emptysetsubset: $o ).
thf(func_def_96,type,
subsetE: $o ).
thf(func_def_97,type,
subsetE2: $o ).
thf(func_def_98,type,
notsubsetI: $o ).
thf(func_def_99,type,
notequalI1: $o ).
thf(func_def_100,type,
notequalI2: $o ).
thf(func_def_101,type,
subsetRefl: $o ).
thf(func_def_102,type,
subsetTrans: $o ).
thf(func_def_103,type,
setadjoinSub: $o ).
thf(func_def_104,type,
setadjoinSub2: $o ).
thf(func_def_105,type,
subset2powerset: $o ).
thf(func_def_106,type,
setextsub: $o ).
thf(func_def_107,type,
subsetemptysetimpeq: $o ).
thf(func_def_108,type,
powersetI1: $o ).
thf(func_def_109,type,
powersetE1: $o ).
thf(func_def_110,type,
inPowerset: $o ).
thf(func_def_111,type,
powersetsubset: $o ).
thf(func_def_112,type,
sepInPowerset: $o ).
thf(func_def_113,type,
sepSubset: $o ).
thf(func_def_114,type,
binunion: $i > $i > $i ).
thf(func_def_115,type,
binunionIL: $o ).
thf(func_def_116,type,
upairset2IR: $o ).
thf(func_def_117,type,
binunionIR: $o ).
thf(func_def_118,type,
binunionEcases: $o ).
thf(func_def_119,type,
binunionE: $o ).
thf(func_def_120,type,
binunionLsub: $o ).
thf(func_def_121,type,
binunionRsub: $o ).
thf(func_def_122,type,
binintersect: $i > $i > $i ).
thf(func_def_123,type,
binintersectI: $o ).
thf(func_def_124,type,
binintersectSubset5: $o ).
thf(func_def_125,type,
binintersectEL: $o ).
thf(func_def_126,type,
binintersectLsub: $o ).
thf(func_def_127,type,
binintersectSubset2: $o ).
thf(func_def_128,type,
binintersectSubset3: $o ).
thf(func_def_129,type,
binintersectER: $o ).
thf(func_def_130,type,
disjointsetsI1: $o ).
thf(func_def_131,type,
binintersectRsub: $o ).
thf(func_def_132,type,
binintersectSubset4: $o ).
thf(func_def_133,type,
binintersectSubset1: $o ).
thf(func_def_134,type,
bs114d: $o ).
thf(func_def_135,type,
regular: $i > $o ).
thf(func_def_136,type,
setminus: $i > $i > $i ).
thf(func_def_137,type,
setminusI: $o ).
thf(func_def_138,type,
setminusEL: $o ).
thf(func_def_139,type,
setminusER: $o ).
thf(func_def_140,type,
setminusSubset2: $o ).
thf(func_def_141,type,
setminusERneg: $o ).
thf(func_def_142,type,
setminusELneg: $o ).
thf(func_def_143,type,
setminusILneg: $o ).
thf(func_def_144,type,
setminusIRneg: $o ).
thf(func_def_145,type,
setminusLsub: $o ).
thf(func_def_146,type,
setminusSubset1: $o ).
thf(func_def_147,type,
symdiff: $i > $i > $i ).
thf(func_def_148,type,
symdiffE: $o ).
thf(func_def_149,type,
symdiffI1: $o ).
thf(func_def_150,type,
symdiffI2: $o ).
thf(func_def_151,type,
symdiffIneg1: $o ).
thf(func_def_152,type,
symdiffIneg2: $o ).
thf(func_def_153,type,
iskpair: $i > $o ).
thf(func_def_154,type,
secondinupair: $o ).
thf(func_def_155,type,
setukpairIL: $o ).
thf(func_def_156,type,
setukpairIR: $o ).
thf(func_def_157,type,
kpairiskpair: $o ).
thf(func_def_158,type,
kpair: $i > $i > $i ).
thf(func_def_159,type,
kpairp: $o ).
thf(func_def_160,type,
cartprod: $i > $i > $i ).
thf(func_def_161,type,
singletonsubset: $o ).
thf(func_def_162,type,
singletoninpowerset: $o ).
thf(func_def_163,type,
singletoninpowunion: $o ).
thf(func_def_164,type,
upairset2E: $o ).
thf(func_def_165,type,
upairsubunion: $o ).
thf(func_def_166,type,
upairinpowunion: $o ).
thf(func_def_167,type,
ubforcartprodlem1: $o ).
thf(func_def_168,type,
ubforcartprodlem2: $o ).
thf(func_def_169,type,
ubforcartprodlem3: $o ).
thf(func_def_170,type,
cartprodpairin: $o ).
thf(func_def_171,type,
cartprodmempair1: $o ).
thf(func_def_172,type,
cartprodmempair: $o ).
thf(func_def_173,type,
setunionE2: $o ).
thf(func_def_174,type,
setunionsingleton1: $o ).
thf(func_def_175,type,
setunionsingleton2: $o ).
thf(func_def_176,type,
setunionsingleton: $o ).
thf(func_def_177,type,
singleton: $i > $o ).
thf(func_def_178,type,
singletonprop: $o ).
thf(func_def_179,type,
ex1: $i > ( $i > $o ) > $o ).
thf(func_def_180,type,
ex1E1: $o ).
thf(func_def_181,type,
ex1I: $o ).
thf(func_def_182,type,
ex1I2: $o ).
thf(func_def_183,type,
singletonsuniq: $o ).
thf(func_def_184,type,
atmost1p: $i > $o ).
thf(func_def_185,type,
atleast2p: $i > $o ).
thf(func_def_186,type,
atmost2p: $i > $o ).
thf(func_def_187,type,
upairsetp: $i > $o ).
thf(func_def_188,type,
setukpairinjL1: $o ).
thf(func_def_189,type,
kfstsingleton: $o ).
thf(func_def_190,type,
theprop: $o ).
thf(func_def_191,type,
kfst: $i > $i ).
thf(func_def_192,type,
kfstpairEq: $o ).
thf(func_def_193,type,
cartprodfstin: $o ).
thf(func_def_194,type,
setukpairinjL2: $o ).
thf(func_def_195,type,
setukpairinjL: $o ).
thf(func_def_196,type,
setukpairinjR11: $o ).
thf(func_def_197,type,
setukpairinjR12: $o ).
thf(func_def_198,type,
setukpairinjR1: $o ).
thf(func_def_199,type,
upairequniteq: $o ).
thf(func_def_202,type,
db0:
!>[X0: $tType] : X0 ).
thf(func_def_203,type,
vLAM:
!>[X0: $tType,X1: $tType] : ( X1 > X0 > X1 ) ).
thf(func_def_204,type,
vEQ:
!>[X0: $tType] : ( X0 > X0 > $o ) ).
thf(func_def_205,type,
vNOT: $o > $o ).
thf(func_def_206,type,
vSIGMA:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_207,type,
vAND: $o > $o > $o ).
thf(func_def_208,type,
db1:
!>[X0: $tType] : X0 ).
thf(func_def_209,type,
db2:
!>[X0: $tType] : X0 ).
thf(func_def_210,type,
vPI:
!>[X0: $tType] : ( ( X0 > $o ) > $o ) ).
thf(func_def_211,type,
vIMP: $o > $o > $o ).
thf(func_def_212,type,
sP0: $i > $i > $o ).
thf(func_def_213,type,
sP1: $i > $o ).
thf(func_def_214,type,
sP2: $o ).
thf(func_def_221,type,
sK9: $i > $o ).
thf(func_def_229,type,
sK17: ( $i > $o ) > $i ).
thf(func_def_230,type,
sK18: ( $i > $o ) > $i ).
thf(func_def_231,type,
sK19: $i > $o ).
thf(func_def_233,type,
sK21: ( $i > $o ) > $i > $i ).
thf(func_def_235,type,
sK23: $i > $o ).
thf(func_def_240,type,
sK28: $i > $o ).
thf(func_def_245,type,
sK33: $i > $o ).
thf(func_def_247,type,
sK35: ( $i > $o ) > $i > $i ).
thf(func_def_248,type,
sK36: ( $i > $o ) > $i > $i ).
thf(func_def_254,type,
sK42: $i > $i > $i ).
thf(func_def_259,type,
sK47: $i > $o ).
thf(func_def_261,type,
sK49: $i > ( $i > $o ) > $i ).
thf(func_def_271,type,
sK59: $i > $i ).
thf(func_def_278,type,
sK66: $i > $o ).
thf(func_def_281,type,
sK69: $i > ( $i > $o ) > $i ).
thf(func_def_291,type,
sK79: $o ).
thf(func_def_305,type,
sK93: $i > $i > $i ).
thf(func_def_314,type,
sK102: $i > $o ).
thf(func_def_319,type,
sK107: $i > $i ).
thf(func_def_332,type,
sK120: $o ).
thf(func_def_335,type,
sK123: $i > $o ).
thf(func_def_351,type,
sK139: $i > $o ).
thf(func_def_352,type,
sK140: $i > $o ).
thf(func_def_353,type,
sK141: ( $i > $o ) > ( $i > $o ) > $i > $i > $i ).
thf(func_def_354,type,
sK142: ( $i > $o ) > ( $i > $o ) > $i > $i > $i ).
thf(func_def_357,type,
sK145: $i > $o ).
thf(func_def_365,type,
sK153: $i > ( $i > $o ) > $i ).
thf(func_def_366,type,
sK154: $i > $o ).
thf(func_def_385,type,
sK173: $o ).
thf(func_def_386,type,
sK174: $i > $o ).
thf(func_def_392,type,
sK180: $i > $i ).
thf(func_def_393,type,
sK181: $i > $i ).
thf(func_def_394,type,
sK182: $i > $i ).
thf(func_def_395,type,
sK183: $i > $i ).
thf(func_def_396,type,
sK184: $i > $i ).
thf(func_def_397,type,
sK185: $i > $i > $i > $i ).
thf(func_def_398,type,
sK186: $i > $i ).
thf(func_def_399,type,
sK187: $i > $i ).
thf(func_def_400,type,
sK188: $i > $i ).
thf(func_def_401,type,
sK189: $i > $i ).
thf(func_def_402,type,
sK190: $i > $i > $i ).
thf(func_def_403,type,
sK191: $i > $i > $i ).
thf(func_def_404,type,
sK192: $i > $i > $i > $i ).
thf(func_def_405,type,
sK193: $i > $i > $i > $i ).
thf(func_def_406,type,
sK194: $i > $i > $i > $i ).
thf(func_def_407,type,
sK195: $i > $i > $i ).
thf(func_def_408,type,
sK196: $i > $i > $i ).
thf(func_def_409,type,
sK197: $i > $i > $i ).
thf(func_def_410,type,
sK198: $i > $i > $i ).
thf(func_def_411,type,
sK199: $i > $i > $i ).
thf(func_def_415,type,
sK203: $o ).
thf(func_def_418,type,
sK206: $i > $o ).
thf(func_def_432,type,
sK220: $i > $i > $i ).
thf(func_def_436,type,
sK224: $i > $o ).
thf(func_def_438,type,
sK226: ( $i > $o ) > $i > $i ).
thf(func_def_439,type,
sK227: ( $i > $o ) > ( $i > $o ) > $i ).
thf(func_def_440,type,
sK228: ( $i > $o ) > ( $i > $o ) > $i ).
thf(func_def_441,type,
sK229: $i > $o ).
thf(func_def_442,type,
sK230: $i > $o ).
thf(func_def_460,type,
sK248: $i > $i ).
thf(func_def_471,type,
sK259: $i > $i > $i > $i ).
thf(func_def_472,type,
sK260: $i > $i > $i > $i ).
thf(func_def_475,type,
sK263: $i > $o ).
thf(func_def_482,type,
sK270: $i > $i > $i ).
thf(func_def_488,type,
sK276: $i > $o ).
thf(func_def_489,type,
sK277: $i > $o ).
thf(func_def_490,type,
sK278: ( $i > $o ) > ( $i > $o ) > $i ).
thf(func_def_491,type,
sK279: ( $i > $o ) > ( $i > $o ) > $i ).
thf(func_def_507,type,
sK295: $i > $i > $o ).
thf(func_def_508,type,
sK296: $i > $i ).
thf(func_def_509,type,
sK297: $i > $i ).
thf(func_def_510,type,
sK298: ( $i > $i > $o ) > $i > $i ).
thf(func_def_511,type,
sK299: ( $i > $i > $o ) > $i > $i ).
thf(func_def_512,type,
sK300: $i > ( $i > $i > $o ) > $i > $i ).
thf(func_def_515,type,
sK303: $i > $o ).
thf(func_def_527,type,
sK315: $i > $i > $i ).
thf(func_def_530,type,
sK318: $i > $i > $i ).
thf(func_def_533,type,
sK321: $i > $i ).
thf(func_def_542,type,
sK330: ( $i > $o ) > $i > $i ).
thf(func_def_544,type,
sK332: $i > $o ).
thf(func_def_547,type,
sK335: $o ).
thf(func_def_558,type,
sK346: $i > ( $i > $o ) > $i ).
thf(func_def_559,type,
sK347: $i > $o ).
thf(func_def_565,type,
sK353: $i > $o ).
thf(func_def_572,type,
sK360: $i > $o ).
thf(func_def_573,type,
sK361: ( $i > $o ) > $i ).
thf(func_def_586,type,
sK374: $o ).
thf(func_def_590,type,
sK378: $i > ( $i > $o ) > $i > $i ).
thf(func_def_592,type,
sK380: $i > $o ).
thf(func_def_594,type,
sK382: $o > $i > $i > $i ).
thf(func_def_597,type,
sK385: $o ).
thf(func_def_600,type,
sK388: $i > $i > $i ).
thf(func_def_632,type,
sK420: $o ).
thf(func_def_643,type,
sK431: $i > $o ).
thf(func_def_644,type,
sK432: ( $i > $o ) > $i ).
thf(func_def_645,type,
sK433: $i > $o ).
thf(func_def_646,type,
sK434: $i > $i ).
thf(func_def_647,type,
sK435: $i > $o ).
thf(func_def_649,type,
sK437: $i > ( $i > $o ) > $i ).
thf(func_def_651,type,
sK439: $i > $i ).
thf(func_def_653,type,
sK441: $i > $i ).
thf(func_def_655,type,
sK443: $i > $i ).
thf(func_def_658,type,
sK446: $i > $i > $i ).
thf(func_def_659,type,
sK447: $i > ( $i > $o ) > $i ).
thf(func_def_660,type,
sK448: $i > $o ).
thf(func_def_663,type,
sK451: ( $i > $o ) > $i ).
thf(func_def_664,type,
sK452: $i > $o ).
thf(func_def_665,type,
sK453: $i > $i ).
thf(func_def_666,type,
sK454: $i > $o ).
thf(func_def_675,type,
sK463: $i > $o ).
thf(func_def_677,type,
sK465: ( $i > $o ) > $i > $i ).
thf(func_def_678,type,
sK466: ( $i > $o ) > $i > $i ).
thf(f4,axiom,
( setadjoinAx
= ( ! [X2: $i,X0: $i,X1: $i] :
( ( in @ X2 @ ( setadjoin @ X0 @ X1 ) )
<=> ( ( X2 = X0 )
| ( in @ X2 @ X1 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',setadjoinAx) ).
thf(f46,axiom,
! [X1: $i,X0: $i] :
( ( ( in @ X0 @ ( setadjoin @ X1 @ emptyset ) )
=> ( X0 = X1 ) )
= uniqinunit ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',uniqinunit) ).
thf(f136,axiom,
( secondinupair
= ( ! [X1: $i,X0: $i] : ( in @ X1 @ ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',secondinupair) ).
thf(f145,axiom,
! [X2: $i,X1: $i,X0: $i] :
( ( ( in @ X2 @ ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) ) )
=> ( ( X2 = X1 )
| ( X2 = X0 ) ) )
= upairset2E ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',upairset2E) ).
thf(f165,axiom,
! [X0: $i,X2: $i,X1: $i] :
( ( ( in @ ( setadjoin @ X2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) ) )
=> ( X0 = X2 ) )
= setukpairinjL1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',setukpairinjL1) ).
thf(f172,axiom,
! [X0: $i,X1: $i] :
( ( ( X0 = X1 )
=> ( ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) )
= ( setadjoin @ X0 @ emptyset ) ) )
= setukpairinjR11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',setukpairinjR11) ).
thf(f175,axiom,
! [X0: $i,X1: $i,X2: $i] :
( ( ( ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) )
= ( setadjoin @ X2 @ emptyset ) )
=> ( X0 = X1 ) )
= upairequniteq ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',upairequniteq) ).
thf(f176,conjecture,
( setextAx
=> ( emptysetAx
=> ( setadjoinAx
=> ( powersetAx
=> ( setunionAx
=> ( omega0Ax
=> ( omegaSAx
=> ( omegaIndAx
=> ( replAx
=> ( foundationAx
=> ( wellorderingAx
=> ( descrp
=> ( dsetconstrI
=> ( dsetconstrEL
=> ( dsetconstrER
=> ( exuE1
=> ( prop2setE
=> ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( subPowSU
=> ( exuE2
=> ( nonemptyImpWitness
=> ( uniqinunit
=> ( notinsingleton
=> ( eqinunit
=> ( singletonsswitch
=> ( upairsetE
=> ( upairsetIL
=> ( upairsetIR
=> ( emptyE1
=> ( vacuousDall
=> ( quantDeMorgan1
=> ( quantDeMorgan2
=> ( quantDeMorgan3
=> ( quantDeMorgan4
=> ( prop2setI
=> ( prop2set2propI
=> ( notdexE
=> ( notdallE
=> ( exuI1
=> ( exuI3
=> ( exuI2
=> ( inCongP
=> ( in__Cong
=> ( exuE3u
=> ( exu__Cong
=> ( emptyset__Cong
=> ( setadjoin__Cong
=> ( powerset__Cong
=> ( setunion__Cong
=> ( omega__Cong
=> ( exuEu
=> ( descr__Cong
=> ( dsetconstr__Cong
=> ( subsetI1
=> ( eqimpsubset2
=> ( eqimpsubset1
=> ( subsetI2
=> ( emptysetsubset
=> ( subsetE
=> ( subsetE2
=> ( notsubsetI
=> ( notequalI1
=> ( notequalI2
=> ( subsetRefl
=> ( subsetTrans
=> ( setadjoinSub
=> ( setadjoinSub2
=> ( subset2powerset
=> ( setextsub
=> ( subsetemptysetimpeq
=> ( powersetI1
=> ( powersetE1
=> ( inPowerset
=> ( powersetsubset
=> ( sepInPowerset
=> ( sepSubset
=> ( binunionIL
=> ( upairset2IR
=> ( binunionIR
=> ( binunionEcases
=> ( binunionE
=> ( binunionLsub
=> ( binunionRsub
=> ( binintersectI
=> ( binintersectSubset5
=> ( binintersectEL
=> ( binintersectLsub
=> ( binintersectSubset2
=> ( binintersectSubset3
=> ( binintersectER
=> ( disjointsetsI1
=> ( binintersectRsub
=> ( binintersectSubset4
=> ( binintersectSubset1
=> ( bs114d
=> ( setminusI
=> ( setminusEL
=> ( setminusER
=> ( setminusSubset2
=> ( setminusERneg
=> ( setminusELneg
=> ( setminusILneg
=> ( setminusIRneg
=> ( setminusLsub
=> ( setminusSubset1
=> ( symdiffE
=> ( symdiffI1
=> ( symdiffI2
=> ( symdiffIneg1
=> ( symdiffIneg2
=> ( secondinupair
=> ( setukpairIL
=> ( setukpairIR
=> ( kpairiskpair
=> ( kpairp
=> ( singletonsubset
=> ( singletoninpowerset
=> ( singletoninpowunion
=> ( upairset2E
=> ( upairsubunion
=> ( upairinpowunion
=> ( ubforcartprodlem1
=> ( ubforcartprodlem2
=> ( ubforcartprodlem3
=> ( cartprodpairin
=> ( cartprodmempair1
=> ( cartprodmempair
=> ( setunionE2
=> ( setunionsingleton1
=> ( setunionsingleton2
=> ( setunionsingleton
=> ( singletonprop
=> ( ex1E1
=> ( ex1I
=> ( ex1I2
=> ( singletonsuniq
=> ( setukpairinjL1
=> ( kfstsingleton
=> ( theprop
=> ( kfstpairEq
=> ( cartprodfstin
=> ( setukpairinjL2
=> ( setukpairinjL
=> ( setukpairinjR11
=> ( setukpairinjR12
=> ( setukpairinjR1
=> ( upairequniteq
=> ! [X0: $i,X2: $i,X1: $i,X3: $i] :
( ( ( setadjoin @ ( setadjoin @ X0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ X2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X2 @ ( setadjoin @ X3 @ emptyset ) ) @ emptyset ) ) )
=> ( X1 = X3 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',setukpairinjR2) ).
thf(f177,negated_conjecture,
~ ( setextAx
=> ( emptysetAx
=> ( setadjoinAx
=> ( powersetAx
=> ( setunionAx
=> ( omega0Ax
=> ( omegaSAx
=> ( omegaIndAx
=> ( replAx
=> ( foundationAx
=> ( wellorderingAx
=> ( descrp
=> ( dsetconstrI
=> ( dsetconstrEL
=> ( dsetconstrER
=> ( exuE1
=> ( prop2setE
=> ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( subPowSU
=> ( exuE2
=> ( nonemptyImpWitness
=> ( uniqinunit
=> ( notinsingleton
=> ( eqinunit
=> ( singletonsswitch
=> ( upairsetE
=> ( upairsetIL
=> ( upairsetIR
=> ( emptyE1
=> ( vacuousDall
=> ( quantDeMorgan1
=> ( quantDeMorgan2
=> ( quantDeMorgan3
=> ( quantDeMorgan4
=> ( prop2setI
=> ( prop2set2propI
=> ( notdexE
=> ( notdallE
=> ( exuI1
=> ( exuI3
=> ( exuI2
=> ( inCongP
=> ( in__Cong
=> ( exuE3u
=> ( exu__Cong
=> ( emptyset__Cong
=> ( setadjoin__Cong
=> ( powerset__Cong
=> ( setunion__Cong
=> ( omega__Cong
=> ( exuEu
=> ( descr__Cong
=> ( dsetconstr__Cong
=> ( subsetI1
=> ( eqimpsubset2
=> ( eqimpsubset1
=> ( subsetI2
=> ( emptysetsubset
=> ( subsetE
=> ( subsetE2
=> ( notsubsetI
=> ( notequalI1
=> ( notequalI2
=> ( subsetRefl
=> ( subsetTrans
=> ( setadjoinSub
=> ( setadjoinSub2
=> ( subset2powerset
=> ( setextsub
=> ( subsetemptysetimpeq
=> ( powersetI1
=> ( powersetE1
=> ( inPowerset
=> ( powersetsubset
=> ( sepInPowerset
=> ( sepSubset
=> ( binunionIL
=> ( upairset2IR
=> ( binunionIR
=> ( binunionEcases
=> ( binunionE
=> ( binunionLsub
=> ( binunionRsub
=> ( binintersectI
=> ( binintersectSubset5
=> ( binintersectEL
=> ( binintersectLsub
=> ( binintersectSubset2
=> ( binintersectSubset3
=> ( binintersectER
=> ( disjointsetsI1
=> ( binintersectRsub
=> ( binintersectSubset4
=> ( binintersectSubset1
=> ( bs114d
=> ( setminusI
=> ( setminusEL
=> ( setminusER
=> ( setminusSubset2
=> ( setminusERneg
=> ( setminusELneg
=> ( setminusILneg
=> ( setminusIRneg
=> ( setminusLsub
=> ( setminusSubset1
=> ( symdiffE
=> ( symdiffI1
=> ( symdiffI2
=> ( symdiffIneg1
=> ( symdiffIneg2
=> ( secondinupair
=> ( setukpairIL
=> ( setukpairIR
=> ( kpairiskpair
=> ( kpairp
=> ( singletonsubset
=> ( singletoninpowerset
=> ( singletoninpowunion
=> ( upairset2E
=> ( upairsubunion
=> ( upairinpowunion
=> ( ubforcartprodlem1
=> ( ubforcartprodlem2
=> ( ubforcartprodlem3
=> ( cartprodpairin
=> ( cartprodmempair1
=> ( cartprodmempair
=> ( setunionE2
=> ( setunionsingleton1
=> ( setunionsingleton2
=> ( setunionsingleton
=> ( singletonprop
=> ( ex1E1
=> ( ex1I
=> ( ex1I2
=> ( singletonsuniq
=> ( setukpairinjL1
=> ( kfstsingleton
=> ( theprop
=> ( kfstpairEq
=> ( cartprodfstin
=> ( setukpairinjL2
=> ( setukpairinjL
=> ( setukpairinjR11
=> ( setukpairinjR12
=> ( setukpairinjR1
=> ( upairequniteq
=> ! [X0: $i,X2: $i,X1: $i,X3: $i] :
( ( ( setadjoin @ ( setadjoin @ X0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ X2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X2 @ ( setadjoin @ X3 @ emptyset ) ) @ emptyset ) ) )
=> ( X1 = X3 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f176]) ).
thf(f187,plain,
( setadjoinAx
= ( ! [X0: $i,X1: $i,X2: $i] :
( ( in @ X0 @ ( setadjoin @ X1 @ X2 ) )
<=> ( ( X0 = X1 )
| ( in @ X0 @ X2 ) ) ) ) ),
inference(rectify,[],[f4]) ).
thf(f188,plain,
( ! [X0: $i,X2: $i,X1: $i] :
( ( ( $true
= ( in @ X0 @ X2 ) )
| ( X0 = X1 ) )
<=> ( $true
= ( in @ X0 @ ( setadjoin @ X1 @ X2 ) ) ) )
<=> ( setadjoinAx = $true ) ),
inference(fool_elimination,[],[f187]) ).
thf(f223,plain,
~ ( setextAx
=> ( emptysetAx
=> ( setadjoinAx
=> ( powersetAx
=> ( setunionAx
=> ( omega0Ax
=> ( omegaSAx
=> ( omegaIndAx
=> ( replAx
=> ( foundationAx
=> ( wellorderingAx
=> ( descrp
=> ( dsetconstrI
=> ( dsetconstrEL
=> ( dsetconstrER
=> ( exuE1
=> ( prop2setE
=> ( emptysetE
=> ( emptysetimpfalse
=> ( notinemptyset
=> ( exuE3e
=> ( setext
=> ( emptyI
=> ( noeltsimpempty
=> ( setbeta
=> ( nonemptyE1
=> ( nonemptyI
=> ( nonemptyI1
=> ( setadjoinIL
=> ( emptyinunitempty
=> ( setadjoinIR
=> ( setadjoinE
=> ( setadjoinOr
=> ( setoftrueEq
=> ( powersetI
=> ( emptyinPowerset
=> ( emptyInPowerset
=> ( powersetE
=> ( setunionI
=> ( setunionE
=> ( subPowSU
=> ( exuE2
=> ( nonemptyImpWitness
=> ( uniqinunit
=> ( notinsingleton
=> ( eqinunit
=> ( singletonsswitch
=> ( upairsetE
=> ( upairsetIL
=> ( upairsetIR
=> ( emptyE1
=> ( vacuousDall
=> ( quantDeMorgan1
=> ( quantDeMorgan2
=> ( quantDeMorgan3
=> ( quantDeMorgan4
=> ( prop2setI
=> ( prop2set2propI
=> ( notdexE
=> ( notdallE
=> ( exuI1
=> ( exuI3
=> ( exuI2
=> ( inCongP
=> ( in__Cong
=> ( exuE3u
=> ( exu__Cong
=> ( emptyset__Cong
=> ( setadjoin__Cong
=> ( powerset__Cong
=> ( setunion__Cong
=> ( omega__Cong
=> ( exuEu
=> ( descr__Cong
=> ( dsetconstr__Cong
=> ( subsetI1
=> ( eqimpsubset2
=> ( eqimpsubset1
=> ( subsetI2
=> ( emptysetsubset
=> ( subsetE
=> ( subsetE2
=> ( notsubsetI
=> ( notequalI1
=> ( notequalI2
=> ( subsetRefl
=> ( subsetTrans
=> ( setadjoinSub
=> ( setadjoinSub2
=> ( subset2powerset
=> ( setextsub
=> ( subsetemptysetimpeq
=> ( powersetI1
=> ( powersetE1
=> ( inPowerset
=> ( powersetsubset
=> ( sepInPowerset
=> ( sepSubset
=> ( binunionIL
=> ( upairset2IR
=> ( binunionIR
=> ( binunionEcases
=> ( binunionE
=> ( binunionLsub
=> ( binunionRsub
=> ( binintersectI
=> ( binintersectSubset5
=> ( binintersectEL
=> ( binintersectLsub
=> ( binintersectSubset2
=> ( binintersectSubset3
=> ( binintersectER
=> ( disjointsetsI1
=> ( binintersectRsub
=> ( binintersectSubset4
=> ( binintersectSubset1
=> ( bs114d
=> ( setminusI
=> ( setminusEL
=> ( setminusER
=> ( setminusSubset2
=> ( setminusERneg
=> ( setminusELneg
=> ( setminusILneg
=> ( setminusIRneg
=> ( setminusLsub
=> ( setminusSubset1
=> ( symdiffE
=> ( symdiffI1
=> ( symdiffI2
=> ( symdiffIneg1
=> ( symdiffIneg2
=> ( secondinupair
=> ( setukpairIL
=> ( setukpairIR
=> ( kpairiskpair
=> ( kpairp
=> ( singletonsubset
=> ( singletoninpowerset
=> ( singletoninpowunion
=> ( upairset2E
=> ( upairsubunion
=> ( upairinpowunion
=> ( ubforcartprodlem1
=> ( ubforcartprodlem2
=> ( ubforcartprodlem3
=> ( cartprodpairin
=> ( cartprodmempair1
=> ( cartprodmempair
=> ( setunionE2
=> ( setunionsingleton1
=> ( setunionsingleton2
=> ( setunionsingleton
=> ( singletonprop
=> ( ex1E1
=> ( ex1I
=> ( ex1I2
=> ( singletonsuniq
=> ( setukpairinjL1
=> ( kfstsingleton
=> ( theprop
=> ( kfstpairEq
=> ( cartprodfstin
=> ( setukpairinjL2
=> ( setukpairinjL
=> ( setukpairinjR11
=> ( setukpairinjR12
=> ( setukpairinjR1
=> ( upairequniteq
=> ! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( ( setadjoin @ ( setadjoin @ X1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X1 @ ( setadjoin @ X3 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ X0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ ( setadjoin @ X2 @ emptyset ) ) @ emptyset ) ) )
=> ( X2 = X3 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(rectify,[],[f177]) ).
thf(f224,plain,
~ ( ( setextAx = $true )
=> ( ( emptysetAx = $true )
=> ( ( setadjoinAx = $true )
=> ( ( powersetAx = $true )
=> ( ( setunionAx = $true )
=> ( ( omega0Ax = $true )
=> ( ( omegaSAx = $true )
=> ( ( omegaIndAx = $true )
=> ( ( replAx = $true )
=> ( ( foundationAx = $true )
=> ( ( wellorderingAx = $true )
=> ( ( descrp = $true )
=> ( ( dsetconstrI = $true )
=> ( ( dsetconstrEL = $true )
=> ( ( dsetconstrER = $true )
=> ( ( exuE1 = $true )
=> ( ( prop2setE = $true )
=> ( ( emptysetE = $true )
=> ( ( emptysetimpfalse = $true )
=> ( ( notinemptyset = $true )
=> ( ( exuE3e = $true )
=> ( ( setext = $true )
=> ( ( emptyI = $true )
=> ( ( noeltsimpempty = $true )
=> ( ( setbeta = $true )
=> ( ( nonemptyE1 = $true )
=> ( ( nonemptyI = $true )
=> ( ( nonemptyI1 = $true )
=> ( ( setadjoinIL = $true )
=> ( ( emptyinunitempty = $true )
=> ( ( setadjoinIR = $true )
=> ( ( setadjoinE = $true )
=> ( ( setadjoinOr = $true )
=> ( ( setoftrueEq = $true )
=> ( ( powersetI = $true )
=> ( ( emptyinPowerset = $true )
=> ( ( emptyInPowerset = $true )
=> ( ( powersetE = $true )
=> ( ( setunionI = $true )
=> ( ( setunionE = $true )
=> ( ( subPowSU = $true )
=> ( ( exuE2 = $true )
=> ( ( nonemptyImpWitness = $true )
=> ( ( uniqinunit = $true )
=> ( ( notinsingleton = $true )
=> ( ( eqinunit = $true )
=> ( ( singletonsswitch = $true )
=> ( ( upairsetE = $true )
=> ( ( upairsetIL = $true )
=> ( ( upairsetIR = $true )
=> ( ( emptyE1 = $true )
=> ( ( vacuousDall = $true )
=> ( ( quantDeMorgan1 = $true )
=> ( ( quantDeMorgan2 = $true )
=> ( ( quantDeMorgan3 = $true )
=> ( ( quantDeMorgan4 = $true )
=> ( ( prop2setI = $true )
=> ( ( prop2set2propI = $true )
=> ( ( notdexE = $true )
=> ( ( notdallE = $true )
=> ( ( exuI1 = $true )
=> ( ( exuI3 = $true )
=> ( ( exuI2 = $true )
=> ( ( inCongP = $true )
=> ( ( in__Cong = $true )
=> ( ( exuE3u = $true )
=> ( ( exu__Cong = $true )
=> ( ( emptyset__Cong = $true )
=> ( ( setadjoin__Cong = $true )
=> ( ( powerset__Cong = $true )
=> ( ( setunion__Cong = $true )
=> ( ( omega__Cong = $true )
=> ( ( exuEu = $true )
=> ( ( descr__Cong = $true )
=> ( ( dsetconstr__Cong = $true )
=> ( ( subsetI1 = $true )
=> ( ( eqimpsubset2 = $true )
=> ( ( eqimpsubset1 = $true )
=> ( ( subsetI2 = $true )
=> ( ( emptysetsubset = $true )
=> ( ( subsetE = $true )
=> ( ( subsetE2 = $true )
=> ( ( notsubsetI = $true )
=> ( ( notequalI1 = $true )
=> ( ( notequalI2 = $true )
=> ( ( subsetRefl = $true )
=> ( ( subsetTrans = $true )
=> ( ( setadjoinSub = $true )
=> ( ( setadjoinSub2 = $true )
=> ( ( subset2powerset = $true )
=> ( ( setextsub = $true )
=> ( ( subsetemptysetimpeq = $true )
=> ( ( powersetI1 = $true )
=> ( ( powersetE1 = $true )
=> ( ( inPowerset = $true )
=> ( ( powersetsubset = $true )
=> ( ( sepInPowerset = $true )
=> ( ( sepSubset = $true )
=> ( ( binunionIL = $true )
=> ( ( upairset2IR = $true )
=> ( ( binunionIR = $true )
=> ( ( binunionEcases = $true )
=> ( ( binunionE = $true )
=> ( ( binunionLsub = $true )
=> ( ( binunionRsub = $true )
=> ( ( binintersectI = $true )
=> ( ( binintersectSubset5 = $true )
=> ( ( binintersectEL = $true )
=> ( ( binintersectLsub = $true )
=> ( ( binintersectSubset2 = $true )
=> ( ( binintersectSubset3 = $true )
=> ( ( binintersectER = $true )
=> ( ( disjointsetsI1 = $true )
=> ( ( binintersectRsub = $true )
=> ( ( binintersectSubset4 = $true )
=> ( ( binintersectSubset1 = $true )
=> ( ( bs114d = $true )
=> ( ( setminusI = $true )
=> ( ( setminusEL = $true )
=> ( ( setminusER = $true )
=> ( ( setminusSubset2 = $true )
=> ( ( setminusERneg = $true )
=> ( ( setminusELneg = $true )
=> ( ( setminusILneg = $true )
=> ( ( setminusIRneg = $true )
=> ( ( setminusLsub = $true )
=> ( ( setminusSubset1 = $true )
=> ( ( symdiffE = $true )
=> ( ( symdiffI1 = $true )
=> ( ( symdiffI2 = $true )
=> ( ( symdiffIneg1 = $true )
=> ( ( symdiffIneg2 = $true )
=> ( ( secondinupair = $true )
=> ( ( setukpairIL = $true )
=> ( ( setukpairIR = $true )
=> ( ( kpairiskpair = $true )
=> ( ( kpairp = $true )
=> ( ( singletonsubset = $true )
=> ( ( singletoninpowerset = $true )
=> ( ( singletoninpowunion = $true )
=> ( ( upairset2E = $true )
=> ( ( upairsubunion = $true )
=> ( ( upairinpowunion = $true )
=> ( ( ubforcartprodlem1 = $true )
=> ( ( ubforcartprodlem2 = $true )
=> ( ( ubforcartprodlem3 = $true )
=> ( ( cartprodpairin = $true )
=> ( ( cartprodmempair1 = $true )
=> ( ( cartprodmempair = $true )
=> ( ( setunionE2 = $true )
=> ( ( setunionsingleton1 = $true )
=> ( ( setunionsingleton2 = $true )
=> ( ( setunionsingleton = $true )
=> ( ( singletonprop = $true )
=> ( ( ex1E1 = $true )
=> ( ( ex1I = $true )
=> ( ( ex1I2 = $true )
=> ( ( singletonsuniq = $true )
=> ( ( setukpairinjL1 = $true )
=> ( ( kfstsingleton = $true )
=> ( ( theprop = $true )
=> ( ( kfstpairEq = $true )
=> ( ( cartprodfstin = $true )
=> ( ( setukpairinjL2 = $true )
=> ( ( setukpairinjL = $true )
=> ( ( setukpairinjR11 = $true )
=> ( ( setukpairinjR12 = $true )
=> ( ( setukpairinjR1 = $true )
=> ( ( upairequniteq = $true )
=> ! [X2: $i,X1: $i,X0: $i,X3: $i] :
( ( ( setadjoin @ ( setadjoin @ X1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X1 @ ( setadjoin @ X3 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ X0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ ( setadjoin @ X2 @ emptyset ) ) @ emptyset ) ) )
=> ( X2 = X3 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
inference(fool_elimination,[],[f223]) ).
thf(f375,plain,
( ( upairequniteq = $true )
<=> ! [X2: $i,X0: $i,X1: $i] :
( ( ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) )
= ( setadjoin @ X2 @ emptyset ) )
=> ( X0 = X1 ) ) ),
inference(fool_elimination,[],[f175]) ).
thf(f406,plain,
( secondinupair
= ( ! [X0: $i,X1: $i] : ( in @ X0 @ ( setadjoin @ X1 @ ( setadjoin @ X0 @ emptyset ) ) ) ) ),
inference(rectify,[],[f136]) ).
thf(f407,plain,
( ( secondinupair = $true )
<=> ! [X1: $i,X0: $i] :
( ( in @ X0 @ ( setadjoin @ X1 @ ( setadjoin @ X0 @ emptyset ) ) )
= $true ) ),
inference(fool_elimination,[],[f406]) ).
thf(f410,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( ( in @ X0 @ ( setadjoin @ X2 @ ( setadjoin @ X1 @ emptyset ) ) )
=> ( ( X0 = X1 )
| ( X2 = X0 ) ) )
= upairset2E ),
inference(rectify,[],[f145]) ).
thf(f411,plain,
( ( upairset2E = $true )
<=> ! [X0: $i,X2: $i,X1: $i] :
( ( ( in @ X0 @ ( setadjoin @ X2 @ ( setadjoin @ X1 @ emptyset ) ) )
= $true )
=> ( ( X0 = X1 )
| ( X0 = X2 ) ) ) ),
inference(fool_elimination,[],[f410]) ).
thf(f442,plain,
( ! [X1: $i,X0: $i] :
( ( X0 = X1 )
=> ( ( setadjoin @ X0 @ emptyset )
= ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) ) ) )
<=> ( setukpairinjR11 = $true ) ),
inference(fool_elimination,[],[f172]) ).
thf(f470,plain,
! [X0: $i,X1: $i] :
( ( ( in @ X1 @ ( setadjoin @ X0 @ emptyset ) )
=> ( X0 = X1 ) )
= uniqinunit ),
inference(rectify,[],[f46]) ).
thf(f471,plain,
( ! [X1: $i,X0: $i] :
( ( ( in @ X1 @ ( setadjoin @ X0 @ emptyset ) )
= $true )
=> ( X0 = X1 ) )
<=> ( uniqinunit = $true ) ),
inference(fool_elimination,[],[f470]) ).
thf(f485,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( ( in @ ( setadjoin @ X1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ ( setadjoin @ X2 @ emptyset ) ) @ emptyset ) ) )
=> ( X0 = X1 ) )
= setukpairinjL1 ),
inference(rectify,[],[f165]) ).
thf(f486,plain,
( ( setukpairinjL1 = $true )
<=> ! [X2: $i,X0: $i,X1: $i] :
( ( ( in @ ( setadjoin @ X1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ ( setadjoin @ X2 @ emptyset ) ) @ emptyset ) ) )
= $true )
=> ( X0 = X1 ) ) ),
inference(fool_elimination,[],[f485]) ).
thf(f568,plain,
( ! [X2: $i,X1: $i,X0: $i] :
( ( X0 = X1 )
| ( ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) )
!= ( setadjoin @ X2 @ emptyset ) ) )
<=> ( upairequniteq = $true ) ),
inference(ennf_transformation,[],[f375]) ).
thf(f590,plain,
( ( upairset2E = $true )
<=> ! [X0: $i,X2: $i,X1: $i] :
( ( X0 = X1 )
| ( X0 = X2 )
| ( ( in @ X0 @ ( setadjoin @ X2 @ ( setadjoin @ X1 @ emptyset ) ) )
!= $true ) ) ),
inference(ennf_transformation,[],[f411]) ).
thf(f591,plain,
( ( upairset2E = $true )
<=> ! [X2: $i,X0: $i,X1: $i] :
( ( ( in @ X0 @ ( setadjoin @ X2 @ ( setadjoin @ X1 @ emptyset ) ) )
!= $true )
| ( X0 = X1 )
| ( X0 = X2 ) ) ),
inference(flattening,[],[f590]) ).
thf(f602,plain,
( ( uniqinunit = $true )
<=> ! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ( ( in @ X1 @ ( setadjoin @ X0 @ emptyset ) )
!= $true ) ) ),
inference(ennf_transformation,[],[f471]) ).
thf(f614,plain,
( ( setukpairinjR11 = $true )
<=> ! [X1: $i,X0: $i] :
( ( X0 != X1 )
| ( ( setadjoin @ X0 @ emptyset )
= ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) ) ) ) ),
inference(ennf_transformation,[],[f442]) ).
thf(f688,plain,
( ! [X0: $i,X1: $i,X2: $i] :
( ( ( in @ ( setadjoin @ X1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ ( setadjoin @ X2 @ emptyset ) ) @ emptyset ) ) )
!= $true )
| ( X0 = X1 ) )
<=> ( setukpairinjL1 = $true ) ),
inference(ennf_transformation,[],[f486]) ).
thf(f722,plain,
( ? [X2: $i,X1: $i,X0: $i,X3: $i] :
( ( ( setadjoin @ ( setadjoin @ X1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X1 @ ( setadjoin @ X3 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ X0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ ( setadjoin @ X2 @ emptyset ) ) @ emptyset ) ) )
& ( X2 != X3 ) )
& ( upairequniteq = $true )
& ( setukpairinjR1 = $true )
& ( setukpairinjR12 = $true )
& ( setukpairinjR11 = $true )
& ( setukpairinjL = $true )
& ( setukpairinjL2 = $true )
& ( cartprodfstin = $true )
& ( kfstpairEq = $true )
& ( theprop = $true )
& ( kfstsingleton = $true )
& ( setukpairinjL1 = $true )
& ( singletonsuniq = $true )
& ( ex1I2 = $true )
& ( ex1I = $true )
& ( ex1E1 = $true )
& ( singletonprop = $true )
& ( setunionsingleton = $true )
& ( setunionsingleton2 = $true )
& ( setunionsingleton1 = $true )
& ( setunionE2 = $true )
& ( cartprodmempair = $true )
& ( cartprodmempair1 = $true )
& ( cartprodpairin = $true )
& ( ubforcartprodlem3 = $true )
& ( ubforcartprodlem2 = $true )
& ( ubforcartprodlem1 = $true )
& ( upairinpowunion = $true )
& ( upairsubunion = $true )
& ( upairset2E = $true )
& ( singletoninpowunion = $true )
& ( singletoninpowerset = $true )
& ( singletonsubset = $true )
& ( kpairp = $true )
& ( kpairiskpair = $true )
& ( setukpairIR = $true )
& ( setukpairIL = $true )
& ( secondinupair = $true )
& ( symdiffIneg2 = $true )
& ( symdiffIneg1 = $true )
& ( symdiffI2 = $true )
& ( symdiffI1 = $true )
& ( symdiffE = $true )
& ( setminusSubset1 = $true )
& ( setminusLsub = $true )
& ( setminusIRneg = $true )
& ( setminusILneg = $true )
& ( setminusELneg = $true )
& ( setminusERneg = $true )
& ( setminusSubset2 = $true )
& ( setminusER = $true )
& ( setminusEL = $true )
& ( setminusI = $true )
& ( bs114d = $true )
& ( binintersectSubset1 = $true )
& ( binintersectSubset4 = $true )
& ( binintersectRsub = $true )
& ( disjointsetsI1 = $true )
& ( binintersectER = $true )
& ( binintersectSubset3 = $true )
& ( binintersectSubset2 = $true )
& ( binintersectLsub = $true )
& ( binintersectEL = $true )
& ( binintersectSubset5 = $true )
& ( binintersectI = $true )
& ( binunionRsub = $true )
& ( binunionLsub = $true )
& ( binunionE = $true )
& ( binunionEcases = $true )
& ( binunionIR = $true )
& ( upairset2IR = $true )
& ( binunionIL = $true )
& ( sepSubset = $true )
& ( sepInPowerset = $true )
& ( powersetsubset = $true )
& ( inPowerset = $true )
& ( powersetE1 = $true )
& ( powersetI1 = $true )
& ( subsetemptysetimpeq = $true )
& ( setextsub = $true )
& ( subset2powerset = $true )
& ( setadjoinSub2 = $true )
& ( setadjoinSub = $true )
& ( subsetTrans = $true )
& ( subsetRefl = $true )
& ( notequalI2 = $true )
& ( notequalI1 = $true )
& ( notsubsetI = $true )
& ( subsetE2 = $true )
& ( subsetE = $true )
& ( emptysetsubset = $true )
& ( subsetI2 = $true )
& ( eqimpsubset1 = $true )
& ( eqimpsubset2 = $true )
& ( subsetI1 = $true )
& ( dsetconstr__Cong = $true )
& ( descr__Cong = $true )
& ( exuEu = $true )
& ( omega__Cong = $true )
& ( setunion__Cong = $true )
& ( powerset__Cong = $true )
& ( setadjoin__Cong = $true )
& ( emptyset__Cong = $true )
& ( exu__Cong = $true )
& ( exuE3u = $true )
& ( in__Cong = $true )
& ( inCongP = $true )
& ( exuI2 = $true )
& ( exuI3 = $true )
& ( exuI1 = $true )
& ( notdallE = $true )
& ( notdexE = $true )
& ( prop2set2propI = $true )
& ( prop2setI = $true )
& ( quantDeMorgan4 = $true )
& ( quantDeMorgan3 = $true )
& ( quantDeMorgan2 = $true )
& ( quantDeMorgan1 = $true )
& ( vacuousDall = $true )
& ( emptyE1 = $true )
& ( upairsetIR = $true )
& ( upairsetIL = $true )
& ( upairsetE = $true )
& ( singletonsswitch = $true )
& ( eqinunit = $true )
& ( notinsingleton = $true )
& ( uniqinunit = $true )
& ( nonemptyImpWitness = $true )
& ( exuE2 = $true )
& ( subPowSU = $true )
& ( setunionE = $true )
& ( setunionI = $true )
& ( powersetE = $true )
& ( emptyInPowerset = $true )
& ( emptyinPowerset = $true )
& ( powersetI = $true )
& ( setoftrueEq = $true )
& ( setadjoinOr = $true )
& ( setadjoinE = $true )
& ( setadjoinIR = $true )
& ( emptyinunitempty = $true )
& ( setadjoinIL = $true )
& ( nonemptyI1 = $true )
& ( nonemptyI = $true )
& ( nonemptyE1 = $true )
& ( setbeta = $true )
& ( noeltsimpempty = $true )
& ( emptyI = $true )
& ( setext = $true )
& ( exuE3e = $true )
& ( notinemptyset = $true )
& ( emptysetimpfalse = $true )
& ( emptysetE = $true )
& ( prop2setE = $true )
& ( exuE1 = $true )
& ( dsetconstrER = $true )
& ( dsetconstrEL = $true )
& ( dsetconstrI = $true )
& ( descrp = $true )
& ( wellorderingAx = $true )
& ( foundationAx = $true )
& ( replAx = $true )
& ( omegaIndAx = $true )
& ( omegaSAx = $true )
& ( omega0Ax = $true )
& ( setunionAx = $true )
& ( powersetAx = $true )
& ( setadjoinAx = $true )
& ( emptysetAx = $true )
& ( setextAx = $true ) ),
inference(ennf_transformation,[],[f224]) ).
thf(f723,plain,
( ( uniqinunit = $true )
& ( symdiffI1 = $true )
& ( sepInPowerset = $true )
& ( noeltsimpempty = $true )
& ( binunionIR = $true )
& ( setukpairinjL2 = $true )
& ( exu__Cong = $true )
& ( setadjoinE = $true )
& ( binintersectI = $true )
& ( symdiffE = $true )
& ( emptyI = $true )
& ( dsetconstrI = $true )
& ( setunionAx = $true )
& ( subsetTrans = $true )
& ( nonemptyI1 = $true )
& ( powersetE = $true )
& ( binintersectLsub = $true )
& ( inCongP = $true )
& ( kpairiskpair = $true )
& ( upairsetIL = $true )
& ( symdiffI2 = $true )
& ( disjointsetsI1 = $true )
& ( setminusIRneg = $true )
& ( quantDeMorgan2 = $true )
& ( setadjoinAx = $true )
& ( descrp = $true )
& ( notequalI2 = $true )
& ( cartprodpairin = $true )
& ( emptysetimpfalse = $true )
& ( ex1E1 = $true )
& ( binintersectSubset5 = $true )
& ( setminusEL = $true )
& ( subPowSU = $true )
& ( powersetI = $true )
& ( powersetAx = $true )
& ( exuE1 = $true )
& ( binunionE = $true )
& ( setukpairIR = $true )
& ( subsetRefl = $true )
& ( singletonsubset = $true )
& ( binintersectEL = $true )
& ( powersetE1 = $true )
& ( singletonprop = $true )
& ( notequalI1 = $true )
& ( setukpairinjR1 = $true )
& ( replAx = $true )
& ( setextAx = $true )
& ( kfstpairEq = $true )
& ( setunionsingleton1 = $true )
& ( exuE2 = $true )
& ( subset2powerset = $true )
& ( powerset__Cong = $true )
& ( emptyE1 = $true )
& ( binunionLsub = $true )
& ( prop2setE = $true )
& ( upairset2IR = $true )
& ( exuEu = $true )
& ( emptyInPowerset = $true )
& ( quantDeMorgan4 = $true )
& ( setadjoinSub2 = $true )
& ( eqimpsubset2 = $true )
& ( subsetE2 = $true )
& ( exuI1 = $true )
& ( dsetconstr__Cong = $true )
& ( setminusER = $true )
& ( vacuousDall = $true )
& ( binunionEcases = $true )
& ( upairset2E = $true )
& ( setminusSubset2 = $true )
& ( emptyinPowerset = $true )
& ( subsetemptysetimpeq = $true )
& ( setunionsingleton2 = $true )
& ( singletonsuniq = $true )
& ( setoftrueEq = $true )
& ( eqimpsubset1 = $true )
& ( setbeta = $true )
& ( emptysetsubset = $true )
& ( singletoninpowerset = $true )
& ( kfstsingleton = $true )
& ( setukpairinjL = $true )
& ( setukpairinjL1 = $true )
& ( emptyset__Cong = $true )
& ( setadjoinIR = $true )
& ( setadjoinSub = $true )
& ( cartprodfstin = $true )
& ( cartprodmempair1 = $true )
& ( setunionE = $true )
& ( prop2setI = $true )
& ( symdiffIneg2 = $true )
& ( inPowerset = $true )
& ( omegaSAx = $true )
& ( exuE3e = $true )
& ( prop2set2propI = $true )
& ( binunionIL = $true )
& ( quantDeMorgan3 = $true )
& ( setadjoin__Cong = $true )
& ( binintersectSubset3 = $true )
& ( omegaIndAx = $true )
& ( setext = $true )
& ( symdiffIneg1 = $true )
& ( notdexE = $true )
& ( foundationAx = $true )
& ( ubforcartprodlem1 = $true )
& ( quantDeMorgan1 = $true )
& ( binintersectER = $true )
& ( bs114d = $true )
& ( upairsetIR = $true )
& ( subsetI2 = $true )
& ( nonemptyE1 = $true )
& ( exuI2 = $true )
& ( ex1I = $true )
& ( exuI3 = $true )
& ( setunion__Cong = $true )
& ( singletoninpowunion = $true )
& ( notinemptyset = $true )
& ( omega__Cong = $true )
& ( setunionE2 = $true )
& ( notsubsetI = $true )
& ? [X2: $i,X1: $i,X0: $i,X3: $i] :
( ( ( setadjoin @ ( setadjoin @ X1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X1 @ ( setadjoin @ X3 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ X0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ ( setadjoin @ X2 @ emptyset ) ) @ emptyset ) ) )
& ( X2 != X3 ) )
& ( setminusILneg = $true )
& ( setminusI = $true )
& ( ex1I2 = $true )
& ( setminusELneg = $true )
& ( ubforcartprodlem2 = $true )
& ( singletonsswitch = $true )
& ( sepSubset = $true )
& ( descr__Cong = $true )
& ( notdallE = $true )
& ( setadjoinIL = $true )
& ( setunionI = $true )
& ( dsetconstrEL = $true )
& ( setminusLsub = $true )
& ( setukpairinjR11 = $true )
& ( setextsub = $true )
& ( upairsubunion = $true )
& ( upairinpowunion = $true )
& ( notinsingleton = $true )
& ( setminusSubset1 = $true )
& ( upairsetE = $true )
& ( setadjoinOr = $true )
& ( powersetsubset = $true )
& ( emptysetAx = $true )
& ( emptyinunitempty = $true )
& ( setukpairinjR12 = $true )
& ( kpairp = $true )
& ( binintersectSubset4 = $true )
& ( subsetE = $true )
& ( setminusERneg = $true )
& ( binintersectRsub = $true )
& ( cartprodmempair = $true )
& ( eqinunit = $true )
& ( setukpairIL = $true )
& ( binintersectSubset2 = $true )
& ( emptysetE = $true )
& ( nonemptyImpWitness = $true )
& ( nonemptyI = $true )
& ( wellorderingAx = $true )
& ( ubforcartprodlem3 = $true )
& ( theprop = $true )
& ( binintersectSubset1 = $true )
& ( secondinupair = $true )
& ( setunionsingleton = $true )
& ( subsetI1 = $true )
& ( exuE3u = $true )
& ( binunionRsub = $true )
& ( dsetconstrER = $true )
& ( omega0Ax = $true )
& ( in__Cong = $true )
& ( powersetI1 = $true )
& ( upairequniteq = $true ) ),
inference(flattening,[],[f722]) ).
thf(f852,plain,
( ( ! [X2: $i,X1: $i,X0: $i] :
( ( X0 = X1 )
| ( ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) )
!= ( setadjoin @ X2 @ emptyset ) ) )
| ( upairequniteq != $true ) )
& ( ( upairequniteq = $true )
| ? [X2: $i,X1: $i,X0: $i] :
( ( X0 != X1 )
& ( ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) )
= ( setadjoin @ X2 @ emptyset ) ) ) ) ),
inference(nnf_transformation,[],[f568]) ).
thf(f853,plain,
( ( ! [X0: $i,X1: $i,X2: $i] :
( ( X1 = X2 )
| ( ( setadjoin @ X0 @ emptyset )
!= ( setadjoin @ X2 @ ( setadjoin @ X1 @ emptyset ) ) ) )
| ( upairequniteq != $true ) )
& ( ( upairequniteq = $true )
| ? [X3: $i,X4: $i,X5: $i] :
( ( X4 != X5 )
& ( ( setadjoin @ X3 @ emptyset )
= ( setadjoin @ X5 @ ( setadjoin @ X4 @ emptyset ) ) ) ) ) ),
inference(rectify,[],[f852]) ).
thf(f854,plain,
( ( ! [X0: $i,X1: $i,X2: $i] :
( ( X1 = X2 )
| ( ( setadjoin @ X0 @ emptyset )
!= ( setadjoin @ X2 @ ( setadjoin @ X1 @ emptyset ) ) ) )
| ( upairequniteq != $true ) )
& ( ( upairequniteq = $true )
| ( ( sK111 != sK112 )
& ( ( setadjoin @ sK110 @ emptyset )
= ( setadjoin @ sK112 @ ( setadjoin @ sK111 @ emptyset ) ) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK110,sK111,sK112]),skolemize(X3,sK110),skolemize(X4,sK111),skolemize(X5,sK112)],[f853]) ).
thf(f885,plain,
( ( ! [X0: $i,X1: $i,X2: $i] :
( ( ( in @ ( setadjoin @ X1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ ( setadjoin @ X2 @ emptyset ) ) @ emptyset ) ) )
!= $true )
| ( X0 = X1 ) )
| ( setukpairinjL1 != $true ) )
& ( ( setukpairinjL1 = $true )
| ? [X0: $i,X1: $i,X2: $i] :
( ( ( in @ ( setadjoin @ X1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ ( setadjoin @ X2 @ emptyset ) ) @ emptyset ) ) )
= $true )
& ( X0 != X1 ) ) ) ),
inference(nnf_transformation,[],[f688]) ).
thf(f886,plain,
( ( ! [X0: $i,X1: $i,X2: $i] :
( ( ( in @ ( setadjoin @ X1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ ( setadjoin @ X2 @ emptyset ) ) @ emptyset ) ) )
!= $true )
| ( X0 = X1 ) )
| ( setukpairinjL1 != $true ) )
& ( ( setukpairinjL1 = $true )
| ? [X3: $i,X4: $i,X5: $i] :
( ( ( in @ ( setadjoin @ X4 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X3 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X3 @ ( setadjoin @ X5 @ emptyset ) ) @ emptyset ) ) )
= $true )
& ( X3 != X4 ) ) ) ),
inference(rectify,[],[f885]) ).
thf(f887,plain,
( ( ! [X0: $i,X1: $i,X2: $i] :
( ( ( in @ ( setadjoin @ X1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ ( setadjoin @ X2 @ emptyset ) ) @ emptyset ) ) )
!= $true )
| ( X0 = X1 ) )
| ( setukpairinjL1 != $true ) )
& ( ( setukpairinjL1 = $true )
| ( ( $true
= ( in @ ( setadjoin @ sK147 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK146 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK146 @ ( setadjoin @ sK148 @ emptyset ) ) @ emptyset ) ) ) )
& ( sK147 != sK146 ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK146,sK147,sK148]),skolemize(X3,sK146),skolemize(X4,sK147),skolemize(X5,sK148)],[f886]) ).
thf(f977,plain,
( ( ! [X0: $i,X2: $i,X1: $i] :
( ( ( $true
= ( in @ X0 @ X2 ) )
| ( X0 = X1 )
| ( $true
!= ( in @ X0 @ ( setadjoin @ X1 @ X2 ) ) ) )
& ( ( $true
= ( in @ X0 @ ( setadjoin @ X1 @ X2 ) ) )
| ( ( $true
!= ( in @ X0 @ X2 ) )
& ( X0 != X1 ) ) ) )
| ( setadjoinAx != $true ) )
& ( ( setadjoinAx = $true )
| ? [X0: $i,X2: $i,X1: $i] :
( ( ( $true
!= ( in @ X0 @ ( setadjoin @ X1 @ X2 ) ) )
| ( ( $true
!= ( in @ X0 @ X2 ) )
& ( X0 != X1 ) ) )
& ( ( $true
= ( in @ X0 @ ( setadjoin @ X1 @ X2 ) ) )
| ( $true
= ( in @ X0 @ X2 ) )
| ( X0 = X1 ) ) ) ) ),
inference(nnf_transformation,[],[f188]) ).
thf(f978,plain,
( ( ! [X0: $i,X2: $i,X1: $i] :
( ( ( $true
= ( in @ X0 @ X2 ) )
| ( X0 = X1 )
| ( $true
!= ( in @ X0 @ ( setadjoin @ X1 @ X2 ) ) ) )
& ( ( $true
= ( in @ X0 @ ( setadjoin @ X1 @ X2 ) ) )
| ( ( $true
!= ( in @ X0 @ X2 ) )
& ( X0 != X1 ) ) ) )
| ( setadjoinAx != $true ) )
& ( ( setadjoinAx = $true )
| ? [X0: $i,X2: $i,X1: $i] :
( ( ( $true
!= ( in @ X0 @ ( setadjoin @ X1 @ X2 ) ) )
| ( ( $true
!= ( in @ X0 @ X2 ) )
& ( X0 != X1 ) ) )
& ( ( $true
= ( in @ X0 @ ( setadjoin @ X1 @ X2 ) ) )
| ( $true
= ( in @ X0 @ X2 ) )
| ( X0 = X1 ) ) ) ) ),
inference(flattening,[],[f977]) ).
thf(f979,plain,
( ( ! [X0: $i,X1: $i,X2: $i] :
( ( ( ( in @ X0 @ X1 )
= $true )
| ( X0 = X2 )
| ( $true
!= ( in @ X0 @ ( setadjoin @ X2 @ X1 ) ) ) )
& ( ( $true
= ( in @ X0 @ ( setadjoin @ X2 @ X1 ) ) )
| ( ( ( in @ X0 @ X1 )
!= $true )
& ( X0 != X2 ) ) ) )
| ( setadjoinAx != $true ) )
& ( ( setadjoinAx = $true )
| ? [X3: $i,X4: $i,X5: $i] :
( ( ( ( in @ X3 @ ( setadjoin @ X5 @ X4 ) )
!= $true )
| ( ( ( in @ X3 @ X4 )
!= $true )
& ( X3 != X5 ) ) )
& ( ( ( in @ X3 @ ( setadjoin @ X5 @ X4 ) )
= $true )
| ( ( in @ X3 @ X4 )
= $true )
| ( X3 = X5 ) ) ) ) ),
inference(rectify,[],[f978]) ).
thf(f980,plain,
( ( ! [X0: $i,X1: $i,X2: $i] :
( ( ( ( in @ X0 @ X1 )
= $true )
| ( X0 = X2 )
| ( $true
!= ( in @ X0 @ ( setadjoin @ X2 @ X1 ) ) ) )
& ( ( $true
= ( in @ X0 @ ( setadjoin @ X2 @ X1 ) ) )
| ( ( ( in @ X0 @ X1 )
!= $true )
& ( X0 != X2 ) ) ) )
| ( setadjoinAx != $true ) )
& ( ( setadjoinAx = $true )
| ( ( ( $true
!= ( in @ sK237 @ ( setadjoin @ sK239 @ sK238 ) ) )
| ( ( $true
!= ( in @ sK237 @ sK238 ) )
& ( sK239 != sK237 ) ) )
& ( ( $true
= ( in @ sK237 @ ( setadjoin @ sK239 @ sK238 ) ) )
| ( $true
= ( in @ sK237 @ sK238 ) )
| ( sK239 = sK237 ) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK237,sK238,sK239]),skolemize(X3,sK237),skolemize(X4,sK238),skolemize(X5,sK239)],[f979]) ).
thf(f1014,plain,
( ( ( setukpairinjR11 = $true )
| ? [X1: $i,X0: $i] :
( ( X0 = X1 )
& ( ( setadjoin @ X0 @ emptyset )
!= ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) ) ) ) )
& ( ! [X1: $i,X0: $i] :
( ( X0 != X1 )
| ( ( setadjoin @ X0 @ emptyset )
= ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) ) ) )
| ( setukpairinjR11 != $true ) ) ),
inference(nnf_transformation,[],[f614]) ).
thf(f1015,plain,
( ( ( setukpairinjR11 = $true )
| ? [X0: $i,X1: $i] :
( ( X0 = X1 )
& ( ( setadjoin @ X1 @ emptyset )
!= ( setadjoin @ X1 @ ( setadjoin @ X0 @ emptyset ) ) ) ) )
& ( ! [X2: $i,X3: $i] :
( ( X2 != X3 )
| ( ( setadjoin @ X3 @ emptyset )
= ( setadjoin @ X3 @ ( setadjoin @ X2 @ emptyset ) ) ) )
| ( setukpairinjR11 != $true ) ) ),
inference(rectify,[],[f1014]) ).
thf(f1016,plain,
( ( ( setukpairinjR11 = $true )
| ( ( sK264 = sK265 )
& ( ( setadjoin @ sK265 @ ( setadjoin @ sK264 @ emptyset ) )
!= ( setadjoin @ sK265 @ emptyset ) ) ) )
& ( ! [X2: $i,X3: $i] :
( ( X2 != X3 )
| ( ( setadjoin @ X3 @ emptyset )
= ( setadjoin @ X3 @ ( setadjoin @ X2 @ emptyset ) ) ) )
| ( setukpairinjR11 != $true ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK264,sK265]),skolemize(X0,sK264),skolemize(X1,sK265)],[f1015]) ).
thf(f1095,plain,
( ( ( upairset2E = $true )
| ? [X2: $i,X0: $i,X1: $i] :
( ( ( in @ X0 @ ( setadjoin @ X2 @ ( setadjoin @ X1 @ emptyset ) ) )
= $true )
& ( X0 != X1 )
& ( X0 != X2 ) ) )
& ( ! [X2: $i,X0: $i,X1: $i] :
( ( ( in @ X0 @ ( setadjoin @ X2 @ ( setadjoin @ X1 @ emptyset ) ) )
!= $true )
| ( X0 = X1 )
| ( X0 = X2 ) )
| ( upairset2E != $true ) ) ),
inference(nnf_transformation,[],[f591]) ).
thf(f1096,plain,
( ( ( upairset2E = $true )
| ? [X0: $i,X1: $i,X2: $i] :
( ( ( in @ X1 @ ( setadjoin @ X0 @ ( setadjoin @ X2 @ emptyset ) ) )
= $true )
& ( X1 != X2 )
& ( X0 != X1 ) ) )
& ( ! [X3: $i,X4: $i,X5: $i] :
( ( $true
!= ( in @ X4 @ ( setadjoin @ X3 @ ( setadjoin @ X5 @ emptyset ) ) ) )
| ( X4 = X5 )
| ( X3 = X4 ) )
| ( upairset2E != $true ) ) ),
inference(rectify,[],[f1095]) ).
thf(f1097,plain,
( ( ( upairset2E = $true )
| ( ( ( in @ sK340 @ ( setadjoin @ sK339 @ ( setadjoin @ sK341 @ emptyset ) ) )
= $true )
& ( sK341 != sK340 )
& ( sK340 != sK339 ) ) )
& ( ! [X3: $i,X4: $i,X5: $i] :
( ( $true
!= ( in @ X4 @ ( setadjoin @ X3 @ ( setadjoin @ X5 @ emptyset ) ) ) )
| ( X4 = X5 )
| ( X3 = X4 ) )
| ( upairset2E != $true ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK339,sK340,sK341]),skolemize(X0,sK339),skolemize(X1,sK340),skolemize(X2,sK341)],[f1096]) ).
thf(f1150,plain,
( ( ( secondinupair = $true )
| ? [X1: $i,X0: $i] :
( ( in @ X0 @ ( setadjoin @ X1 @ ( setadjoin @ X0 @ emptyset ) ) )
!= $true ) )
& ( ! [X1: $i,X0: $i] :
( ( in @ X0 @ ( setadjoin @ X1 @ ( setadjoin @ X0 @ emptyset ) ) )
= $true )
| ( secondinupair != $true ) ) ),
inference(nnf_transformation,[],[f407]) ).
thf(f1151,plain,
( ( ( secondinupair = $true )
| ? [X0: $i,X1: $i] :
( ( in @ X1 @ ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) ) )
!= $true ) )
& ( ! [X2: $i,X3: $i] :
( ( in @ X3 @ ( setadjoin @ X2 @ ( setadjoin @ X3 @ emptyset ) ) )
= $true )
| ( secondinupair != $true ) ) ),
inference(rectify,[],[f1150]) ).
thf(f1152,plain,
( ( ( secondinupair = $true )
| ( ( in @ sK390 @ ( setadjoin @ sK389 @ ( setadjoin @ sK390 @ emptyset ) ) )
!= $true ) )
& ( ! [X2: $i,X3: $i] :
( ( in @ X3 @ ( setadjoin @ X2 @ ( setadjoin @ X3 @ emptyset ) ) )
= $true )
| ( secondinupair != $true ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK389,sK390]),skolemize(X0,sK389),skolemize(X1,sK390)],[f1151]) ).
thf(f1192,plain,
( ( uniqinunit = $true )
& ( symdiffI1 = $true )
& ( sepInPowerset = $true )
& ( noeltsimpempty = $true )
& ( binunionIR = $true )
& ( setukpairinjL2 = $true )
& ( exu__Cong = $true )
& ( setadjoinE = $true )
& ( binintersectI = $true )
& ( symdiffE = $true )
& ( emptyI = $true )
& ( dsetconstrI = $true )
& ( setunionAx = $true )
& ( subsetTrans = $true )
& ( nonemptyI1 = $true )
& ( powersetE = $true )
& ( binintersectLsub = $true )
& ( inCongP = $true )
& ( kpairiskpair = $true )
& ( upairsetIL = $true )
& ( symdiffI2 = $true )
& ( disjointsetsI1 = $true )
& ( setminusIRneg = $true )
& ( quantDeMorgan2 = $true )
& ( setadjoinAx = $true )
& ( descrp = $true )
& ( notequalI2 = $true )
& ( cartprodpairin = $true )
& ( emptysetimpfalse = $true )
& ( ex1E1 = $true )
& ( binintersectSubset5 = $true )
& ( setminusEL = $true )
& ( subPowSU = $true )
& ( powersetI = $true )
& ( powersetAx = $true )
& ( exuE1 = $true )
& ( binunionE = $true )
& ( setukpairIR = $true )
& ( subsetRefl = $true )
& ( singletonsubset = $true )
& ( binintersectEL = $true )
& ( powersetE1 = $true )
& ( singletonprop = $true )
& ( notequalI1 = $true )
& ( setukpairinjR1 = $true )
& ( replAx = $true )
& ( setextAx = $true )
& ( kfstpairEq = $true )
& ( setunionsingleton1 = $true )
& ( exuE2 = $true )
& ( subset2powerset = $true )
& ( powerset__Cong = $true )
& ( emptyE1 = $true )
& ( binunionLsub = $true )
& ( prop2setE = $true )
& ( upairset2IR = $true )
& ( exuEu = $true )
& ( emptyInPowerset = $true )
& ( quantDeMorgan4 = $true )
& ( setadjoinSub2 = $true )
& ( eqimpsubset2 = $true )
& ( subsetE2 = $true )
& ( exuI1 = $true )
& ( dsetconstr__Cong = $true )
& ( setminusER = $true )
& ( vacuousDall = $true )
& ( binunionEcases = $true )
& ( upairset2E = $true )
& ( setminusSubset2 = $true )
& ( emptyinPowerset = $true )
& ( subsetemptysetimpeq = $true )
& ( setunionsingleton2 = $true )
& ( singletonsuniq = $true )
& ( setoftrueEq = $true )
& ( eqimpsubset1 = $true )
& ( setbeta = $true )
& ( emptysetsubset = $true )
& ( singletoninpowerset = $true )
& ( kfstsingleton = $true )
& ( setukpairinjL = $true )
& ( setukpairinjL1 = $true )
& ( emptyset__Cong = $true )
& ( setadjoinIR = $true )
& ( setadjoinSub = $true )
& ( cartprodfstin = $true )
& ( cartprodmempair1 = $true )
& ( setunionE = $true )
& ( prop2setI = $true )
& ( symdiffIneg2 = $true )
& ( inPowerset = $true )
& ( omegaSAx = $true )
& ( exuE3e = $true )
& ( prop2set2propI = $true )
& ( binunionIL = $true )
& ( quantDeMorgan3 = $true )
& ( setadjoin__Cong = $true )
& ( binintersectSubset3 = $true )
& ( omegaIndAx = $true )
& ( setext = $true )
& ( symdiffIneg1 = $true )
& ( notdexE = $true )
& ( foundationAx = $true )
& ( ubforcartprodlem1 = $true )
& ( quantDeMorgan1 = $true )
& ( binintersectER = $true )
& ( bs114d = $true )
& ( upairsetIR = $true )
& ( subsetI2 = $true )
& ( nonemptyE1 = $true )
& ( exuI2 = $true )
& ( ex1I = $true )
& ( exuI3 = $true )
& ( setunion__Cong = $true )
& ( singletoninpowunion = $true )
& ( notinemptyset = $true )
& ( omega__Cong = $true )
& ( setunionE2 = $true )
& ( notsubsetI = $true )
& ? [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( ( setadjoin @ ( setadjoin @ X1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X1 @ ( setadjoin @ X3 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ X2 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X2 @ ( setadjoin @ X0 @ emptyset ) ) @ emptyset ) ) )
& ( X0 != X3 ) )
& ( setminusILneg = $true )
& ( setminusI = $true )
& ( ex1I2 = $true )
& ( setminusELneg = $true )
& ( ubforcartprodlem2 = $true )
& ( singletonsswitch = $true )
& ( sepSubset = $true )
& ( descr__Cong = $true )
& ( notdallE = $true )
& ( setadjoinIL = $true )
& ( setunionI = $true )
& ( dsetconstrEL = $true )
& ( setminusLsub = $true )
& ( setukpairinjR11 = $true )
& ( setextsub = $true )
& ( upairsubunion = $true )
& ( upairinpowunion = $true )
& ( notinsingleton = $true )
& ( setminusSubset1 = $true )
& ( upairsetE = $true )
& ( setadjoinOr = $true )
& ( powersetsubset = $true )
& ( emptysetAx = $true )
& ( emptyinunitempty = $true )
& ( setukpairinjR12 = $true )
& ( kpairp = $true )
& ( binintersectSubset4 = $true )
& ( subsetE = $true )
& ( setminusERneg = $true )
& ( binintersectRsub = $true )
& ( cartprodmempair = $true )
& ( eqinunit = $true )
& ( setukpairIL = $true )
& ( binintersectSubset2 = $true )
& ( emptysetE = $true )
& ( nonemptyImpWitness = $true )
& ( nonemptyI = $true )
& ( wellorderingAx = $true )
& ( ubforcartprodlem3 = $true )
& ( theprop = $true )
& ( binintersectSubset1 = $true )
& ( secondinupair = $true )
& ( setunionsingleton = $true )
& ( subsetI1 = $true )
& ( exuE3u = $true )
& ( binunionRsub = $true )
& ( dsetconstrER = $true )
& ( omega0Ax = $true )
& ( in__Cong = $true )
& ( powersetI1 = $true )
& ( upairequniteq = $true ) ),
inference(rectify,[],[f723]) ).
thf(f1193,plain,
( ( uniqinunit = $true )
& ( symdiffI1 = $true )
& ( sepInPowerset = $true )
& ( noeltsimpempty = $true )
& ( binunionIR = $true )
& ( setukpairinjL2 = $true )
& ( exu__Cong = $true )
& ( setadjoinE = $true )
& ( binintersectI = $true )
& ( symdiffE = $true )
& ( emptyI = $true )
& ( dsetconstrI = $true )
& ( setunionAx = $true )
& ( subsetTrans = $true )
& ( nonemptyI1 = $true )
& ( powersetE = $true )
& ( binintersectLsub = $true )
& ( inCongP = $true )
& ( kpairiskpair = $true )
& ( upairsetIL = $true )
& ( symdiffI2 = $true )
& ( disjointsetsI1 = $true )
& ( setminusIRneg = $true )
& ( quantDeMorgan2 = $true )
& ( setadjoinAx = $true )
& ( descrp = $true )
& ( notequalI2 = $true )
& ( cartprodpairin = $true )
& ( emptysetimpfalse = $true )
& ( ex1E1 = $true )
& ( binintersectSubset5 = $true )
& ( setminusEL = $true )
& ( subPowSU = $true )
& ( powersetI = $true )
& ( powersetAx = $true )
& ( exuE1 = $true )
& ( binunionE = $true )
& ( setukpairIR = $true )
& ( subsetRefl = $true )
& ( singletonsubset = $true )
& ( binintersectEL = $true )
& ( powersetE1 = $true )
& ( singletonprop = $true )
& ( notequalI1 = $true )
& ( setukpairinjR1 = $true )
& ( replAx = $true )
& ( setextAx = $true )
& ( kfstpairEq = $true )
& ( setunionsingleton1 = $true )
& ( exuE2 = $true )
& ( subset2powerset = $true )
& ( powerset__Cong = $true )
& ( emptyE1 = $true )
& ( binunionLsub = $true )
& ( prop2setE = $true )
& ( upairset2IR = $true )
& ( exuEu = $true )
& ( emptyInPowerset = $true )
& ( quantDeMorgan4 = $true )
& ( setadjoinSub2 = $true )
& ( eqimpsubset2 = $true )
& ( subsetE2 = $true )
& ( exuI1 = $true )
& ( dsetconstr__Cong = $true )
& ( setminusER = $true )
& ( vacuousDall = $true )
& ( binunionEcases = $true )
& ( upairset2E = $true )
& ( setminusSubset2 = $true )
& ( emptyinPowerset = $true )
& ( subsetemptysetimpeq = $true )
& ( setunionsingleton2 = $true )
& ( singletonsuniq = $true )
& ( setoftrueEq = $true )
& ( eqimpsubset1 = $true )
& ( setbeta = $true )
& ( emptysetsubset = $true )
& ( singletoninpowerset = $true )
& ( kfstsingleton = $true )
& ( setukpairinjL = $true )
& ( setukpairinjL1 = $true )
& ( emptyset__Cong = $true )
& ( setadjoinIR = $true )
& ( setadjoinSub = $true )
& ( cartprodfstin = $true )
& ( cartprodmempair1 = $true )
& ( setunionE = $true )
& ( prop2setI = $true )
& ( symdiffIneg2 = $true )
& ( inPowerset = $true )
& ( omegaSAx = $true )
& ( exuE3e = $true )
& ( prop2set2propI = $true )
& ( binunionIL = $true )
& ( quantDeMorgan3 = $true )
& ( setadjoin__Cong = $true )
& ( binintersectSubset3 = $true )
& ( omegaIndAx = $true )
& ( setext = $true )
& ( symdiffIneg1 = $true )
& ( notdexE = $true )
& ( foundationAx = $true )
& ( ubforcartprodlem1 = $true )
& ( quantDeMorgan1 = $true )
& ( binintersectER = $true )
& ( bs114d = $true )
& ( upairsetIR = $true )
& ( subsetI2 = $true )
& ( nonemptyE1 = $true )
& ( exuI2 = $true )
& ( ex1I = $true )
& ( exuI3 = $true )
& ( setunion__Cong = $true )
& ( singletoninpowunion = $true )
& ( notinemptyset = $true )
& ( omega__Cong = $true )
& ( setunionE2 = $true )
& ( notsubsetI = $true )
& ( ( setadjoin @ ( setadjoin @ sK425 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK425 @ ( setadjoin @ sK423 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ sK424 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) ) @ emptyset ) ) )
& ( sK423 != sK426 )
& ( setminusILneg = $true )
& ( setminusI = $true )
& ( ex1I2 = $true )
& ( setminusELneg = $true )
& ( ubforcartprodlem2 = $true )
& ( singletonsswitch = $true )
& ( sepSubset = $true )
& ( descr__Cong = $true )
& ( notdallE = $true )
& ( setadjoinIL = $true )
& ( setunionI = $true )
& ( dsetconstrEL = $true )
& ( setminusLsub = $true )
& ( setukpairinjR11 = $true )
& ( setextsub = $true )
& ( upairsubunion = $true )
& ( upairinpowunion = $true )
& ( notinsingleton = $true )
& ( setminusSubset1 = $true )
& ( upairsetE = $true )
& ( setadjoinOr = $true )
& ( powersetsubset = $true )
& ( emptysetAx = $true )
& ( emptyinunitempty = $true )
& ( setukpairinjR12 = $true )
& ( kpairp = $true )
& ( binintersectSubset4 = $true )
& ( subsetE = $true )
& ( setminusERneg = $true )
& ( binintersectRsub = $true )
& ( cartprodmempair = $true )
& ( eqinunit = $true )
& ( setukpairIL = $true )
& ( binintersectSubset2 = $true )
& ( emptysetE = $true )
& ( nonemptyImpWitness = $true )
& ( nonemptyI = $true )
& ( wellorderingAx = $true )
& ( ubforcartprodlem3 = $true )
& ( theprop = $true )
& ( binintersectSubset1 = $true )
& ( secondinupair = $true )
& ( setunionsingleton = $true )
& ( subsetI1 = $true )
& ( exuE3u = $true )
& ( binunionRsub = $true )
& ( dsetconstrER = $true )
& ( omega0Ax = $true )
& ( in__Cong = $true )
& ( powersetI1 = $true )
& ( upairequniteq = $true ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK423,sK424,sK425,sK426]),skolemize(X0,sK423),skolemize(X1,sK424),skolemize(X2,sK425),skolemize(X3,sK426)],[f1192]) ).
thf(f1227,plain,
( ( ( uniqinunit = $true )
| ? [X0: $i,X1: $i] :
( ( X0 != X1 )
& ( ( in @ X1 @ ( setadjoin @ X0 @ emptyset ) )
= $true ) ) )
& ( ! [X0: $i,X1: $i] :
( ( X0 = X1 )
| ( ( in @ X1 @ ( setadjoin @ X0 @ emptyset ) )
!= $true ) )
| ( uniqinunit != $true ) ) ),
inference(nnf_transformation,[],[f602]) ).
thf(f1228,plain,
( ( ( uniqinunit = $true )
| ? [X0: $i,X1: $i] :
( ( X0 != X1 )
& ( ( in @ X1 @ ( setadjoin @ X0 @ emptyset ) )
= $true ) ) )
& ( ! [X2: $i,X3: $i] :
( ( X2 = X3 )
| ( ( in @ X3 @ ( setadjoin @ X2 @ emptyset ) )
!= $true ) )
| ( uniqinunit != $true ) ) ),
inference(rectify,[],[f1227]) ).
thf(f1229,plain,
( ( ( uniqinunit = $true )
| ( ( sK461 != sK460 )
& ( ( in @ sK461 @ ( setadjoin @ sK460 @ emptyset ) )
= $true ) ) )
& ( ! [X2: $i,X3: $i] :
( ( X2 = X3 )
| ( ( in @ X3 @ ( setadjoin @ X2 @ emptyset ) )
!= $true ) )
| ( uniqinunit != $true ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK460,sK461]),skolemize(X0,sK460),skolemize(X1,sK461)],[f1228]) ).
thf(f1385,plain,
! [X2: $i,X0: $i,X1: $i] :
( ( upairequniteq != $true )
| ( X1 = X2 )
| ( ( setadjoin @ X0 @ emptyset )
!= ( setadjoin @ X2 @ ( setadjoin @ X1 @ emptyset ) ) ) ),
inference(cnf_transformation,[],[f854]) ).
thf(f1428,plain,
! [X2: $i,X0: $i,X1: $i] :
( ( setukpairinjL1 != $true )
| ( ( in @ ( setadjoin @ X1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ ( setadjoin @ X2 @ emptyset ) ) @ emptyset ) ) )
!= $true )
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f887]) ).
thf(f1584,plain,
! [X2: $i,X0: $i,X1: $i] :
( ( $true
= ( in @ X0 @ ( setadjoin @ X2 @ X1 ) ) )
| ( X0 != X2 )
| ( setadjoinAx != $true ) ),
inference(cnf_transformation,[],[f980]) ).
thf(f1586,plain,
! [X2: $i,X0: $i,X1: $i] :
( ( $true
!= ( in @ X0 @ ( setadjoin @ X2 @ X1 ) ) )
| ( setadjoinAx != $true )
| ( ( in @ X0 @ X1 )
= $true )
| ( X0 = X2 ) ),
inference(cnf_transformation,[],[f980]) ).
thf(f1619,plain,
! [X2: $i,X3: $i] :
( ( X2 != X3 )
| ( ( setadjoin @ X3 @ emptyset )
= ( setadjoin @ X3 @ ( setadjoin @ X2 @ emptyset ) ) )
| ( setukpairinjR11 != $true ) ),
inference(cnf_transformation,[],[f1016]) ).
thf(f1719,plain,
! [X3: $i,X4: $i,X5: $i] :
( ( X4 = X5 )
| ( upairset2E != $true )
| ( $true
!= ( in @ X4 @ ( setadjoin @ X3 @ ( setadjoin @ X5 @ emptyset ) ) ) )
| ( X3 = X4 ) ),
inference(cnf_transformation,[],[f1097]) ).
thf(f1788,plain,
! [X2: $i,X3: $i] :
( ( secondinupair != $true )
| ( ( in @ X3 @ ( setadjoin @ X2 @ ( setadjoin @ X3 @ emptyset ) ) )
= $true ) ),
inference(cnf_transformation,[],[f1152]) ).
thf(f1836,plain,
upairequniteq = $true,
inference(cnf_transformation,[],[f1193]) ).
thf(f1845,plain,
secondinupair = $true,
inference(cnf_transformation,[],[f1193]) ).
thf(f1873,plain,
setukpairinjR11 = $true,
inference(cnf_transformation,[],[f1193]) ).
thf(f1887,plain,
sK423 != sK426,
inference(cnf_transformation,[],[f1193]) ).
thf(f1888,plain,
( ( setadjoin @ ( setadjoin @ sK425 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK425 @ ( setadjoin @ sK423 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ sK424 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) ) @ emptyset ) ) ),
inference(cnf_transformation,[],[f1193]) ).
thf(f1926,plain,
setukpairinjL1 = $true,
inference(cnf_transformation,[],[f1193]) ).
thf(f1939,plain,
upairset2E = $true,
inference(cnf_transformation,[],[f1193]) ).
thf(f1982,plain,
setadjoinAx = $true,
inference(cnf_transformation,[],[f1193]) ).
thf(f2006,plain,
uniqinunit = $true,
inference(cnf_transformation,[],[f1193]) ).
thf(f2054,plain,
! [X2: $i,X3: $i] :
( ( ( in @ X3 @ ( setadjoin @ X2 @ emptyset ) )
!= $true )
| ( uniqinunit != $true )
| ( X2 = X3 ) ),
inference(cnf_transformation,[],[f1229]) ).
thf(f2096,plain,
! [X2: $i,X1: $i] :
( ( setadjoinAx != $true )
| ( ( in @ X2 @ ( setadjoin @ X2 @ X1 ) )
= $true ) ),
inference(equality_resolution,[],[f1584]) ).
thf(f2097,plain,
! [X3: $i] :
( ( setukpairinjR11 != $true )
| ( ( setadjoin @ X3 @ emptyset )
= ( setadjoin @ X3 @ ( setadjoin @ X3 @ emptyset ) ) ) ),
inference(equality_resolution,[],[f1619]) ).
thf(f2264,definition,
( spl470_5
<=> ! [X2: $i,X0: $i,X1: $i] :
( ( ( in @ ( setadjoin @ X1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ ( setadjoin @ X2 @ emptyset ) ) @ emptyset ) ) )
!= $true )
| ( X0 = X1 ) ) ),
introduced(definition,[new_symbols(definition,[spl470_5])],[avatar_definition]) ).
thf(f2265,plain,
( ! [X2: $i,X0: $i,X1: $i] :
( ( ( in @ ( setadjoin @ X1 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ emptyset ) @ ( setadjoin @ ( setadjoin @ X0 @ ( setadjoin @ X2 @ emptyset ) ) @ emptyset ) ) )
!= $true )
| ( X0 = X1 ) )
| ~ spl470_5 ),
inference(avatar_component_clause,[],[f2264]) ).
thf(f2267,definition,
( spl470_6
<=> ( setukpairinjL1 = $true ) ),
introduced(definition,[new_symbols(definition,[spl470_6])],[avatar_definition]) ).
thf(f2270,plain,
( spl470_5
| ~ spl470_6 ),
inference(avatar_split_clause,[],[f1428,f2267,f2264]) ).
thf(f2318,definition,
( spl470_18
<=> ! [X2: $i,X3: $i] :
( ( X2 = X3 )
| ( ( in @ X2 @ ( setadjoin @ X3 @ emptyset ) )
!= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl470_18])],[avatar_definition]) ).
thf(f2319,plain,
( ! [X2: $i,X3: $i] :
( ( ( in @ X2 @ ( setadjoin @ X3 @ emptyset ) )
!= $true )
| ( X2 = X3 ) )
| ~ spl470_18 ),
inference(avatar_component_clause,[],[f2318]) ).
thf(f2514,definition,
( spl470_63
<=> ! [X0: $i,X1: $i] :
( ( in @ X0 @ ( setadjoin @ X0 @ X1 ) )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl470_63])],[avatar_definition]) ).
thf(f2515,plain,
( ! [X0: $i,X1: $i] :
( ( in @ X0 @ ( setadjoin @ X0 @ X1 ) )
= $true )
| ~ spl470_63 ),
inference(avatar_component_clause,[],[f2514]) ).
thf(f2594,definition,
( spl470_81
<=> ( setukpairinjR11 = $true ) ),
introduced(definition,[new_symbols(definition,[spl470_81])],[avatar_definition]) ).
thf(f2598,definition,
( spl470_82
<=> ! [X3: $i] :
( ( setadjoin @ X3 @ emptyset )
= ( setadjoin @ X3 @ ( setadjoin @ X3 @ emptyset ) ) ) ),
introduced(definition,[new_symbols(definition,[spl470_82])],[avatar_definition]) ).
thf(f2599,plain,
( ! [X3: $i] :
( ( setadjoin @ X3 @ emptyset )
= ( setadjoin @ X3 @ ( setadjoin @ X3 @ emptyset ) ) )
| ~ spl470_82 ),
inference(avatar_component_clause,[],[f2598]) ).
thf(f2600,plain,
( ~ spl470_81
| spl470_82 ),
inference(avatar_split_clause,[],[f2097,f2598,f2594]) ).
thf(f2606,definition,
( spl470_84
<=> ! [X4: $i,X5: $i,X3: $i] :
( ( ( in @ X5 @ ( setadjoin @ X4 @ X3 ) )
!= $true )
| ( X4 = X5 )
| ( ( in @ X5 @ X3 )
= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl470_84])],[avatar_definition]) ).
thf(f2607,plain,
( ! [X3: $i,X4: $i,X5: $i] :
( ( ( in @ X5 @ ( setadjoin @ X4 @ X3 ) )
!= $true )
| ( ( in @ X5 @ X3 )
= $true )
| ( X4 = X5 ) )
| ~ spl470_84 ),
inference(avatar_component_clause,[],[f2606]) ).
thf(f2885,definition,
( spl470_147
<=> ( setadjoinAx = $true ) ),
introduced(definition,[new_symbols(definition,[spl470_147])],[avatar_definition]) ).
thf(f2946,definition,
( spl470_161
<=> ( upairequniteq = $true ) ),
introduced(definition,[new_symbols(definition,[spl470_161])],[avatar_definition]) ).
thf(f2950,definition,
( spl470_162
<=> ! [X2: $i,X0: $i,X1: $i] :
( ( X1 = X2 )
| ( ( setadjoin @ X0 @ emptyset )
!= ( setadjoin @ X2 @ ( setadjoin @ X1 @ emptyset ) ) ) ) ),
introduced(definition,[new_symbols(definition,[spl470_162])],[avatar_definition]) ).
thf(f2951,plain,
( ! [X2: $i,X0: $i,X1: $i] :
( ( ( setadjoin @ X0 @ emptyset )
!= ( setadjoin @ X2 @ ( setadjoin @ X1 @ emptyset ) ) )
| ( X1 = X2 ) )
| ~ spl470_162 ),
inference(avatar_component_clause,[],[f2950]) ).
thf(f2952,plain,
( ~ spl470_161
| spl470_162 ),
inference(avatar_split_clause,[],[f1385,f2950,f2946]) ).
thf(f3024,definition,
( spl470_179
<=> ( upairset2E = $true ) ),
introduced(definition,[new_symbols(definition,[spl470_179])],[avatar_definition]) ).
thf(f3209,plain,
spl470_6,
inference(avatar_split_clause,[],[f1926,f2267]) ).
thf(f3286,definition,
( spl470_236
<=> ( secondinupair = $true ) ),
introduced(definition,[new_symbols(definition,[spl470_236])],[avatar_definition]) ).
thf(f3562,definition,
( spl470_295
<=> ! [X4: $i,X5: $i,X3: $i] :
( ( X4 = X5 )
| ( X3 = X5 )
| ( ( in @ X5 @ ( setadjoin @ X4 @ ( setadjoin @ X3 @ emptyset ) ) )
!= $true ) ) ),
introduced(definition,[new_symbols(definition,[spl470_295])],[avatar_definition]) ).
thf(f3563,plain,
( ! [X3: $i,X4: $i,X5: $i] :
( ( ( in @ X5 @ ( setadjoin @ X4 @ ( setadjoin @ X3 @ emptyset ) ) )
!= $true )
| ( X4 = X5 )
| ( X3 = X5 ) )
| ~ spl470_295 ),
inference(avatar_component_clause,[],[f3562]) ).
thf(f3626,plain,
( spl470_295
| ~ spl470_179 ),
inference(avatar_split_clause,[],[f1719,f3024,f3562]) ).
thf(f3660,definition,
( spl470_317
<=> ( uniqinunit = $true ) ),
introduced(definition,[new_symbols(definition,[spl470_317])],[avatar_definition]) ).
thf(f3663,plain,
( ~ spl470_317
| spl470_18 ),
inference(avatar_split_clause,[],[f2054,f2318,f3660]) ).
thf(f3721,plain,
spl470_81,
inference(avatar_split_clause,[],[f1873,f2594]) ).
thf(f3924,plain,
spl470_317,
inference(avatar_split_clause,[],[f2006,f3660]) ).
thf(f4077,plain,
( ~ spl470_147
| spl470_63 ),
inference(avatar_split_clause,[],[f2096,f2514,f2885]) ).
thf(f4310,definition,
( spl470_456
<=> ( ( setadjoin @ ( setadjoin @ sK425 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK425 @ ( setadjoin @ sK423 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ sK424 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) ) @ emptyset ) ) ) ),
introduced(definition,[new_symbols(definition,[spl470_456])],[avatar_definition]) ).
thf(f4312,plain,
( ( ( setadjoin @ ( setadjoin @ sK425 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK425 @ ( setadjoin @ sK423 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ sK424 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) ) @ emptyset ) ) )
| ~ spl470_456 ),
inference(avatar_component_clause,[],[f4310]) ).
thf(f4313,plain,
spl470_456,
inference(avatar_split_clause,[],[f1888,f4310]) ).
thf(f4416,definition,
( spl470_477
<=> ! [X0: $i,X1: $i] :
( ( in @ X1 @ ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) ) )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl470_477])],[avatar_definition]) ).
thf(f4417,plain,
( ! [X0: $i,X1: $i] :
( ( in @ X1 @ ( setadjoin @ X0 @ ( setadjoin @ X1 @ emptyset ) ) )
= $true )
| ~ spl470_477 ),
inference(avatar_component_clause,[],[f4416]) ).
thf(f4547,plain,
spl470_236,
inference(avatar_split_clause,[],[f1845,f3286]) ).
thf(f4802,definition,
( spl470_557
<=> ( sK423 = sK426 ) ),
introduced(definition,[new_symbols(definition,[spl470_557])],[avatar_definition]) ).
thf(f4804,plain,
( ( sK423 != sK426 )
| spl470_557 ),
inference(avatar_component_clause,[],[f4802]) ).
thf(f4805,plain,
~ spl470_557,
inference(avatar_split_clause,[],[f1887,f4802]) ).
thf(f5015,plain,
spl470_161,
inference(avatar_split_clause,[],[f1836,f2946]) ).
thf(f5118,plain,
( ~ spl470_147
| spl470_84 ),
inference(avatar_split_clause,[],[f1586,f2606,f2885]) ).
thf(f5461,plain,
spl470_179,
inference(avatar_split_clause,[],[f1939,f3024]) ).
thf(f5598,plain,
( ~ spl470_236
| spl470_477 ),
inference(avatar_split_clause,[],[f1788,f4416,f3286]) ).
thf(f5736,plain,
spl470_147,
inference(avatar_split_clause,[],[f1982,f2885]) ).
thf(f6127,plain,
( ( ( in @ ( setadjoin @ sK425 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK424 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) ) @ emptyset ) ) )
= $true )
| ~ spl470_63
| ~ spl470_456 ),
inference(superposition,[],[f2515,f4312]) ).
thf(f6131,definition,
( spl470_787
<=> ( ( in @ ( setadjoin @ sK425 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK424 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) ) @ emptyset ) ) )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl470_787])],[avatar_definition]) ).
thf(f6133,plain,
( ( ( in @ ( setadjoin @ sK425 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK424 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) ) @ emptyset ) ) )
= $true )
| ~ spl470_787 ),
inference(avatar_component_clause,[],[f6131]) ).
thf(f6134,plain,
( spl470_787
| ~ spl470_63
| ~ spl470_456 ),
inference(avatar_split_clause,[],[f6127,f4310,f2514,f6131]) ).
thf(f6329,plain,
( ( ( in @ ( setadjoin @ sK425 @ ( setadjoin @ sK423 @ emptyset ) ) @ ( setadjoin @ ( setadjoin @ sK424 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) ) @ emptyset ) ) )
= $true )
| ~ spl470_456
| ~ spl470_477 ),
inference(superposition,[],[f4417,f4312]) ).
thf(f6334,definition,
( spl470_794
<=> ( ( in @ ( setadjoin @ sK425 @ ( setadjoin @ sK423 @ emptyset ) ) @ ( setadjoin @ ( setadjoin @ sK424 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) ) @ emptyset ) ) )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl470_794])],[avatar_definition]) ).
thf(f6336,plain,
( ( ( in @ ( setadjoin @ sK425 @ ( setadjoin @ sK423 @ emptyset ) ) @ ( setadjoin @ ( setadjoin @ sK424 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) ) @ emptyset ) ) )
= $true )
| ~ spl470_794 ),
inference(avatar_component_clause,[],[f6334]) ).
thf(f6337,plain,
( spl470_794
| ~ spl470_456
| ~ spl470_477 ),
inference(avatar_split_clause,[],[f6329,f4416,f4310,f6334]) ).
thf(f6477,plain,
( ! [X0: $i] :
( ( ( setadjoin @ sK425 @ ( setadjoin @ sK423 @ emptyset ) )
= ( setadjoin @ sK425 @ emptyset ) )
| ( ( setadjoin @ X0 @ emptyset )
!= ( setadjoin @ ( setadjoin @ sK424 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) ) @ emptyset ) ) ) )
| ~ spl470_162
| ~ spl470_456 ),
inference(superposition,[],[f2951,f4312]) ).
thf(f6479,definition,
( spl470_804
<=> ! [X0: $i] :
( ( setadjoin @ X0 @ emptyset )
!= ( setadjoin @ ( setadjoin @ sK424 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) ) @ emptyset ) ) ) ),
introduced(definition,[new_symbols(definition,[spl470_804])],[avatar_definition]) ).
thf(f6480,plain,
( ! [X0: $i] :
( ( setadjoin @ X0 @ emptyset )
!= ( setadjoin @ ( setadjoin @ sK424 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) ) @ emptyset ) ) )
| ~ spl470_804 ),
inference(avatar_component_clause,[],[f6479]) ).
thf(f6482,definition,
( spl470_805
<=> ( ( setadjoin @ sK425 @ ( setadjoin @ sK423 @ emptyset ) )
= ( setadjoin @ sK425 @ emptyset ) ) ),
introduced(definition,[new_symbols(definition,[spl470_805])],[avatar_definition]) ).
thf(f6483,plain,
( ( ( setadjoin @ sK425 @ ( setadjoin @ sK423 @ emptyset ) )
!= ( setadjoin @ sK425 @ emptyset ) )
| spl470_805 ),
inference(avatar_component_clause,[],[f6482]) ).
thf(f6484,plain,
( ( ( setadjoin @ sK425 @ ( setadjoin @ sK423 @ emptyset ) )
= ( setadjoin @ sK425 @ emptyset ) )
| ~ spl470_805 ),
inference(avatar_component_clause,[],[f6482]) ).
thf(f6485,plain,
( spl470_804
| spl470_805
| ~ spl470_162
| ~ spl470_456 ),
inference(avatar_split_clause,[],[f6477,f4310,f2950,f6482,f6479]) ).
thf(f6787,plain,
( ! [X0: $i] :
( ( ( in @ X0 @ ( setadjoin @ ( setadjoin @ sK425 @ ( setadjoin @ sK423 @ emptyset ) ) @ emptyset ) )
= $true )
| ( ( in @ X0 @ ( setadjoin @ ( setadjoin @ sK424 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) ) @ emptyset ) ) )
!= $true )
| ( ( setadjoin @ sK425 @ emptyset )
= X0 ) )
| ~ spl470_84
| ~ spl470_456 ),
inference(superposition,[],[f2607,f4312]) ).
thf(f6828,definition,
( spl470_817
<=> ( ( setadjoin @ sK425 @ ( setadjoin @ sK423 @ emptyset ) )
= ( setadjoin @ sK424 @ emptyset ) ) ),
introduced(definition,[new_symbols(definition,[spl470_817])],[avatar_definition]) ).
thf(f6830,plain,
( ( ( setadjoin @ sK425 @ ( setadjoin @ sK423 @ emptyset ) )
= ( setadjoin @ sK424 @ emptyset ) )
| ~ spl470_817 ),
inference(avatar_component_clause,[],[f6828]) ).
thf(f6909,definition,
( spl470_819
<=> ( ( in @ sK423 @ ( setadjoin @ sK424 @ emptyset ) )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl470_819])],[avatar_definition]) ).
thf(f6911,plain,
( ( ( in @ sK423 @ ( setadjoin @ sK424 @ emptyset ) )
= $true )
| ~ spl470_819 ),
inference(avatar_component_clause,[],[f6909]) ).
thf(f6914,definition,
( spl470_820
<=> ( sK425 = sK423 ) ),
introduced(definition,[new_symbols(definition,[spl470_820])],[avatar_definition]) ).
thf(f6915,plain,
( ( sK425 != sK423 )
| spl470_820 ),
inference(avatar_component_clause,[],[f6914]) ).
thf(f6916,plain,
( ( sK425 = sK423 )
| ~ spl470_820 ),
inference(avatar_component_clause,[],[f6914]) ).
thf(f6951,plain,
( ( ( setadjoin @ sK425 @ ( setadjoin @ sK423 @ emptyset ) )
= ( setadjoin @ sK424 @ emptyset ) )
| ( ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) )
= ( setadjoin @ sK425 @ ( setadjoin @ sK423 @ emptyset ) ) )
| ( $true != $true )
| ~ spl470_295
| ~ spl470_794 ),
inference(superposition,[],[f3563,f6336]) ).
thf(f6966,plain,
( ( ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) )
= ( setadjoin @ sK425 @ ( setadjoin @ sK423 @ emptyset ) ) )
| ( ( setadjoin @ sK425 @ ( setadjoin @ sK423 @ emptyset ) )
= ( setadjoin @ sK424 @ emptyset ) )
| ~ spl470_295
| ~ spl470_794 ),
inference(trivial_inequality_removal,[],[f6951]) ).
thf(f6985,definition,
( spl470_828
<=> ( ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) )
= ( setadjoin @ sK425 @ ( setadjoin @ sK423 @ emptyset ) ) ) ),
introduced(definition,[new_symbols(definition,[spl470_828])],[avatar_definition]) ).
thf(f6987,plain,
( ( ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) )
= ( setadjoin @ sK425 @ ( setadjoin @ sK423 @ emptyset ) ) )
| ~ spl470_828 ),
inference(avatar_component_clause,[],[f6985]) ).
thf(f6988,plain,
( spl470_817
| spl470_828
| ~ spl470_295
| ~ spl470_794 ),
inference(avatar_split_clause,[],[f6966,f6334,f3562,f6985,f6828]) ).
thf(f7194,plain,
( ( ( setadjoin @ ( setadjoin @ sK423 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK423 @ ( setadjoin @ sK423 @ emptyset ) ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ sK424 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) ) @ emptyset ) ) )
| ~ spl470_456
| ~ spl470_820 ),
inference(superposition,[],[f4312,f6916]) ).
thf(f7202,plain,
( ( ( setadjoin @ ( setadjoin @ sK423 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK423 @ emptyset ) @ emptyset ) )
= ( setadjoin @ ( setadjoin @ sK424 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) ) @ emptyset ) ) )
| ~ spl470_82
| ~ spl470_456
| ~ spl470_820 ),
inference(forward_demodulation,[],[f7194,f2599]) ).
thf(f7210,plain,
( ( ( setadjoin @ ( setadjoin @ sK423 @ emptyset ) @ emptyset )
= ( setadjoin @ ( setadjoin @ sK424 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) ) @ emptyset ) ) )
| ~ spl470_82
| ~ spl470_456
| ~ spl470_820 ),
inference(forward_demodulation,[],[f7202,f2599]) ).
thf(f7216,plain,
( $false
| ~ spl470_82
| ~ spl470_456
| ~ spl470_804
| ~ spl470_820 ),
inference(forward_subsumption_resolution,[],[f7210,f6480]) ).
thf(f7217,plain,
( ~ spl470_82
| ~ spl470_456
| ~ spl470_804
| ~ spl470_820 ),
inference(avatar_contradiction_clause,[],[f7216]) ).
thf(f7250,definition,
( spl470_837
<=> ( sK425 = sK424 ) ),
introduced(definition,[new_symbols(definition,[spl470_837])],[avatar_definition]) ).
thf(f7252,plain,
( ( sK425 = sK424 )
| ~ spl470_837 ),
inference(avatar_component_clause,[],[f7250]) ).
thf(f7439,plain,
( ( $true != $true )
| ( sK424 = sK423 )
| ~ spl470_18
| ~ spl470_819 ),
inference(superposition,[],[f2319,f6911]) ).
thf(f7443,plain,
( ( sK424 = sK423 )
| ~ spl470_18
| ~ spl470_819 ),
inference(trivial_inequality_removal,[],[f7439]) ).
thf(f7448,definition,
( spl470_840
<=> ( sK424 = sK423 ) ),
introduced(definition,[new_symbols(definition,[spl470_840])],[avatar_definition]) ).
thf(f7450,plain,
( ( sK424 = sK423 )
| ~ spl470_840 ),
inference(avatar_component_clause,[],[f7448]) ).
thf(f7451,plain,
( spl470_840
| ~ spl470_18
| ~ spl470_819 ),
inference(avatar_split_clause,[],[f7443,f6909,f2318,f7448]) ).
thf(f8126,plain,
( ( sK424 != sK423 )
| spl470_820
| ~ spl470_837 ),
inference(superposition,[],[f6915,f7252]) ).
thf(f8147,plain,
( ~ spl470_840
| spl470_820
| ~ spl470_837 ),
inference(avatar_split_clause,[],[f8126,f7250,f6914,f7448]) ).
thf(f8665,plain,
( ( sK425 = sK424 )
| ( $true != $true )
| ~ spl470_5
| ~ spl470_787 ),
inference(superposition,[],[f2265,f6133]) ).
thf(f8671,plain,
( ( sK425 = sK424 )
| ~ spl470_5
| ~ spl470_787 ),
inference(trivial_inequality_removal,[],[f8665]) ).
thf(f8680,plain,
( spl470_837
| ~ spl470_5
| ~ spl470_787 ),
inference(avatar_split_clause,[],[f8671,f6131,f2264,f7250]) ).
thf(f9203,definition,
( spl470_886
<=> ( ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) )
= ( setadjoin @ sK424 @ emptyset ) ) ),
introduced(definition,[new_symbols(definition,[spl470_886])],[avatar_definition]) ).
thf(f9205,plain,
( ( ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) )
= ( setadjoin @ sK424 @ emptyset ) )
| ~ spl470_886 ),
inference(avatar_component_clause,[],[f9203]) ).
thf(f9207,definition,
( spl470_887
<=> ( ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) )
= ( setadjoin @ sK424 @ ( setadjoin @ sK423 @ emptyset ) ) ) ),
introduced(definition,[new_symbols(definition,[spl470_887])],[avatar_definition]) ).
thf(f9209,plain,
( ( ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) )
= ( setadjoin @ sK424 @ ( setadjoin @ sK423 @ emptyset ) ) )
| ~ spl470_887 ),
inference(avatar_component_clause,[],[f9207]) ).
thf(f9233,plain,
( ( ( setadjoin @ sK424 @ emptyset )
= ( setadjoin @ sK424 @ ( setadjoin @ sK423 @ emptyset ) ) )
| ~ spl470_805
| ~ spl470_837 ),
inference(forward_demodulation,[],[f6484,f7252]) ).
thf(f9235,plain,
( ( ( setadjoin @ sK424 @ emptyset )
= ( setadjoin @ sK424 @ ( setadjoin @ sK423 @ emptyset ) ) )
| ~ spl470_817
| ~ spl470_837 ),
inference(forward_demodulation,[],[f6830,f7252]) ).
thf(f9238,definition,
( spl470_892
<=> ( ( setadjoin @ sK424 @ emptyset )
= ( setadjoin @ sK424 @ ( setadjoin @ sK423 @ emptyset ) ) ) ),
introduced(definition,[new_symbols(definition,[spl470_892])],[avatar_definition]) ).
thf(f9240,plain,
( ( ( setadjoin @ sK424 @ emptyset )
= ( setadjoin @ sK424 @ ( setadjoin @ sK423 @ emptyset ) ) )
| ~ spl470_892 ),
inference(avatar_component_clause,[],[f9238]) ).
thf(f9241,plain,
( spl470_892
| ~ spl470_805
| ~ spl470_837 ),
inference(avatar_split_clause,[],[f9233,f7250,f6482,f9238]) ).
thf(f9243,plain,
( spl470_892
| ~ spl470_817
| ~ spl470_837 ),
inference(avatar_split_clause,[],[f9235,f7250,f6828,f9238]) ).
thf(f9248,plain,
( ( ( in @ sK423 @ ( setadjoin @ sK424 @ emptyset ) )
= $true )
| ~ spl470_477
| ~ spl470_892 ),
inference(superposition,[],[f4417,f9240]) ).
thf(f9266,plain,
( spl470_819
| ~ spl470_477
| ~ spl470_892 ),
inference(avatar_split_clause,[],[f9248,f9238,f4416,f6909]) ).
thf(f9356,plain,
( ( sK424 != sK426 )
| spl470_557
| ~ spl470_840 ),
inference(superposition,[],[f4804,f7450]) ).
thf(f9367,definition,
( spl470_894
<=> ( sK424 = sK426 ) ),
introduced(definition,[new_symbols(definition,[spl470_894])],[avatar_definition]) ).
thf(f9369,plain,
( ( sK424 != sK426 )
| spl470_894 ),
inference(avatar_component_clause,[],[f9367]) ).
thf(f9370,plain,
( ~ spl470_894
| spl470_557
| ~ spl470_840 ),
inference(avatar_split_clause,[],[f9356,f7448,f4802,f9367]) ).
thf(f9426,plain,
( ! [X0: $i] :
( ( ( setadjoin @ sK425 @ emptyset )
= X0 )
| ( ( in @ X0 @ ( setadjoin @ ( setadjoin @ sK424 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) ) @ emptyset ) ) )
!= $true )
| ( ( in @ X0 @ ( setadjoin @ ( setadjoin @ sK424 @ ( setadjoin @ sK423 @ emptyset ) ) @ emptyset ) )
= $true ) )
| ~ spl470_84
| ~ spl470_456
| ~ spl470_837 ),
inference(forward_demodulation,[],[f6787,f7252]) ).
thf(f9427,plain,
( ! [X0: $i] :
( ( ( in @ X0 @ ( setadjoin @ ( setadjoin @ sK424 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) ) @ emptyset ) ) )
!= $true )
| ( ( setadjoin @ sK424 @ emptyset )
= X0 )
| ( ( in @ X0 @ ( setadjoin @ ( setadjoin @ sK424 @ ( setadjoin @ sK423 @ emptyset ) ) @ emptyset ) )
= $true ) )
| ~ spl470_84
| ~ spl470_456
| ~ spl470_837 ),
inference(forward_demodulation,[],[f9426,f7252]) ).
thf(f9428,plain,
( ! [X0: $i] :
( ( ( in @ X0 @ ( setadjoin @ ( setadjoin @ sK424 @ emptyset ) @ emptyset ) )
= $true )
| ( ( in @ X0 @ ( setadjoin @ ( setadjoin @ sK424 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) ) @ emptyset ) ) )
!= $true )
| ( ( setadjoin @ sK424 @ emptyset )
= X0 ) )
| ~ spl470_84
| ~ spl470_456
| ~ spl470_837
| ~ spl470_892 ),
inference(forward_demodulation,[],[f9427,f9240]) ).
thf(f9429,plain,
( ! [X0: $i] :
( ( ( in @ X0 @ ( setadjoin @ ( setadjoin @ sK424 @ emptyset ) @ ( setadjoin @ ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) ) @ emptyset ) ) )
!= $true )
| ( ( setadjoin @ sK424 @ emptyset )
= X0 ) )
| ~ spl470_18
| ~ spl470_84
| ~ spl470_456
| ~ spl470_837
| ~ spl470_892 ),
inference(forward_subsumption_resolution,[],[f9428,f2319]) ).
thf(f9431,plain,
( ( ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) )
= ( setadjoin @ sK424 @ emptyset ) )
| ( $true != $true )
| ~ spl470_18
| ~ spl470_84
| ~ spl470_456
| ~ spl470_477
| ~ spl470_837
| ~ spl470_892 ),
inference(superposition,[],[f9429,f4417]) ).
thf(f9483,plain,
( ( ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) )
= ( setadjoin @ sK424 @ emptyset ) )
| ~ spl470_18
| ~ spl470_84
| ~ spl470_456
| ~ spl470_477
| ~ spl470_837
| ~ spl470_892 ),
inference(trivial_inequality_removal,[],[f9431]) ).
thf(f9498,plain,
( spl470_886
| ~ spl470_18
| ~ spl470_84
| ~ spl470_456
| ~ spl470_477
| ~ spl470_837
| ~ spl470_892 ),
inference(avatar_split_clause,[],[f9483,f9238,f7250,f4416,f4310,f2606,f2318,f9203]) ).
thf(f9725,plain,
( ( ( in @ sK426 @ ( setadjoin @ sK424 @ emptyset ) )
= $true )
| ~ spl470_477
| ~ spl470_886 ),
inference(superposition,[],[f4417,f9205]) ).
thf(f9742,definition,
( spl470_900
<=> ( ( in @ sK426 @ ( setadjoin @ sK424 @ emptyset ) )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl470_900])],[avatar_definition]) ).
thf(f9744,plain,
( ( ( in @ sK426 @ ( setadjoin @ sK424 @ emptyset ) )
= $true )
| ~ spl470_900 ),
inference(avatar_component_clause,[],[f9742]) ).
thf(f9745,plain,
( spl470_900
| ~ spl470_477
| ~ spl470_886 ),
inference(avatar_split_clause,[],[f9725,f9203,f4416,f9742]) ).
thf(f9815,plain,
( ( $true != $true )
| ( sK424 = sK426 )
| ~ spl470_18
| ~ spl470_900 ),
inference(superposition,[],[f2319,f9744]) ).
thf(f9820,plain,
( ( sK424 = sK426 )
| ~ spl470_18
| ~ spl470_900 ),
inference(trivial_inequality_removal,[],[f9815]) ).
thf(f9823,plain,
( $false
| ~ spl470_18
| spl470_894
| ~ spl470_900 ),
inference(forward_subsumption_resolution,[],[f9820,f9369]) ).
thf(f9824,plain,
( ~ spl470_18
| spl470_894
| ~ spl470_900 ),
inference(avatar_contradiction_clause,[],[f9823]) ).
thf(f9855,plain,
( ( ( setadjoin @ sK424 @ emptyset )
!= ( setadjoin @ sK424 @ ( setadjoin @ sK423 @ emptyset ) ) )
| spl470_805
| ~ spl470_837 ),
inference(forward_demodulation,[],[f6483,f7252]) ).
thf(f9879,plain,
( ~ spl470_892
| spl470_805
| ~ spl470_837 ),
inference(avatar_split_clause,[],[f9855,f7250,f6482,f9238]) ).
thf(f10163,plain,
( ( ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) )
= ( setadjoin @ sK424 @ ( setadjoin @ sK423 @ emptyset ) ) )
| ~ spl470_828
| ~ spl470_837 ),
inference(forward_demodulation,[],[f6987,f7252]) ).
thf(f10164,plain,
( spl470_887
| ~ spl470_828
| ~ spl470_837 ),
inference(avatar_split_clause,[],[f10163,f7250,f6985,f9207]) ).
thf(f10201,plain,
( ( ( in @ sK423 @ ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) ) )
= $true )
| ~ spl470_477
| ~ spl470_887 ),
inference(superposition,[],[f4417,f9209]) ).
thf(f10222,definition,
( spl470_921
<=> ( ( in @ sK423 @ ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) ) )
= $true ) ),
introduced(definition,[new_symbols(definition,[spl470_921])],[avatar_definition]) ).
thf(f10224,plain,
( ( ( in @ sK423 @ ( setadjoin @ sK424 @ ( setadjoin @ sK426 @ emptyset ) ) )
= $true )
| ~ spl470_921 ),
inference(avatar_component_clause,[],[f10222]) ).
thf(f10225,plain,
( spl470_921
| ~ spl470_477
| ~ spl470_887 ),
inference(avatar_split_clause,[],[f10201,f9207,f4416,f10222]) ).
thf(f10251,plain,
( ( sK423 = sK426 )
| ( $true != $true )
| ( sK424 = sK423 )
| ~ spl470_295
| ~ spl470_921 ),
inference(superposition,[],[f3563,f10224]) ).
thf(f10258,plain,
( ( sK423 = sK426 )
| ( sK424 = sK423 )
| ~ spl470_295
| ~ spl470_921 ),
inference(trivial_inequality_removal,[],[f10251]) ).
thf(f10269,plain,
( ( sK424 = sK423 )
| ~ spl470_295
| spl470_557
| ~ spl470_921 ),
inference(forward_subsumption_resolution,[],[f10258,f4804]) ).
thf(f10270,plain,
( spl470_840
| ~ spl470_295
| spl470_557
| ~ spl470_921 ),
inference(avatar_split_clause,[],[f10269,f10222,f4802,f3562,f7448]) ).
cnf(s4,plain,
( spl470_5
| ~ spl470_6 ),
inference(sat_conversion,[],[f2270]) ).
cnf(s52,plain,
( ~ spl470_81
| spl470_82 ),
inference(sat_conversion,[],[f2600]) ).
cnf(s103,plain,
( ~ spl470_161
| spl470_162 ),
inference(sat_conversion,[],[f2952]) ).
cnf(s144,plain,
spl470_6,
inference(sat_conversion,[],[f3209]) ).
cnf(s228,plain,
( ~ spl470_179
| spl470_295 ),
inference(sat_conversion,[],[f3626]) ).
cnf(s234,plain,
( spl470_18
| ~ spl470_317 ),
inference(sat_conversion,[],[f3663]) ).
cnf(s245,plain,
spl470_81,
inference(sat_conversion,[],[f3721]) ).
cnf(s290,plain,
spl470_317,
inference(sat_conversion,[],[f3924]) ).
cnf(s331,plain,
( spl470_63
| ~ spl470_147 ),
inference(sat_conversion,[],[f4077]) ).
cnf(s383,plain,
spl470_456,
inference(sat_conversion,[],[f4313]) ).
cnf(s441,plain,
spl470_236,
inference(sat_conversion,[],[f4547]) ).
cnf(s505,plain,
~ spl470_557,
inference(sat_conversion,[],[f4805]) ).
cnf(s561,plain,
spl470_161,
inference(sat_conversion,[],[f5015]) ).
cnf(s590,plain,
( spl470_84
| ~ spl470_147 ),
inference(sat_conversion,[],[f5118]) ).
cnf(s683,plain,
spl470_179,
inference(sat_conversion,[],[f5461]) ).
cnf(s722,plain,
( ~ spl470_236
| spl470_477 ),
inference(sat_conversion,[],[f5598]) ).
cnf(s757,plain,
spl470_147,
inference(sat_conversion,[],[f5736]) ).
cnf(s807,plain,
( ~ spl470_63
| ~ spl470_456
| spl470_787 ),
inference(sat_conversion,[],[f6134]) ).
cnf(s816,plain,
( ~ spl470_456
| ~ spl470_477
| spl470_794 ),
inference(sat_conversion,[],[f6337]) ).
cnf(s823,plain,
( ~ spl470_162
| ~ spl470_456
| spl470_804
| spl470_805 ),
inference(sat_conversion,[],[f6485]) ).
cnf(s848,plain,
( ~ spl470_295
| ~ spl470_794
| spl470_817
| spl470_828 ),
inference(sat_conversion,[],[f6988]) ).
cnf(s858,plain,
( ~ spl470_82
| ~ spl470_456
| ~ spl470_804
| ~ spl470_820 ),
inference(sat_conversion,[],[f7217]) ).
cnf(s864,plain,
( ~ spl470_18
| ~ spl470_819
| spl470_840 ),
inference(sat_conversion,[],[f7451]) ).
cnf(s882,plain,
( spl470_820
| ~ spl470_837
| ~ spl470_840 ),
inference(sat_conversion,[],[f8147]) ).
cnf(s904,plain,
( ~ spl470_5
| ~ spl470_787
| spl470_837 ),
inference(sat_conversion,[],[f8680]) ).
cnf(s929,plain,
( ~ spl470_805
| ~ spl470_837
| spl470_892 ),
inference(sat_conversion,[],[f9241]) ).
cnf(s931,plain,
( ~ spl470_817
| ~ spl470_837
| spl470_892 ),
inference(sat_conversion,[],[f9243]) ).
cnf(s932,plain,
( ~ spl470_477
| spl470_819
| ~ spl470_892 ),
inference(sat_conversion,[],[f9266]) ).
cnf(s936,plain,
( spl470_557
| ~ spl470_840
| ~ spl470_894 ),
inference(sat_conversion,[],[f9370]) ).
cnf(s952,plain,
( ~ spl470_18
| ~ spl470_84
| ~ spl470_456
| ~ spl470_477
| ~ spl470_837
| spl470_886
| ~ spl470_892 ),
inference(sat_conversion,[],[f9498]) ).
cnf(s961,plain,
( ~ spl470_477
| ~ spl470_886
| spl470_900 ),
inference(sat_conversion,[],[f9745]) ).
cnf(s967,plain,
( ~ spl470_18
| spl470_894
| ~ spl470_900 ),
inference(sat_conversion,[],[f9824]) ).
cnf(s1001,plain,
( spl470_805
| ~ spl470_837
| ~ spl470_892 ),
inference(sat_conversion,[],[f9879]) ).
cnf(s1019,plain,
( ~ spl470_828
| ~ spl470_837
| spl470_887 ),
inference(sat_conversion,[],[f10164]) ).
cnf(s1021,plain,
( ~ spl470_477
| ~ spl470_887
| spl470_921 ),
inference(sat_conversion,[],[f10225]) ).
cnf(s1026,plain,
( ~ spl470_295
| spl470_557
| spl470_840
| ~ spl470_921 ),
inference(sat_conversion,[],[f10270]) ).
cnf(s1041,plain,
spl470_84,
inference(rat,[],[s590,s757]) ).
cnf(s1069,plain,
spl470_477,
inference(rat,[],[s722,s441]) ).
cnf(s1088,plain,
spl470_794,
inference(rat,[],[s816,s1069,s383]) ).
cnf(s1100,plain,
spl470_63,
inference(rat,[],[s331,s757]) ).
cnf(s1101,plain,
spl470_787,
inference(rat,[],[s807,s383,s1100]) ).
cnf(s1135,plain,
spl470_18,
inference(rat,[],[s234,s290]) ).
cnf(s1136,plain,
spl470_295,
inference(rat,[],[s228,s683]) ).
cnf(s1190,plain,
spl470_162,
inference(rat,[],[s103,s561]) ).
cnf(s1220,plain,
spl470_82,
inference(rat,[],[s52,s245]) ).
cnf(s1258,plain,
spl470_5,
inference(rat,[],[s4,s144]) ).
cnf(s1259,plain,
spl470_837,
inference(rat,[],[s904,s1101,s1258]) ).
cnf(s1275,plain,
spl470_805,
inference(rat,[],[s1021,s1026,s1019,s882,s848,s858,s931,s823,s1001,s1069,s505,s1136,s1259,s1088,s383,s1220,s1190]) ).
cnf(s1276,plain,
spl470_892,
inference(rat,[],[s929,s1259,s1275]) ).
cnf(s1278,plain,
spl470_819,
inference(rat,[],[s932,s1069,s1276]) ).
cnf(s1281,plain,
spl470_886,
inference(rat,[],[s952,s1259,s1135,s383,s1069,s1041,s1276]) ).
cnf(s1289,plain,
spl470_840,
inference(rat,[],[s864,s1135,s1278]) ).
cnf(s1294,plain,
spl470_900,
inference(rat,[],[s961,s1069,s1281]) ).
cnf(s1299,plain,
~ spl470_894,
inference(rat,[],[s936,s505,s1289]) ).
cnf(s1301,plain,
$false,
inference(rat,[],[s967,s1135,s1294,s1299]) ).
thf(f10271,plain,
$false,
inference(avatar_sat_refutation,[],[s1301]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU653^1 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n019.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Tue Sep 29 14:03:03 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running higher-order theorem proving
% 0.09/0.26 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.63/0.38 % (821262)Detected a higher-order problem, will run a greedy HOL sequence.
% 0.63/0.38 % (821267)lrs+10_40_drc=off:e2e=on:si=on:uwa=one_side_interpreted:random_seed=831767570:s2a=on:i=87:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/87Mi)
% 0.63/0.38 % (821273)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 0.63/0.38 % (821273)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.63/0.38 % (821268)lrs+10_16_si=on:nwc=1.5:random_seed=4087471512:i=18:kws=arity_squared:rtra=on:fe=abstraction:ntd=on_2999 on theBenchmark for (2999ds/18Mi)
% 0.63/0.38 % (821269)lrs+10_1_cnfonf=off:si=on:uwa=one_side_interpreted:random_seed=3362672914:i=3:rtra=on:inj=on:ntd=on_2999 on theBenchmark for (2999ds/3Mi)
% 0.63/0.38 % (821271)dis+21_4_fde=none:e2e=on:si=on:uwa=off:foolp=on:random_seed=4063695596:i=24:av=off:rtra=on_2999 on theBenchmark for (2999ds/24Mi)
% 0.63/0.38 % (821270)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=2806153931:hsq=on:hsqr=16,1:s2a=on:i=634:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2999 on theBenchmark for (2999ds/634Mi)
% 0.63/0.38 % (821272)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=724361155:s2a=on:i=75:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2999 on theBenchmark for (2999ds/75Mi)
% 0.63/0.38 % (821273)dis+1002_8_to=kbo:sil=128000:tgt=full:drc=off:si=on:sp=const_max:lma=off:spb=non_intro:cbe=off:uwa=interpreted_only:random_seed=1677341694:hsqr=1,8:i=157:s2at=5:add=on:nm=2:rtra=on_2999 on theBenchmark for (2999ds/157Mi)
% 0.63/0.38 % (821269)Instruction limit reached!
% 0.63/0.38 % (821269)------------------------------
% 0.63/0.38 % (821269)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.38 % (821269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.38 % (821269)CaDiCaL version: 2.1.3
% 0.63/0.38 % (821269)Termination reason: Instruction limit
% 0.63/0.38 % (821269)Termination phase: shuffling
% 0.63/0.38 % (821269)Time elapsed: 0.002 s
% 0.63/0.38 % (821269)Peak memory usage: 10 MB
% 0.63/0.38 % (821269)Instructions burned: 3 (million)
% 0.63/0.38 % (821268)Instruction limit reached!
% 0.63/0.38 % (821268)------------------------------
% 0.63/0.38 % (821268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.38 % (821268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.38 % (821268)CaDiCaL version: 2.1.3
% 0.63/0.38 % (821268)Termination reason: Instruction limit
% 0.63/0.38 % (821268)Termination phase: shuffling
% 0.63/0.38 % (821268)Time elapsed: 0.008 s
% 0.63/0.38 % (821268)Peak memory usage: 10 MB
% 0.63/0.38 % (821268)Instructions burned: 18 (million)
% 0.63/0.38 % (821271)Instruction limit reached!
% 0.63/0.38 % (821271)------------------------------
% 0.63/0.38 % (821271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.38 % (821271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.38 % (821271)CaDiCaL version: 2.1.3
% 0.63/0.38 % (821271)Termination reason: Instruction limit
% 0.63/0.38 % (821271)Termination phase: Preprocessing 3
% 0.63/0.38 % (821271)Time elapsed: 0.012 s
% 0.63/0.38 % (821271)Peak memory usage: 11 MB
% 0.63/0.38 % (821271)Instructions burned: 25 (million)
% 0.63/0.38 % (821267)Instruction limit reached!
% 0.63/0.38 % (821267)------------------------------
% 0.63/0.38 % (821267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.38 % (821267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.38 % (821267)CaDiCaL version: 2.1.3
% 0.63/0.38 % (821267)Termination reason: Instruction limit
% 0.63/0.38 % (821267)Termination phase: Property scanning
% 0.63/0.38 % (821267)Time elapsed: 0.022 s
% 0.63/0.38 % (821267)Peak memory usage: 12 MB
% 0.63/0.38 % (821267)Instructions burned: 90 (million)
% 0.63/0.38 % (821281)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=4239676974:i=2:hud=10:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.63/0.38 % (821284)lrs+10_1_sil=128000:si=on:urr=on:slsqc=1:slsq=on:random_seed=2345369836:i=12:s2at=2:kws=inv_frequency:bd=all:rtra=on_2999 on theBenchmark for (2999ds/12Mi)
% 0.63/0.38 % (821281)Instruction limit reached!
% 0.63/0.42 % (821281)------------------------------
% 0.63/0.42 % (821281)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.42 % (821281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.42 % (821281)CaDiCaL version: 2.1.3
% 0.63/0.42 % (821281)Termination reason: Instruction limit
% 0.63/0.42 % (821281)Termination phase: shuffling
% 0.63/0.42 % (821281)Time elapsed: 0.002 s
% 0.63/0.42 % (821281)Peak memory usage: 9 MB
% 0.63/0.42 % (821281)Instructions burned: 4 (million)
% 0.63/0.42 % (821283)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.63/0.42 % (821284)Instruction limit reached!
% 0.63/0.42 % (821284)------------------------------
% 0.63/0.42 % (821284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.42 % (821284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.42 % (821282)lrs+1010_2:3_cha=on:si=on:uwa=off:nwc=1:random_seed=2559336100:i=5:fgj=on:av=off:rtra=on:fe=axiom:ntd=on_2999 on theBenchmark for (2999ds/5Mi)
% 0.63/0.42 % (821284)CaDiCaL version: 2.1.3
% 0.63/0.42 % (821284)Termination reason: Instruction limit
% 0.63/0.42 % (821284)Termination phase: shuffling
% 0.63/0.42 % (821284)Time elapsed: 0.003 s
% 0.63/0.42 % (821284)Peak memory usage: 10 MB
% 0.63/0.42 % (821284)Instructions burned: 12 (million)
% 0.63/0.42 % (821283)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=3639632511:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2999 on theBenchmark for (2999ds/7Mi)
% 0.63/0.42 % (821282)Instruction limit reached!
% 0.63/0.42 % (821282)------------------------------
% 0.63/0.42 % (821282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.42 % (821282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.42 % (821282)CaDiCaL version: 2.1.3
% 0.63/0.42 % (821282)Termination reason: Instruction limit
% 0.63/0.42 % (821282)Termination phase: shuffling
% 0.63/0.42 % (821282)Time elapsed: 0.003 s
% 0.63/0.42 % (821282)Peak memory usage: 10 MB
% 0.63/0.42 % (821282)Instructions burned: 7 (million)
% 0.63/0.42 % (821272)Instruction limit reached!
% 0.63/0.42 % (821272)------------------------------
% 0.63/0.42 % (821272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.42 % (821272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.42 % (821272)CaDiCaL version: 2.1.3
% 0.63/0.42 % (821272)Termination reason: Instruction limit
% 0.63/0.42 % (821272)Termination phase: Property scanning
% 0.63/0.42 % (821272)Time elapsed: 0.035 s
% 0.63/0.42 % (821272)Peak memory usage: 12 MB
% 0.63/0.42 % (821272)Instructions burned: 77 (million)
% 0.63/0.42 % (821283)Instruction limit reached!
% 0.63/0.42 % (821283)------------------------------
% 0.63/0.42 % (821283)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.42 % (821283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.42 % (821283)CaDiCaL version: 2.1.3
% 0.63/0.42 % (821283)Termination reason: Instruction limit
% 0.63/0.42 % (821283)Termination phase: shuffling
% 0.63/0.42 % (821283)Time elapsed: 0.004 s
% 0.63/0.42 % (821283)Peak memory usage: 10 MB
% 0.63/0.42 % (821283)Instructions burned: 8 (million)
% 0.63/0.42 % (821289)lrs+1002_64_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sp=occurrence:lma=off:plsqr=32,1:uwa=interpreted_only:random_seed=2031068448:i=86:piset=equals:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/86Mi)
% 0.63/0.42 % (821287)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 0.63/0.42 % (821287)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(1) has been set then forward_subsumption_demodulation(off) is equal to on
% 0.63/0.42 % (821287)ott+1010_64_tgt=ground:cnfonf=lazy_simp:si=on:lma=off:spb=goal:lcm=predicate:random_seed=61357835:i=28:s2at=5:piset=not:hud=10:bd=all:av=off:rtra=on:ixr=off:fsdmm=1_2999 on theBenchmark for (2999ds/28Mi)
% 0.63/0.42 % (821291)lrs+10_1_si=on:cs=on:random_seed=3000259948:i=8:rtra=on:ntd=on_2999 on theBenchmark for (2999ds/8Mi)
% 0.63/0.42 % (821292)WARNING Broken Constraint: if positive_literal_split_queue_ratios(1,32) has been set then positive_literal_split_queue(off) is equal to on
% 0.63/0.45 % (821293)lrs+1002_3:1_sil=128000:e2e=on:si=on:urr=on:uwa=one_side_constant:nwc=1.5:random_seed=3438775661:i=38:bd=all:rtra=on:amm=off:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/38Mi)
% 0.63/0.45 % (821292)ott+1002_20_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:plsqr=1,32:bce=on:uwa=interpreted_only:foolp=on:random_seed=4038407351:i=2:add=on:rtra=on_2999 on theBenchmark for (2999ds/2Mi)
% 0.63/0.45 % (821291)Instruction limit reached!
% 0.63/0.45 % (821291)------------------------------
% 0.63/0.45 % (821291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.45 % (821291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.45 % (821291)CaDiCaL version: 2.1.3
% 0.63/0.45 % (821291)Termination reason: Instruction limit
% 0.63/0.45 % (821291)Termination phase: shuffling
% 0.63/0.45 % (821291)Time elapsed: 0.005 s
% 0.63/0.45 % (821291)Peak memory usage: 10 MB
% 0.63/0.45 % (821291)Instructions burned: 10 (million)
% 0.63/0.45 % (821292)Instruction limit reached!
% 0.63/0.45 % (821292)------------------------------
% 0.63/0.45 % (821292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.45 % (821292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.45 % (821292)CaDiCaL version: 2.1.3
% 0.63/0.45 % (821292)Termination reason: Instruction limit
% 0.63/0.45 % (821292)Termination phase: shuffling
% 0.63/0.45 % (821292)Time elapsed: 0.002 s
% 0.63/0.45 % (821292)Peak memory usage: 10 MB
% 0.63/0.45 % (821292)Instructions burned: 3 (million)
% 0.63/0.45 % (821289)Instruction limit reached!
% 0.63/0.45 % (821289)------------------------------
% 0.63/0.45 % (821289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.45 % (821289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.45 % (821289)CaDiCaL version: 2.1.3
% 0.63/0.45 % (821289)Termination reason: Instruction limit
% 0.63/0.45 % (821289)Termination phase: Saturation
% 0.63/0.45 % (821289)Time elapsed: 0.019 s
% 0.63/0.45 % (821289)Peak memory usage: 12 MB
% 0.63/0.45 % (821289)Instructions burned: 89 (million)
% 0.63/0.45 % (821287)Instruction limit reached!
% 0.63/0.45 % (821287)------------------------------
% 0.63/0.45 % (821287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.45 % (821287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.45 % (821287)CaDiCaL version: 2.1.3
% 0.63/0.45 % (821287)Termination reason: Instruction limit
% 0.63/0.45 % (821287)Termination phase: Property scanning
% 0.63/0.45 % (821287)Time elapsed: 0.013 s
% 0.63/0.45 % (821287)Peak memory usage: 10 MB
% 0.63/0.45 % (821287)Instructions burned: 29 (million)
% 0.63/0.45 % (821273)Instruction limit reached!
% 0.63/0.45 % (821273)------------------------------
% 0.63/0.45 % (821273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.45 % (821273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.45 % (821273)CaDiCaL version: 2.1.3
% 0.63/0.45 % (821273)Termination reason: Instruction limit
% 0.63/0.45 % (821273)Termination phase: Saturation
% 0.63/0.45 % (821273)Time elapsed: 0.067 s
% 0.63/0.45 % (821273)Peak memory usage: 13 MB
% 0.63/0.45 % (821273)Instructions burned: 158 (million)
% 0.63/0.45 % (821301)lrs+10_16:1_sil=128000:si=on:lma=off:urr=on:uwa=interpreted_only:random_seed=3178222320:i=14:kws=precedence:aac=none:nm=10:rtra=on:er=filter:ntd=on_2999 on theBenchmark for (2999ds/14Mi)
% 0.63/0.45 % (821301)Instruction limit reached!
% 0.63/0.45 % (821301)------------------------------
% 0.63/0.45 % (821301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.45 % (821301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.45 % (821301)CaDiCaL version: 2.1.3
% 0.63/0.45 % (821301)Termination reason: Instruction limit
% 0.63/0.45 % (821301)Termination phase: shuffling
% 0.63/0.45 % (821301)Time elapsed: 0.004 s
% 0.63/0.45 % (821301)Peak memory usage: 10 MB
% 0.63/0.45 % (821301)Instructions burned: 17 (million)
% 0.63/0.45 % (821293)Instruction limit reached!
% 0.63/0.45 % (821293)------------------------------
% 0.63/0.45 % (821293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.63/0.45 % (821293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.63/0.45 % (821293)CaDiCaL version: 2.1.3
% 0.63/0.45 % (821293)Termination reason: Instruction limit
% 0.63/0.45 % (821293)Termination phase: Preprocessing 3
% 0.63/0.45 % (821293)Time elapsed: 0.018 s
% 1.39/0.52 % (821293)Peak memory usage: 11 MB
% 1.39/0.52 % (821293)Instructions burned: 39 (million)
% 1.39/0.52 % (821299)lrs+1002_1_to=lpo:sil=128000:si=on:sos=on:spb=goal_then_units:uwa=off:random_seed=393915686:st=2:i=249:sd=1:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/249Mi)
% 1.39/0.52 % (821300)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=4210881978:hsq=on:st=2:i=25:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2999 on theBenchmark for (2999ds/25Mi)
% 1.39/0.52 % (821302)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=1585516815:st=3:s2a=on:i=327:sd=3:rtra=on:ss=axioms_2999 on theBenchmark for (2999ds/327Mi)
% 1.39/0.52 % (821305)ott+21_20_to=lpo:sil=128000:tgt=ground:si=on:sp=arity:lma=off:uwa=off:foolp=on:random_seed=3903989638:st=4:i=2:add=off:sd=3:nm=16:fsr=off:rtra=on:ss=axioms:sgt=8:ntd=on_2998 on theBenchmark for (2998ds/2Mi)
% 1.39/0.52 % (821305)Instruction limit reached!
% 1.39/0.52 % (821305)------------------------------
% 1.39/0.52 % (821305)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.39/0.52 % (821305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.39/0.52 % (821305)CaDiCaL version: 2.1.3
% 1.39/0.52 % (821305)Termination reason: Instruction limit
% 1.39/0.52 % (821305)Termination phase: shuffling
% 1.39/0.52 % (821305)Time elapsed: 0.001 s
% 1.39/0.52 % (821305)Peak memory usage: 10 MB
% 1.39/0.52 % (821305)Instructions burned: 3 (million)
% 1.39/0.52 % (821303)dis+10_1_anc=all_dependent:to=kbo:sil=128000:si=on:chr=on:random_seed=1569655788:uwa_fpi=on:i=14:aac=none:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/14Mi)
% 1.39/0.52 % (821300)Instruction limit reached!
% 1.39/0.52 % (821300)------------------------------
% 1.39/0.52 % (821300)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.39/0.52 % (821300)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.39/0.52 % (821300)CaDiCaL version: 2.1.3
% 1.39/0.52 % (821300)Termination reason: Instruction limit
% 1.39/0.52 % (821300)Termination phase: SInE selection
% 1.39/0.52 % (821300)Time elapsed: 0.011 s
% 1.39/0.52 % (821300)Peak memory usage: 10 MB
% 1.39/0.52 % (821300)Instructions burned: 26 (million)
% 1.39/0.52 % (821306)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1188190779:i=26:ep=R:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/26Mi)
% 1.39/0.52 % (821303)Instruction limit reached!
% 1.39/0.52 % (821303)------------------------------
% 1.39/0.52 % (821303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.39/0.52 % (821303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.39/0.52 % (821303)CaDiCaL version: 2.1.3
% 1.39/0.52 % (821303)Termination reason: Instruction limit
% 1.39/0.52 % (821303)Termination phase: shuffling
% 1.39/0.52 % (821303)Time elapsed: 0.007 s
% 1.39/0.52 % (821303)Peak memory usage: 10 MB
% 1.39/0.52 % (821303)Instructions burned: 16 (million)
% 1.39/0.52 % (821311)dis+1002_16_sil=128000:si=on:sp=occurrence:random_seed=2996925828:cond=fast:i=23:hud=1:av=off:rtra=on:fe=abstraction:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 1.39/0.52 % (821311)Instruction limit reached!
% 1.39/0.52 % (821311)------------------------------
% 1.39/0.52 % (821311)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.39/0.52 % (821311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.39/0.52 % (821311)CaDiCaL version: 2.1.3
% 1.39/0.52 % (821311)Termination reason: Instruction limit
% 1.39/0.52 % (821311)Termination phase: Property scanning
% 1.39/0.52 % (821311)Time elapsed: 0.006 s
% 1.39/0.52 % (821311)Peak memory usage: 10 MB
% 1.39/0.52 % (821311)Instructions burned: 27 (million)
% 1.39/0.52 % (821306)Instruction limit reached!
% 1.39/0.52 % (821306)------------------------------
% 1.39/0.52 % (821306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.39/0.52 % (821306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.39/0.52 % (821306)CaDiCaL version: 2.1.3
% 1.39/0.52 % (821306)Termination reason: Instruction limit
% 1.39/0.52 % (821306)Termination phase: Property scanning
% 1.39/0.52 % (821306)Time elapsed: 0.012 s
% 1.39/0.52 % (821306)Peak memory usage: 10 MB
% 1.39/0.52 % (821306)Instructions burned: 27 (million)
% 1.39/0.52 % (821313)lrs+1002_1024_sil=128000:tgt=ground:fde=none:e2e=on:si=on:uwa=off:nwc=1:random_seed=3172589647:cond=on:i=60:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/60Mi)
% 1.39/0.52 % (821316)WARNING Broken Constraint: if sine_to_age_generality_threshold(10) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 2.11/0.57 % (821316)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(otter) is equal to lrs
% 2.11/0.57 % (821317)WARNING Broken Constraint: if choice_reasoning(on) has been set then choice_ax(on) is equal to off
% 2.11/0.57 % (821317)lrs+1010_4:1_slsqr=8,1:to=kbo:cha=on:drc=off:si=on:sp=arity:lcm=predicate:uwa=off:fd=preordered:gs=on:nwc=5:s2agt=32:slsqc=1:kmz=on:updr=off:chr=on:pe=on:slsq=on:random_seed=4151056313:i=8:nm=2:rtra=on:fe=abstraction:inj=on_2998 on theBenchmark for (2998ds/8Mi)
% 2.11/0.57 % (821316)ott+21_1_to=kbo:sil=128000:cnfonf=lazy_gen:bsd=on:si=on:sp=const_frequency:lma=off:uwa=off:foolp=on:s2agt=10:lwlo=on:random_seed=3350099305:i=14:add=off:nm=40:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.11/0.57 % (821317)Instruction limit reached!
% 2.11/0.57 % (821317)------------------------------
% 2.11/0.57 % (821317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.57 % (821317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.57 % (821317)CaDiCaL version: 2.1.3
% 2.11/0.57 % (821317)Termination reason: Instruction limit
% 2.11/0.57 % (821317)Termination phase: shuffling
% 2.11/0.57 % (821317)Time elapsed: 0.002 s
% 2.11/0.57 % (821317)Peak memory usage: 10 MB
% 2.11/0.57 % (821317)Instructions burned: 8 (million)
% 2.11/0.57 % (821316)Instruction limit reached!
% 2.11/0.57 % (821316)------------------------------
% 2.11/0.57 % (821316)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.57 % (821316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.57 % (821316)CaDiCaL version: 2.1.3
% 2.11/0.57 % (821316)Termination reason: Instruction limit
% 2.11/0.57 % (821316)Termination phase: shuffling
% 2.11/0.57 % (821316)Time elapsed: 0.006 s
% 2.11/0.57 % (821316)Peak memory usage: 10 MB
% 2.11/0.57 % (821316)Instructions burned: 14 (million)
% 2.11/0.57 % (821318)dis+1004_50_to=lpo:drc=off:fde=unused:cnfonf=lazy_not_gen_be_off:si=on:sp=reverse_arity:spb=units:cbe=off:foolp=on:random_seed=925876388:uwa_fpi=on:i=31:doe=on:bd=preordered:rtra=on:fsd=on_2998 on theBenchmark for (2998ds/31Mi)
% 2.11/0.57 % (821322)dis+10_1024_sil=128000:cnfonf=off:si=on:fd=off:random_seed=2052326535:i=7:hud=5:bd=preordered:rtra=on:bet=on_2998 on theBenchmark for (2998ds/7Mi)
% 2.11/0.57 % (821322)Instruction limit reached!
% 2.11/0.57 % (821322)------------------------------
% 2.11/0.57 % (821322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.57 % (821322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.57 % (821322)CaDiCaL version: 2.1.3
% 2.11/0.57 % (821322)Termination reason: Instruction limit
% 2.11/0.57 % (821322)Termination phase: shuffling
% 2.11/0.57 % (821322)Time elapsed: 0.003 s
% 2.11/0.57 % (821322)Peak memory usage: 10 MB
% 2.11/0.57 % (821322)Instructions burned: 11 (million)
% 2.11/0.57 % (821313)Instruction limit reached!
% 2.11/0.57 % (821313)------------------------------
% 2.11/0.57 % (821313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.57 % (821313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.57 % (821313)CaDiCaL version: 2.1.3
% 2.11/0.57 % (821313)Termination reason: Instruction limit
% 2.11/0.57 % (821313)Termination phase: Property scanning
% 2.11/0.57 % (821313)Time elapsed: 0.028 s
% 2.11/0.57 % (821313)Peak memory usage: 12 MB
% 2.11/0.57 % (821313)Instructions burned: 60 (million)
% 2.11/0.57 % (821323)lrs+10_1_plsq=on:drc=ordering:cnfonf=lazy_not_gen_be_off:bsd=on:si=on:plsqr=32,1:cs=on:random_seed=1240106177:i=23:rtra=on:ntd=on_2998 on theBenchmark for (2998ds/23Mi)
% 2.11/0.57 % (821318)Instruction limit reached!
% 2.11/0.57 % (821318)------------------------------
% 2.11/0.57 % (821318)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.11/0.57 % (821318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.11/0.57 % (821318)CaDiCaL version: 2.1.3
% 2.11/0.57 % (821318)Termination reason: Instruction limit
% 2.11/0.57 % (821318)Termination phase: Property scanning
% 2.11/0.57 % (821318)Time elapsed: 0.014 s
% 2.11/0.57 % (821318)Peak memory usage: 10 MB
% 2.11/0.57 % (821318)Instructions burned: 32 (million)
% 2.11/0.57 % (821326)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=272761419:s2a=on:i=20:kws=inv_frequency:bd=all:rtra=on_2998 on theBenchmark for (2998ds/20Mi)
% 2.38/0.66 % (821326)Instruction limit reached!
% 2.38/0.66 % (821326)------------------------------
% 2.38/0.66 % (821326)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.38/0.66 % (821326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.38/0.66 % (821326)CaDiCaL version: 2.1.3
% 2.38/0.66 % (821326)Termination reason: Instruction limit
% 2.38/0.66 % (821326)Termination phase: Property scanning
% 2.38/0.66 % (821326)Time elapsed: 0.005 s
% 2.38/0.66 % (821326)Peak memory usage: 10 MB
% 2.38/0.66 % (821326)Instructions burned: 20 (million)
% 2.38/0.66 % (821323)Instruction limit reached!
% 2.38/0.66 % (821323)------------------------------
% 2.38/0.66 % (821323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.38/0.66 % (821323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.38/0.66 % (821323)CaDiCaL version: 2.1.3
% 2.38/0.66 % (821323)Termination reason: Instruction limit
% 2.38/0.66 % (821323)Termination phase: Property scanning
% 2.38/0.66 % (821323)Time elapsed: 0.011 s
% 2.38/0.66 % (821323)Peak memory usage: 10 MB
% 2.38/0.66 % (821323)Instructions burned: 26 (million)
% 2.38/0.66 % (821327)dis+1010_2:1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:slsq=on:random_seed=2972116233:i=1240:rtra=on:ixr=off_2998 on theBenchmark for (2998ds/1240Mi)
% 2.38/0.66 % (821329)ott+1002_32_tgt=ground:si=on:sp=const_max:acc=on:nwc=0.5:random_seed=1483033037:i=143:fgj=on:piset=pi_sigma:rtra=on:fe=abstraction_2998 on theBenchmark for (2998ds/143Mi)
% 2.38/0.66 % (821331)lrs+1002_1_sil=128000:si=on:acc=on:uwa=off:random_seed=1731035095:st=5:s2a=on:i=193:sd=1:rtra=on:ss=axioms_2998 on theBenchmark for (2998ds/193Mi)
% 2.38/0.66 % (821332)dis+10_1024_sil=128000:si=on:sp=unary_first:urr=on:uwa=all:fd=off:random_seed=3319260075:i=42:hud=10:rtra=on_2998 on theBenchmark for (2998ds/42Mi)
% 2.38/0.66 % (821332)Instruction limit reached!
% 2.38/0.66 % (821332)------------------------------
% 2.38/0.66 % (821332)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.38/0.66 % (821332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.38/0.66 % (821332)CaDiCaL version: 2.1.3
% 2.38/0.66 % (821332)Termination reason: Instruction limit
% 2.38/0.66 % (821332)Termination phase: Property scanning
% 2.38/0.66 % (821332)Time elapsed: 0.018 s
% 2.38/0.66 % (821332)Peak memory usage: 11 MB
% 2.38/0.66 % (821332)Instructions burned: 42 (million)
% 2.38/0.66 % (821299)Instruction limit reached!
% 2.38/0.66 % (821299)------------------------------
% 2.38/0.66 % (821299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.38/0.66 % (821299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.38/0.66 % (821299)CaDiCaL version: 2.1.3
% 2.38/0.66 % (821299)Termination reason: Instruction limit
% 2.38/0.66 % (821299)Termination phase: Saturation
% 2.38/0.66 % (821299)Time elapsed: 0.122 s
% 2.38/0.66 % (821299)Peak memory usage: 14 MB
% 2.38/0.66 % (821299)Instructions burned: 249 (million)
% 2.38/0.66 % (821337)WARNING Broken Constraint: if forward_subsumption_demodulation_max_matches(5) has been set then forward_subsumption_demodulation(off) is equal to on
% 2.38/0.66 % (821337)dis+21_1_to=kbo:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:uwa=hol:random_seed=1385006666:uwa_fpi=on:i=7:fgj=on:hud=10:fsr=off:rtra=on:rawr=on:fsdmm=5_2997 on theBenchmark for (2997ds/7Mi)
% 2.38/0.66 % (821331)Instruction limit reached!
% 2.38/0.66 % (821331)------------------------------
% 2.38/0.66 % (821331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.38/0.66 % (821331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.38/0.66 % (821331)CaDiCaL version: 2.1.3
% 2.38/0.66 % (821331)Termination reason: Instruction limit
% 2.38/0.66 % (821331)Termination phase: Saturation
% 2.38/0.66 % (821331)Time elapsed: 0.049 s
% 2.38/0.66 % (821331)Peak memory usage: 14 MB
% 2.38/0.66 % (821331)Instructions burned: 195 (million)
% 2.38/0.66 % (821337)Instruction limit reached!
% 2.38/0.66 % (821337)------------------------------
% 2.38/0.66 % (821337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.38/0.66 % (821337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.38/0.66 % (821337)CaDiCaL version: 2.1.3
% 2.38/0.66 % (821337)Termination reason: Instruction limit
% 2.38/0.66 % (821337)Termination phase: shuffling
% 2.57/0.72 % (821337)Time elapsed: 0.004 s
% 2.57/0.72 % (821337)Peak memory usage: 10 MB
% 2.57/0.72 % (821337)Instructions burned: 9 (million)
% 2.57/0.72 % (821338)lrs+10_1_to=lpo:sil=128000:si=on:sp=arity:urr=on:random_seed=2579400550:i=181:sd=2:bd=preordered:rtra=on:ss=axioms_2997 on theBenchmark for (2997ds/181Mi)
% 2.57/0.72 % (821329)Instruction limit reached!
% 2.57/0.72 % (821329)------------------------------
% 2.57/0.72 % (821329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.72 % (821329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.72 % (821329)CaDiCaL version: 2.1.3
% 2.57/0.72 % (821329)Termination reason: Instruction limit
% 2.57/0.72 % (821329)Termination phase: Saturation
% 2.57/0.72 % (821329)Time elapsed: 0.061 s
% 2.57/0.72 % (821329)Peak memory usage: 14 MB
% 2.57/0.72 % (821329)Instructions burned: 144 (million)
% 2.57/0.72 % (821340)dis+10_8_sil=128000:plsq=on:plsqc=1:si=on:sp=unary_first:sos=on:lma=off:plsqr=64,1:uwa=interpreted_only:foolp=on:random_seed=80696428:st=3:avsq=on:i=169:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2997 on theBenchmark for (2997ds/169Mi)
% 2.57/0.72 % (821341)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(5) has been set then sine_level_split_queue(off) is equal to on
% 2.57/0.72 % (821341)lrs+1002_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=arity:cbe=off:uwa=all:slsqc=5:random_seed=944558938:st=4:s2a=on:i=6:add=on:doe=on:hud=10:rtra=on:bet=on:ss=axioms_2997 on theBenchmark for (2997ds/6Mi)
% 2.57/0.72 % (821302)Instruction limit reached!
% 2.57/0.72 % (821302)------------------------------
% 2.57/0.72 % (821302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.72 % (821302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.72 % (821302)CaDiCaL version: 2.1.3
% 2.57/0.72 % (821302)Termination reason: Instruction limit
% 2.57/0.72 % (821302)Termination phase: Saturation
% 2.57/0.72 % (821302)Time elapsed: 0.154 s
% 2.57/0.72 % (821302)Peak memory usage: 14 MB
% 2.57/0.72 % (821302)Instructions burned: 327 (million)
% 2.57/0.72 % (821341)Instruction limit reached!
% 2.57/0.72 % (821341)------------------------------
% 2.57/0.72 % (821341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.72 % (821341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.72 % (821341)CaDiCaL version: 2.1.3
% 2.57/0.72 % (821341)Termination reason: Instruction limit
% 2.57/0.72 % (821341)Termination phase: shuffling
% 2.57/0.72 % (821341)Time elapsed: 0.003 s
% 2.57/0.72 % (821341)Peak memory usage: 10 MB
% 2.57/0.72 % (821341)Instructions burned: 6 (million)
% 2.57/0.72 % (821343)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=172732797:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2997 on theBenchmark for (2997ds/22Mi)
% 2.57/0.72 % (821343)Instruction limit reached!
% 2.57/0.72 % (821343)------------------------------
% 2.57/0.72 % (821343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.72 % (821343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.72 % (821343)CaDiCaL version: 2.1.3
% 2.57/0.72 % (821343)Termination reason: Instruction limit
% 2.57/0.72 % (821343)Termination phase: Property scanning
% 2.57/0.72 % (821343)Time elapsed: 0.010 s
% 2.57/0.72 % (821343)Peak memory usage: 10 MB
% 2.57/0.72 % (821343)Instructions burned: 22 (million)
% 2.57/0.72 % (821346)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=3356443340:i=19:add=on:rtra=on_2997 on theBenchmark for (2997ds/19Mi)
% 2.57/0.72 % (821347)ott+10_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:lma=off:plsqr=128,1:urr=ec_only:uwa=off:rp=on:nwc=20:br=off:random_seed=3918623240:i=316:bs=unit_only:ins=25:rtra=on:ntd=on_2997 on theBenchmark for (2997ds/316Mi)
% 2.57/0.72 % (821340)Instruction limit reached!
% 2.57/0.72 % (821340)------------------------------
% 2.57/0.72 % (821340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.57/0.72 % (821340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.57/0.72 % (821340)CaDiCaL version: 2.1.3
% 2.57/0.72 % (821340)Termination reason: Instruction limit
% 2.57/0.72 % (821340)Termination phase: Saturation
% 2.57/0.72 % (821340)Time elapsed: 0.039 s
% 2.57/0.72 % (821340)Peak memory usage: 14 MB
% 2.57/0.72 % (821340)Instructions burned: 169 (million)
% 2.57/0.72 % (821346)Instruction limit reached!
% 2.57/0.72 % (821346)------------------------------
% 3.35/0.82 % (821346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.35/0.82 % (821346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.35/0.82 % (821346)CaDiCaL version: 2.1.3
% 3.35/0.82 % (821346)Termination reason: Instruction limit
% 3.35/0.82 % (821346)Termination phase: shuffling
% 3.35/0.82 % (821346)Time elapsed: 0.009 s
% 3.35/0.82 % (821346)Peak memory usage: 10 MB
% 3.35/0.82 % (821346)Instructions burned: 20 (million)
% 3.35/0.82 % (821349)dis+1004_4:1_slsqr=1,2:to=lpo:plsq=on:fde=unused:e2e=on:si=on:spb=goal_then_units:acc=on:urr=on:uwa=off:fd=preordered:s2agt=16:slsqc=1:slsq=on:random_seed=1372866375:hsq=on:hsqr=16,1:s2a=on:i=853:add=off:bd=all:nm=64:rtra=on:gtg=position:c=on:ntd=on_2997 on theBenchmark for (2997ds/853Mi)
% 3.35/0.82 % (821353)lrs+1002_1_sil=128000:fde=unused:e2e=on:si=on:sos=on:uwa=interpreted_only:random_seed=2035638539:i=480:rtra=on_2996 on theBenchmark for (2996ds/480Mi)
% 3.35/0.82 % (821352)dis+1003_3:4_to=kbo:plsq=on:prc=on:sims=off:e2e=on:si=on:spb=intro:acc=on:urr=on:uwa=off:foolp=on:s2agt=32:slsqc=3:slsq=on:random_seed=1192723762:hsq=on:hsqr=16,1:s2a=on:i=45:erml=3:slsql=off:rtra=on:gtg=exists_top:er=filter:ntd=on_2996 on theBenchmark for (2996ds/45Mi)
% 3.35/0.82 % (821338)Instruction limit reached!
% 3.35/0.82 % (821338)------------------------------
% 3.35/0.82 % (821338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.35/0.82 % (821338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.35/0.82 % (821338)CaDiCaL version: 2.1.3
% 3.35/0.82 % (821338)Termination reason: Instruction limit
% 3.35/0.82 % (821338)Termination phase: Saturation
% 3.35/0.82 % (821338)Time elapsed: 0.082 s
% 3.35/0.82 % (821338)Peak memory usage: 14 MB
% 3.35/0.82 % (821338)Instructions burned: 183 (million)
% 3.35/0.82 % (821352)Instruction limit reached!
% 3.35/0.82 % (821352)------------------------------
% 3.35/0.82 % (821352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.35/0.82 % (821352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.35/0.82 % (821352)CaDiCaL version: 2.1.3
% 3.35/0.82 % (821352)Termination reason: Instruction limit
% 3.35/0.82 % (821352)Termination phase: Preprocessing 3
% 3.35/0.82 % (821352)Time elapsed: 0.021 s
% 3.35/0.82 % (821352)Peak memory usage: 11 MB
% 3.35/0.82 % (821352)Instructions burned: 45 (million)
% 3.35/0.82 % (821358)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(2) has been set then sine_level_split_queue(off) is equal to on
% 3.35/0.82 % (821357)dis+1010_40_sil=128000:si=on:uwa=off:nwc=1:sac=on:chr=on:avsqc=3:random_seed=1182758824:avsq=on:i=21:avsqr=8,1:kws=frequency:fgj=on:bd=all:rtra=on:fe=axiom:ntd=on_2996 on theBenchmark for (2996ds/21Mi)
% 3.35/0.82 % (821358)ott+1002_3_si=on:sp=weighted_frequency:spb=goal:cbe=off:slsqc=2:random_seed=1826805710:cts=off:uwa_fpi=on:i=200:av=off:fsr=off:rtra=on:ntd=on_2996 on theBenchmark for (2996ds/200Mi)
% 3.35/0.82 % (821357)Instruction limit reached!
% 3.35/0.82 % (821357)------------------------------
% 3.35/0.82 % (821357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.35/0.82 % (821357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.35/0.82 % (821357)CaDiCaL version: 2.1.3
% 3.35/0.82 % (821357)Termination reason: Instruction limit
% 3.35/0.82 % (821357)Termination phase: Property scanning
% 3.35/0.82 % (821357)Time elapsed: 0.010 s
% 3.35/0.82 % (821357)Peak memory usage: 10 MB
% 3.35/0.82 % (821357)Instructions burned: 22 (million)
% 3.35/0.82 % (821270)Instruction limit reached!
% 3.35/0.82 % (821270)------------------------------
% 3.35/0.82 % (821270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.35/0.82 % (821270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.35/0.82 % (821270)CaDiCaL version: 2.1.3
% 3.35/0.82 % (821270)Termination reason: Instruction limit
% 3.35/0.82 % (821270)Termination phase: Saturation
% 3.35/0.82 % (821270)Time elapsed: 0.335 s
% 3.35/0.82 % (821270)Peak memory usage: 19 MB
% 3.35/0.82 % (821270)Instructions burned: 634 (million)
% 3.35/0.82 % (821361)lrs+10_1_sil=128000:fde=unused:si=on:random_seed=378688615:s2a=on:i=13:kws=inv_frequency:bd=all:rtra=on_2996 on theBenchmark for (2996ds/13Mi)
% 3.35/0.82 % (821362)lrs+1010_1_anc=none:slsqr=1,2:sil=128000:cnfonf=conj_eager:sas=cadical:si=on:hi=on:uwa=one_side_interpreted:rp=on:nwc=2:slsqc=3:slsq=on:random_seed=1272636865:i=66:s2at=3:nm=2:rtra=on:rawr=on_2996 on theBenchmark for (2996ds/66Mi)
% 3.74/1.01 % (821361)Instruction limit reached!
% 3.74/1.01 % (821361)------------------------------
% 3.74/1.01 % (821361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.74/1.01 % (821361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.01 % (821361)CaDiCaL version: 2.1.3
% 3.74/1.01 % (821361)Termination reason: Instruction limit
% 3.74/1.01 % (821361)Termination phase: shuffling
% 3.74/1.01 % (821361)Time elapsed: 0.006 s
% 3.74/1.01 % (821361)Peak memory usage: 10 MB
% 3.74/1.01 % (821361)Instructions burned: 14 (million)
% 3.74/1.01 % (821365)lrs+1004_128_si=on:sos=all:uwa=off:random_seed=4251918086:i=51:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/51Mi)
% 3.74/1.01 % (821362)Instruction limit reached!
% 3.74/1.01 % (821362)------------------------------
% 3.74/1.01 % (821362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.74/1.01 % (821362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.01 % (821362)CaDiCaL version: 2.1.3
% 3.74/1.01 % (821362)Termination reason: Instruction limit
% 3.74/1.01 % (821362)Termination phase: Function definition elimination
% 3.74/1.01 % (821362)Time elapsed: 0.028 s
% 3.74/1.01 % (821362)Peak memory usage: 11 MB
% 3.74/1.01 % (821362)Instructions burned: 66 (million)
% 3.74/1.01 % (821353)Instruction limit reached!
% 3.74/1.01 % (821353)------------------------------
% 3.74/1.01 % (821353)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.74/1.01 % (821353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.01 % (821353)CaDiCaL version: 2.1.3
% 3.74/1.01 % (821353)Termination reason: Instruction limit
% 3.74/1.01 % (821353)Termination phase: Saturation
% 3.74/1.01 % (821353)Time elapsed: 0.121 s
% 3.74/1.01 % (821353)Peak memory usage: 16 MB
% 3.74/1.01 % (821353)Instructions burned: 481 (million)
% 3.74/1.01 % (821365)Instruction limit reached!
% 3.74/1.01 % (821365)------------------------------
% 3.74/1.01 % (821365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.74/1.01 % (821365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.01 % (821365)CaDiCaL version: 2.1.3
% 3.74/1.01 % (821365)Termination reason: Instruction limit
% 3.74/1.01 % (821365)Termination phase: Property scanning
% 3.74/1.01 % (821365)Time elapsed: 0.022 s
% 3.74/1.01 % (821365)Peak memory usage: 11 MB
% 3.74/1.01 % (821365)Instructions burned: 53 (million)
% 3.74/1.01 % (821347)Instruction limit reached!
% 3.74/1.01 % (821347)------------------------------
% 3.74/1.01 % (821347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.74/1.01 % (821347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.01 % (821347)CaDiCaL version: 2.1.3
% 3.74/1.01 % (821347)Termination reason: Instruction limit
% 3.74/1.01 % (821347)Termination phase: Saturation
% 3.74/1.01 % (821347)Time elapsed: 0.146 s
% 3.74/1.01 % (821347)Peak memory usage: 17 MB
% 3.74/1.01 % (821347)Instructions burned: 318 (million)
% 3.74/1.01 % (821367)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=3776323775:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2995 on theBenchmark for (2995ds/31Mi)
% 3.74/1.01 % (821368)dis+1010_40_to=kbo:tgt=full:fde=unused:si=on:sp=const_frequency:lma=off:cbe=off:uwa=interpreted_only:random_seed=4071607997:i=137:kws=precedence:bd=all:rtra=on:c=on:ntd=on_2995 on theBenchmark for (2995ds/137Mi)
% 3.74/1.02 % (821358)Instruction limit reached!
% 3.74/1.02 % (821358)------------------------------
% 3.74/1.02 % (821358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.74/1.02 % (821358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.74/1.02 % (821358)CaDiCaL version: 2.1.3
% 3.74/1.02 % (821358)Termination reason: Instruction limit
% 3.74/1.02 % (821358)Termination phase: Saturation
% 3.74/1.02 % (821358)Time elapsed: 0.089 s
% 3.74/1.02 % (821358)Peak memory usage: 14 MB
% 3.74/1.02 % (821358)Instructions burned: 202 (million)
% 3.74/1.02 % (821369)dis+10_2_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_pi_sigma_gen:si=on:sp=occurrence:plsqr=5,1:bsr=on:plsql=on:random_seed=3995068264:cond=on:i=34:hud=10:nm=10:rtra=on_2995 on theBenchmark for (2995ds/34Mi)
% 3.74/1.02 % (821367)Instruction limit reached!
% 3.74/1.02 % (821367)------------------------------
% 3.74/1.02 % (821367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.74/1.02 % (821367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/1.07 % (821367)CaDiCaL version: 2.1.3
% 5.42/1.07 % (821367)Termination reason: Instruction limit
% 5.42/1.07 % (821367)Termination phase: Property scanning
% 5.42/1.07 % (821367)Time elapsed: 0.014 s
% 5.42/1.07 % (821367)Peak memory usage: 10 MB
% 5.42/1.07 % (821367)Instructions burned: 32 (million)
% 5.42/1.07 % (821370)lrs+1010_1_sil=128000:hsqc=4:si=on:sos=on:random_seed=3556423625:hsq=on:i=67:hsqaw=5:rtra=on:fe=abstraction:ntd=on_2995 on theBenchmark for (2995ds/67Mi)
% 5.42/1.07 % (821373)WARNING Broken Constraint: if sine_generality_threshold(60) has been set then sine_selection(off) is not equal to off
% 5.42/1.07 % (821373)dis+21_1_to=lpo:sil=128000:cnfonf=lazy_not_gen_be_off:si=on:sp=unary_frequency:bsr=on:random_seed=1729684764:i=180:hud=16:bd=all:fsr=off:rtra=on:sgt=60:ntd=on_2995 on theBenchmark for (2995ds/180Mi)
% 5.42/1.07 % (821369)Instruction limit reached!
% 5.42/1.07 % (821369)------------------------------
% 5.42/1.07 % (821369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.42/1.07 % (821369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/1.07 % (821369)CaDiCaL version: 2.1.3
% 5.42/1.07 % (821369)Termination reason: Instruction limit
% 5.42/1.07 % (821369)Termination phase: Property scanning
% 5.42/1.07 % (821369)Time elapsed: 0.015 s
% 5.42/1.07 % (821369)Peak memory usage: 10 MB
% 5.42/1.07 % (821369)Instructions burned: 36 (million)
% 5.42/1.07 % (821375)lrs+1002_1_sil=128000:si=on:uwa=off:random_seed=818230981:st=2:i=246:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/246Mi)
% 5.42/1.07 % (821368)Instruction limit reached!
% 5.42/1.07 % (821368)------------------------------
% 5.42/1.07 % (821368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.42/1.07 % (821368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/1.07 % (821368)CaDiCaL version: 2.1.3
% 5.42/1.07 % (821368)Termination reason: Instruction limit
% 5.42/1.07 % (821368)Termination phase: Saturation
% 5.42/1.07 % (821368)Time elapsed: 0.031 s
% 5.42/1.07 % (821368)Peak memory usage: 13 MB
% 5.42/1.07 % (821368)Instructions burned: 140 (million)
% 5.42/1.07 % (821370)Instruction limit reached!
% 5.42/1.07 % (821370)------------------------------
% 5.42/1.07 % (821370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.42/1.07 % (821370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/1.07 % (821370)CaDiCaL version: 2.1.3
% 5.42/1.07 % (821370)Termination reason: Instruction limit
% 5.42/1.07 % (821370)Termination phase: Property scanning
% 5.42/1.07 % (821370)Time elapsed: 0.028 s
% 5.42/1.07 % (821370)Peak memory usage: 11 MB
% 5.42/1.07 % (821370)Instructions burned: 68 (million)
% 5.42/1.07 % (821378)lrs+10_7_sil=128000:tgt=full:si=on:lma=off:uwa=off:nwc=1:sac=on:random_seed=1520422455:cond=on:i=96:bd=all:rtra=on_2995 on theBenchmark for (2995ds/96Mi)
% 5.42/1.07 % (821380)lrs+10_1_sil=128000:si=on:sos=on:urr=on:random_seed=3179203447:i=427:sd=1:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/427Mi)
% 5.42/1.07 % (821381)dis+1010_1_sil=128000:si=on:uwa=off:random_seed=2584814539:st=3:s2a=on:i=874:sd=3:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/874Mi)
% 5.42/1.07 % (821378)Instruction limit reached!
% 5.42/1.07 % (821378)------------------------------
% 5.42/1.07 % (821378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.42/1.07 % (821378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/1.07 % (821378)CaDiCaL version: 2.1.3
% 5.42/1.07 % (821378)Termination reason: Instruction limit
% 5.42/1.07 % (821378)Termination phase: Saturation
% 5.42/1.07 % (821378)Time elapsed: 0.040 s
% 5.42/1.07 % (821378)Peak memory usage: 13 MB
% 5.42/1.07 % (821378)Instructions burned: 96 (million)
% 5.42/1.07 % (821373)Instruction limit reached!
% 5.42/1.07 % (821373)------------------------------
% 5.42/1.07 % (821373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.42/1.07 % (821373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.42/1.07 % (821373)CaDiCaL version: 2.1.3
% 5.42/1.07 % (821373)Termination reason: Instruction limit
% 5.42/1.07 % (821373)Termination phase: Saturation
% 5.42/1.07 % (821373)Time elapsed: 0.073 s
% 5.42/1.07 % (821373)Peak memory usage: 13 MB
% 5.42/1.07 % (821373)Instructions burned: 183 (million)
% 5.42/1.07 % (821385)dis+1010_4_sas=cadical:si=on:cbe=off:nwc=20:random_seed=4036154851:st=6:s2a=on:i=515:sd=2:nm=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/515Mi)
% 5.89/1.17 % (821386)lrs+1002_1_cnfonf=lazy_pi_sigma_gen:si=on:uwa=off:random_seed=1773440617:st=1.5:i=130:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/130Mi)
% 5.89/1.17 % (821386)Instruction limit reached!
% 5.89/1.17 % (821386)------------------------------
% 5.89/1.17 % (821386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.89/1.17 % (821386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.89/1.17 % (821386)CaDiCaL version: 2.1.3
% 5.89/1.17 % (821386)Termination reason: Instruction limit
% 5.89/1.17 % (821386)Termination phase: Saturation
% 5.89/1.17 % (821386)Time elapsed: 0.029 s
% 5.89/1.17 % (821386)Peak memory usage: 12 MB
% 5.89/1.17 % (821386)Instructions burned: 134 (million)
% 5.89/1.17 % (821375)Instruction limit reached!
% 5.89/1.17 % (821375)------------------------------
% 5.89/1.17 % (821375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.89/1.17 % (821375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.89/1.17 % (821375)CaDiCaL version: 2.1.3
% 5.89/1.17 % (821375)Termination reason: Instruction limit
% 5.89/1.17 % (821375)Termination phase: Saturation
% 5.89/1.17 % (821375)Time elapsed: 0.114 s
% 5.89/1.17 % (821375)Peak memory usage: 14 MB
% 5.89/1.17 % (821375)Instructions burned: 247 (million)
% 5.89/1.17 % (821389)ott+1004_1_sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:sp=unary_frequency:cbe=off:uwa=off:nwc=1:random_seed=1934401540:i=44:ep=R:rtra=on:ntd=on_2994 on theBenchmark for (2994ds/44Mi)
% 5.89/1.17 % (821389)Instruction limit reached!
% 5.89/1.17 % (821389)------------------------------
% 5.89/1.17 % (821389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.89/1.17 % (821389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.89/1.17 % (821389)CaDiCaL version: 2.1.3
% 5.89/1.17 % (821389)Termination reason: Instruction limit
% 5.89/1.17 % (821389)Termination phase: Property scanning
% 5.89/1.17 % (821389)Time elapsed: 0.010 s
% 5.89/1.17 % (821389)Peak memory usage: 10 MB
% 5.89/1.17 % (821389)Instructions burned: 48 (million)
% 5.89/1.17 % (821390)lrs+1010_8:1_sil=128000:fde=unused:e2e=on:si=on:sos=on:urr=on:uwa=one_side_constant:fd=off:random_seed=1760732610:s2a=on:i=571:nm=16:rtra=on_2994 on theBenchmark for (2994ds/571Mi)
% 5.89/1.17 % (821392)dis+1010_8_to=lpo:sil=128000:tgt=ground:si=on:sp=reverse_frequency:cbe=off:uwa=off:random_seed=1365090307:i=450:rtra=on:ixr=off:ntd=on_2993 on theBenchmark for (2993ds/450Mi)
% 5.89/1.17 % (821380)Instruction limit reached!
% 5.89/1.17 % (821380)------------------------------
% 5.89/1.17 % (821380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.89/1.17 % (821380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.89/1.17 % (821380)CaDiCaL version: 2.1.3
% 5.89/1.17 % (821380)Termination reason: Instruction limit
% 5.89/1.17 % (821380)Termination phase: Saturation
% 5.89/1.17 % (821380)Time elapsed: 0.206 s
% 5.89/1.17 % (821380)Peak memory usage: 15 MB
% 5.89/1.17 % (821380)Instructions burned: 428 (million)
% 5.89/1.17 % (821392)Instruction limit reached!
% 5.89/1.17 % (821392)------------------------------
% 5.89/1.17 % (821392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.89/1.17 % (821392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.89/1.17 % (821392)CaDiCaL version: 2.1.3
% 5.89/1.17 % (821392)Termination reason: Instruction limit
% 5.89/1.17 % (821392)Termination phase: Saturation
% 5.89/1.17 % (821392)Time elapsed: 0.104 s
% 5.89/1.17 % (821392)Peak memory usage: 19 MB
% 5.89/1.17 % (821392)Instructions burned: 453 (million)
% 5.89/1.17 % (821395)lrs+10_5:1_to=lpo:sil=128000:si=on:uwa=one_side_interpreted:random_seed=1135031817:cts=off:i=95:piset=pi_sigma:bd=all:rtra=on:ntd=on_2992 on theBenchmark for (2992ds/95Mi)
% 5.89/1.17 % (821396)lrs+1003_1_sil=128000:drc=off:cnfonf=lazy_pi_sigma_gen:si=on:uwa=one_side_interpreted:fd=off:rp=on:sac=on:random_seed=1397074508:s2a=on:i=65:add=on:bd=preordered:ins=10:rtra=on_2992 on theBenchmark for (2992ds/65Mi)
% 5.89/1.17 % (821396)Instruction limit reached!
% 5.89/1.17 % (821396)------------------------------
% 5.89/1.17 % (821396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.89/1.17 % (821396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.89/1.17 % (821396)CaDiCaL version: 2.1.3
% 5.89/1.17 % (821396)Termination reason: Instruction limit
% 5.89/1.17 % (821396)Termination phase: Function definition elimination
% 6.02/1.30 % (821396)Time elapsed: 0.015 s
% 6.02/1.30 % (821396)Peak memory usage: 11 MB
% 6.02/1.30 % (821396)Instructions burned: 68 (million)
% 6.02/1.30 % (821399)dis+1010_2:1_slsqr=2,1:to=lpo:plsq=on:cnfonf=lazy_pi_sigma_gen:si=on:sp=reverse_arity:acc=on:uwa=hol:fd=preordered:s2agt=16:flr=on:pe=on:slsq=on:random_seed=1621483163:uwa_fpi=on:avsq=on:s2a=on:cond=fast:i=105:s2at=1.5:aac=none:fgj=on:piset=and:hud=3:fsr=off:rtra=on:er=filter:rawr=on_2992 on theBenchmark for (2992ds/105Mi)
% 6.02/1.30 % (821349)Instruction limit reached!
% 6.02/1.30 % (821349)------------------------------
% 6.02/1.30 % (821349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.02/1.30 % (821349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.02/1.30 % (821349)CaDiCaL version: 2.1.3
% 6.02/1.30 % (821349)Termination reason: Instruction limit
% 6.02/1.30 % (821349)Termination phase: Saturation
% 6.02/1.30 % (821349)Time elapsed: 0.454 s
% 6.02/1.30 % (821349)Peak memory usage: 20 MB
% 6.02/1.30 % (821349)Instructions burned: 854 (million)
% 6.02/1.30 % (821395)Instruction limit reached!
% 6.02/1.30 % (821395)------------------------------
% 6.02/1.30 % (821395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.02/1.30 % (821395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.02/1.30 % (821395)CaDiCaL version: 2.1.3
% 6.02/1.30 % (821395)Termination reason: Instruction limit
% 6.02/1.30 % (821395)Termination phase: Saturation
% 6.02/1.30 % (821395)Time elapsed: 0.040 s
% 6.02/1.30 % (821395)Peak memory usage: 12 MB
% 6.02/1.30 % (821395)Instructions burned: 95 (million)
% 6.02/1.30 % (821385)Instruction limit reached!
% 6.02/1.30 % (821385)------------------------------
% 6.02/1.30 % (821385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.02/1.30 % (821385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.02/1.30 % (821385)CaDiCaL version: 2.1.3
% 6.02/1.30 % (821385)Termination reason: Instruction limit
% 6.02/1.30 % (821385)Termination phase: Saturation
% 6.02/1.30 % (821385)Time elapsed: 0.226 s
% 6.02/1.30 % (821385)Peak memory usage: 15 MB
% 6.02/1.30 % (821385)Instructions burned: 516 (million)
% 6.02/1.30 % (821399)Instruction limit reached!
% 6.02/1.30 % (821399)------------------------------
% 6.02/1.30 % (821399)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.02/1.30 % (821399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.02/1.30 % (821399)CaDiCaL version: 2.1.3
% 6.02/1.30 % (821399)Termination reason: Instruction limit
% 6.02/1.30 % (821399)Termination phase: Saturation
% 6.02/1.30 % (821399)Time elapsed: 0.024 s
% 6.02/1.30 % (821399)Peak memory usage: 12 MB
% 6.02/1.30 % (821399)Instructions burned: 109 (million)
% 6.02/1.30 % (821401)dis+10_4:1_sfv=off:to=kbo:fde=unused:cnfonf=off:sas=cadical:e2e=on:si=on:sp=occurrence:acc=on:uwa=off:fd=preordered:foolp=on:random_seed=3967249409:hsq=on:hsqr=16,1:s2a=on:i=5755:piset=or:nm=32:rtra=on:ss=axioms:c=on:sgt=8:rawr=on_2992 on theBenchmark for (2992ds/5755Mi)
% 6.02/1.30 % (821402)lrs+10_1_sil=128000:drc=off:si=on:fs=off:urr=on:uwa=one_side_constant:random_seed=3536044516:st=10:i=375:sd=1:bd=all:fsr=off:rtra=on:ss=axioms_2992 on theBenchmark for (2992ds/375Mi)
% 6.02/1.30 % (821327)Instruction limit reached!
% 6.02/1.30 % (821327)------------------------------
% 6.02/1.30 % (821327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.02/1.30 % (821406)dis+10_2_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_pi_sigma_gen:si=on:sp=occurrence:plsqr=5,1:bsr=on:plsql=on:random_seed=4028579455:cond=on:i=34:hud=10:nm=10:rtra=on_2992 on theBenchmark for (2992ds/34Mi)
% 6.02/1.30 % (821327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.02/1.30 % (821327)CaDiCaL version: 2.1.3
% 6.02/1.30 % (821327)Termination reason: Instruction limit
% 6.02/1.30 % (821327)Termination phase: Saturation
% 6.02/1.30 % (821327)Time elapsed: 0.599 s
% 6.02/1.30 % (821327)Peak memory usage: 19 MB
% 6.02/1.30 % (821327)Instructions burned: 1240 (million)
% 6.02/1.30 % (821403)lrs+10_1_to=lpo:sil=128000:e2e=on:si=on:random_seed=185025478:s2a=on:i=495:s2at=3:aac=none:bd=preordered:rtra=on:fe=abstraction_2992 on theBenchmark for (2992ds/495Mi)
% 6.02/1.30 % (821406)Instruction limit reached!
% 6.02/1.30 % (821406)------------------------------
% 6.02/1.30 % (821406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.02/1.30 % (821406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/1.38 % (821406)CaDiCaL version: 2.1.3
% 6.50/1.38 % (821406)Termination reason: Instruction limit
% 6.50/1.38 % (821406)Termination phase: Property scanning
% 6.50/1.38 % (821406)Time elapsed: 0.008 s
% 6.50/1.38 % (821406)Peak memory usage: 10 MB
% 6.50/1.38 % (821406)Instructions burned: 38 (million)
% 6.50/1.38 % (821410)dis+2_1_sil=128000:tgt=ground:e2e=on:si=on:sos=on:urr=on:uwa=off:nwc=2:random_seed=508371559:i=66:sd=50:kws=inv_arity:bd=preordered:nm=64:rtra=on:ss=axioms:c=on:ntd=on_2991 on theBenchmark for (2991ds/66Mi)
% 6.50/1.38 % (821408)ott+1002_4_tgt=ground:si=on:tsa=off:nwc=1:random_seed=1239940325:s2a=on:i=91:piset=or:hud=5:rtra=on:fe=abstraction_2992 on theBenchmark for (2992ds/91Mi)
% 6.50/1.38 % (821410)Instruction limit reached!
% 6.50/1.38 % (821410)------------------------------
% 6.50/1.38 % (821410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.50/1.38 % (821410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/1.38 % (821410)CaDiCaL version: 2.1.3
% 6.50/1.38 % (821410)Termination reason: Instruction limit
% 6.50/1.38 % (821410)Termination phase: Property scanning
% 6.50/1.38 % (821410)Time elapsed: 0.017 s
% 6.50/1.38 % (821410)Peak memory usage: 12 MB
% 6.50/1.38 % (821410)Instructions burned: 69 (million)
% 6.50/1.38 % (821413)ott+2_5:4_anc=none:to=lpo:si=on:lma=off:cbe=off:uwa=ground:nwc=3:random_seed=3318204957:uwa_fpi=on:i=22:add=on:doe=on:ins=1:rtra=on_2991 on theBenchmark for (2991ds/22Mi)
% 6.50/1.38 % (821413)Instruction limit reached!
% 6.50/1.38 % (821413)------------------------------
% 6.50/1.38 % (821413)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.50/1.38 % (821413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/1.38 % (821413)CaDiCaL version: 2.1.3
% 6.50/1.38 % (821413)Termination reason: Instruction limit
% 6.50/1.38 % (821413)Termination phase: Property scanning
% 6.50/1.38 % (821413)Time elapsed: 0.006 s
% 6.50/1.38 % (821413)Peak memory usage: 10 MB
% 6.50/1.38 % (821413)Instructions burned: 27 (million)
% 6.50/1.38 % (821408)Instruction limit reached!
% 6.50/1.38 % (821408)------------------------------
% 6.50/1.38 % (821408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.50/1.38 % (821408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/1.38 % (821408)CaDiCaL version: 2.1.3
% 6.50/1.38 % (821408)Termination reason: Instruction limit
% 6.50/1.38 % (821408)Termination phase: Property scanning
% 6.50/1.38 % (821408)Time elapsed: 0.039 s
% 6.50/1.38 % (821408)Peak memory usage: 12 MB
% 6.50/1.38 % (821408)Instructions burned: 92 (million)
% 6.50/1.38 % (821415)lrs+21_16_anc=none:sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:sas=cadical:si=on:plsqr=32,1:uwa=interpreted_only:foolp=on:nwc=3:random_seed=1193825944:i=338:bd=all:ins=4:rtra=on_2991 on theBenchmark for (2991ds/338Mi)
% 6.50/1.38 % (821416)lrs+10_1_sil=128000:si=on:urr=on:random_seed=4207144961:i=28:sd=1:rtra=on:ss=axioms:sgt=64_2991 on theBenchmark for (2991ds/28Mi)
% 6.50/1.38 % (821416)Instruction limit reached!
% 6.50/1.38 % (821416)------------------------------
% 6.50/1.38 % (821416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.50/1.38 % (821416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/1.38 % (821416)CaDiCaL version: 2.1.3
% 6.50/1.38 % (821416)Termination reason: Instruction limit
% 6.50/1.38 % (821416)Termination phase: Property scanning
% 6.50/1.38 % (821416)Time elapsed: 0.013 s
% 6.50/1.38 % (821416)Peak memory usage: 10 MB
% 6.50/1.38 % (821416)Instructions burned: 29 (million)
% 6.50/1.38 % (821390)Instruction limit reached!
% 6.50/1.38 % (821390)------------------------------
% 6.50/1.38 % (821390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.50/1.38 % (821390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.50/1.38 % (821390)CaDiCaL version: 2.1.3
% 6.50/1.38 % (821390)Termination reason: Instruction limit
% 6.50/1.38 % (821390)Termination phase: Saturation
% 6.50/1.38 % (821390)Time elapsed: 0.285 s
% 6.50/1.38 % (821390)Peak memory usage: 17 MB
% 6.50/1.38 % (821390)Instructions burned: 571 (million)
% 6.50/1.38 % (821419)WARNING Broken Constraint: if avatar_split_queue_ratios(1,16) has been set then avatar_split_queue(off) is equal to on
% 6.50/1.38 % (821419)lrs+1010_2:13_to=kbo:sil=128000:cnfonf=lazy_not_gen:si=on:sp=const_min:uwa=interpreted_only:random_seed=3804109225:i=137:add=off:avsqr=1,16:kws=inv_arity:bd=preordered:nm=0:rtra=on:ntd=on:rawr=on_2991 on theBenchmark for (2991ds/137Mi)
% 7.45/1.54 % (821420)dis+10_32_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=32,1:uwa=one_side_interpreted:nwc=1:random_seed=363971419:hsq=on:hsqr=1,8:i=340:hsql=off:bd=preordered:av=off:rtra=on_2991 on theBenchmark for (2991ds/340Mi)
% 7.45/1.54 % (821381)Instruction limit reached!
% 7.45/1.54 % (821381)------------------------------
% 7.45/1.54 % (821381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.45/1.54 % (821381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.54 % (821381)CaDiCaL version: 2.1.3
% 7.45/1.54 % (821381)Termination reason: Instruction limit
% 7.45/1.54 % (821381)Termination phase: Saturation
% 7.45/1.54 % (821381)Time elapsed: 0.424 s
% 7.45/1.54 % (821381)Peak memory usage: 15 MB
% 7.45/1.54 % (821381)Instructions burned: 874 (million)
% 7.45/1.54 % (821415)Instruction limit reached!
% 7.45/1.54 % (821415)------------------------------
% 7.45/1.54 % (821415)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.45/1.54 % (821415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.54 % (821415)CaDiCaL version: 2.1.3
% 7.45/1.54 % (821415)Termination reason: Instruction limit
% 7.45/1.54 % (821415)Termination phase: Saturation
% 7.45/1.54 % (821415)Time elapsed: 0.073 s
% 7.45/1.54 % (821415)Peak memory usage: 15 MB
% 7.45/1.54 % (821415)Instructions burned: 339 (million)
% 7.45/1.54 % (821424)WARNING Broken Constraint: if sine_level_split_queue_cutoffs(1) has been set then sine_level_split_queue(off) is equal to on
% 7.45/1.54 % (821424)dis+1010_1_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:plsqr=64,1:nwc=2:slsqc=1:random_seed=4248238190:i=373:hud=10:nm=16:av=off:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/373Mi)
% 7.45/1.54 % (821423)dis+1004_1_sil=128000:si=on:sos=on:uwa=one_side_interpreted:random_seed=2982554340:i=227:sd=1:bd=all:rtra=on:ss=axioms_2990 on theBenchmark for (2990ds/227Mi)
% 7.45/1.54 % (821419)Instruction limit reached!
% 7.45/1.54 % (821419)------------------------------
% 7.45/1.54 % (821419)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.45/1.54 % (821419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.54 % (821419)CaDiCaL version: 2.1.3
% 7.45/1.54 % (821419)Termination reason: Instruction limit
% 7.45/1.54 % (821419)Termination phase: Saturation
% 7.45/1.54 % (821419)Time elapsed: 0.056 s
% 7.45/1.54 % (821419)Peak memory usage: 12 MB
% 7.45/1.54 % (821419)Instructions burned: 138 (million)
% 7.45/1.54 % (821402)Instruction limit reached!
% 7.45/1.54 % (821402)------------------------------
% 7.45/1.54 % (821402)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.45/1.54 % (821402)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.54 % (821402)CaDiCaL version: 2.1.3
% 7.45/1.54 % (821402)Termination reason: Instruction limit
% 7.45/1.54 % (821402)Termination phase: Saturation
% 7.45/1.54 % (821402)Time elapsed: 0.177 s
% 7.45/1.54 % (821402)Peak memory usage: 14 MB
% 7.45/1.54 % (821402)Instructions burned: 376 (million)
% 7.45/1.54 % (821428)lrs+10_1_sil=128000:drc=off:si=on:sos=on:erd=off:urr=on:uwa=interpreted_only:random_seed=2447604398:i=575:rtra=on_2990 on theBenchmark for (2990ds/575Mi)
% 7.45/1.54 % (821427)lrs+10_64_anc=all_dependent:sil=128000:e2e=on:si=on:cbe=off:uwa=off:random_seed=4164076976:i=116:ep=RSTC:rtra=on:ntd=on_2990 on theBenchmark for (2990ds/116Mi)
% 7.45/1.54 % (821424)Instruction limit reached!
% 7.45/1.54 % (821424)------------------------------
% 7.45/1.54 % (821424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.45/1.54 % (821424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.54 % (821424)CaDiCaL version: 2.1.3
% 7.45/1.54 % (821424)Termination reason: Instruction limit
% 7.45/1.54 % (821424)Termination phase: Saturation
% 7.45/1.54 % (821424)Time elapsed: 0.089 s
% 7.45/1.54 % (821424)Peak memory usage: 13 MB
% 7.45/1.54 % (821424)Instructions burned: 377 (million)
% 7.45/1.54 % (821427)Instruction limit reached!
% 7.45/1.54 % (821427)------------------------------
% 7.45/1.54 % (821427)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.45/1.54 % (821427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.45/1.54 % (821427)CaDiCaL version: 2.1.3
% 7.45/1.54 % (821427)Termination reason: Instruction limit
% 7.45/1.54 % (821427)Termination phase: Saturation
% 8.18/1.61 % (821427)Time elapsed: 0.052 s
% 8.18/1.61 % (821427)Peak memory usage: 13 MB
% 8.18/1.61 % (821427)Instructions burned: 118 (million)
% 8.18/1.61 % (821403)Instruction limit reached!
% 8.18/1.61 % (821403)------------------------------
% 8.18/1.61 % (821403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.18/1.61 % (821403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/1.61 % (821403)CaDiCaL version: 2.1.3
% 8.18/1.61 % (821403)Termination reason: Instruction limit
% 8.18/1.61 % (821403)Termination phase: Saturation
% 8.18/1.61 % (821403)Time elapsed: 0.251 s
% 8.18/1.61 % (821403)Peak memory usage: 17 MB
% 8.18/1.61 % (821403)Instructions burned: 495 (million)
% 8.18/1.61 % (821431)dis+2_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:si=on:fdtod=off:sp=const_max:lma=off:random_seed=1324623857:cts=off:i=270:doe=on:hud=5:bs=unit_only:bd=preordered:nm=30:ins=25:rtra=on_2989 on theBenchmark for (2989ds/270Mi)
% 8.18/1.61 % (821432)dis+1002_4:1_sfv=off:to=lpo:plsq=on:fde=none:e2e=on:si=on:spb=non_intro:acc=on:uwa=off:fd=preordered:foolp=on:s2agt=32:slsqc=1:slsq=on:random_seed=565558728:hsq=on:hsqr=16,1:s2a=on:i=9840:add=on:nm=16:nicw=on:rtra=on:gtg=position:ss=included:ixr=off:c=on:inj=on:ntd=on:rawr=on_2989 on theBenchmark for (2989ds/9840Mi)
% 8.18/1.61 % (821420)Instruction limit reached!
% 8.18/1.61 % (821420)------------------------------
% 8.18/1.61 % (821420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.18/1.61 % (821420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/1.61 % (821420)CaDiCaL version: 2.1.3
% 8.18/1.61 % (821420)Termination reason: Instruction limit
% 8.18/1.61 % (821420)Termination phase: Saturation
% 8.18/1.61 % (821420)Time elapsed: 0.144 s
% 8.18/1.61 % (821420)Peak memory usage: 13 MB
% 8.18/1.61 % (821420)Instructions burned: 341 (million)
% 8.18/1.61 % (821423)Instruction limit reached!
% 8.18/1.61 % (821423)------------------------------
% 8.18/1.61 % (821423)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.18/1.61 % (821423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/1.61 % (821423)CaDiCaL version: 2.1.3
% 8.18/1.61 % (821423)Termination reason: Instruction limit
% 8.18/1.61 % (821423)Termination phase: Saturation
% 8.18/1.61 % (821423)Time elapsed: 0.110 s
% 8.18/1.61 % (821423)Peak memory usage: 14 MB
% 8.18/1.61 % (821423)Instructions burned: 228 (million)
% 8.18/1.61 % (821433)lrs+1010_1_sil=128000:si=on:sos=all:uwa=off:nwc=1:random_seed=2165412298:i=421:rtra=on:ss=axioms_2989 on theBenchmark for (2989ds/421Mi)
% 8.18/1.61 % (821436)WARNING Broken Constraint: if sine_to_age_tolerance(3) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 8.18/1.61 % (821436)lrs+10_40_sil=128000:tgt=full:cnfonf=off:si=on:sp=reverse_frequency:spb=goal_then_units:uwa=off:fd=preordered:nwc=1:random_seed=47229638:avsq=on:i=270:s2at=3:avsqr=1,16:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/270Mi)
% 8.18/1.61 % (821437)dis+1002_64_sil=128000:cnfonf=lazy_not_gen_be_off:si=on:cbe=off:uwa=off:nwc=0.5:random_seed=2083136765:i=31:kws=inv_frequency:bd=all:rtra=on:ntd=on_2989 on theBenchmark for (2989ds/31Mi)
% 8.18/1.61 % (821437)Instruction limit reached!
% 8.18/1.61 % (821437)------------------------------
% 8.18/1.61 % (821437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.18/1.61 % (821437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/1.61 % (821437)CaDiCaL version: 2.1.3
% 8.18/1.61 % (821437)Termination reason: Instruction limit
% 8.18/1.61 % (821437)Termination phase: Property scanning
% 8.18/1.61 % (821437)Time elapsed: 0.014 s
% 8.18/1.61 % (821437)Peak memory usage: 10 MB
% 8.18/1.61 % (821437)Instructions burned: 32 (million)
% 8.18/1.61 % (821436)Refutation not found, incomplete strategy
% 8.18/1.61 % (821436)------------------------------
% 8.18/1.61 % (821436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.18/1.61 % (821436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/1.61 % (821436)CaDiCaL version: 2.1.3
% 8.18/1.61 % (821436)Termination reason: Refutation not found, incomplete strategy
% 8.18/1.61 % (821436)Time elapsed: 0.037 s
% 8.18/1.61 % (821436)Peak memory usage: 14 MB
% 8.18/1.61 % (821436)Instructions burned: 156 (million)
% 8.18/1.61 % (821436)------------------------------
% 8.18/1.61 % (821436)------------------------------
% 8.18/1.61 % (821441)WARNING Broken Constraint: if ho_split_queue_ratios(1,8) has been set then ho_split_queue(off) is equal to on
% 8.18/1.61 % (821441)WARNING Broken Constraint: if sine_to_age_tolerance(5) has been set then sine_to_age(off) is equal to on or sine_to_pred_levels(off) is not equal to off or sine_level_split_queue(off) is equal to on
% 8.18/1.61 % (821441)dis+1002_8_to=kbo:sil=128000:tgt=full:drc=off:si=on:sp=const_max:lma=off:spb=non_intro:cbe=off:uwa=interpreted_only:random_seed=2247195177:hsqr=1,8:i=1440:s2at=5:add=on:nm=2:rtra=on_2989 on theBenchmark for (2989ds/1440Mi)
% 8.18/1.61 % (821442)dis+10_2_sil=128000:si=on:random_seed=287739115:s2a=on:i=339:av=off:rtra=on:fe=abstraction:ss=axioms:fsd=on:ntd=on_2988 on theBenchmark for (2988ds/339Mi)
% 8.18/1.61 % (821431)Instruction limit reached!
% 8.18/1.61 % (821431)------------------------------
% 8.18/1.61 % (821431)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.18/1.61 % (821431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/1.61 % (821431)CaDiCaL version: 2.1.3
% 8.18/1.61 % (821431)Termination reason: Instruction limit
% 8.18/1.61 % (821431)Termination phase: Saturation
% 8.18/1.61 % (821431)Time elapsed: 0.108 s
% 8.18/1.61 % (821431)Peak memory usage: 15 MB
% 8.18/1.61 % (821431)Instructions burned: 270 (million)
% 8.18/1.61 % (821445)lrs+2_16:1_si=on:cbe=off:uwa=interpreted_only:random_seed=2982379169:i=111:add=on:fgj=on:rtra=on:fdi=1024_2988 on theBenchmark for (2988ds/111Mi)
% 8.18/1.61 % (821442)Instruction limit reached!
% 8.18/1.61 % (821442)------------------------------
% 8.18/1.61 % (821442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.18/1.61 % (821442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/1.61 % (821442)CaDiCaL version: 2.1.3
% 8.18/1.61 % (821442)Termination reason: Instruction limit
% 8.18/1.61 % (821442)Termination phase: Saturation
% 8.18/1.61 % (821442)Time elapsed: 0.081 s
% 8.18/1.61 % (821442)Peak memory usage: 14 MB
% 8.18/1.61 % (821442)Instructions burned: 344 (million)
% 8.18/1.61 % (821447)dis+10_8_sil=128000:plsq=on:plsqc=1:si=on:sp=unary_first:sos=on:lma=off:plsqr=64,1:uwa=interpreted_only:foolp=on:random_seed=2958661196:st=3:avsq=on:i=122:avsqr=8,1:sd=2:kws=precedence:bd=preordered:rtra=on:ss=axioms:ntd=on_2987 on theBenchmark for (2987ds/122Mi)
% 8.18/1.61 % (821445)Instruction limit reached!
% 8.18/1.61 % (821445)------------------------------
% 8.18/1.61 % (821445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.18/1.61 % (821445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/1.61 % (821445)CaDiCaL version: 2.1.3
% 8.18/1.61 % (821445)Termination reason: Instruction limit
% 8.18/1.61 % (821445)Termination phase: Saturation
% 8.18/1.61 % (821445)Time elapsed: 0.047 s
% 8.18/1.61 % (821445)Peak memory usage: 13 MB
% 8.18/1.61 % (821445)Instructions burned: 111 (million)
% 8.18/1.61 % (821428)Instruction limit reached!
% 8.18/1.61 % (821428)------------------------------
% 8.18/1.61 % (821428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.18/1.61 % (821428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/1.61 % (821428)CaDiCaL version: 2.1.3
% 8.18/1.61 % (821428)Termination reason: Instruction limit
% 8.18/1.61 % (821428)Termination phase: Saturation
% 8.18/1.61 % (821428)Time elapsed: 0.253 s
% 8.18/1.61 % (821428)Peak memory usage: 15 MB
% 8.18/1.61 % (821428)Instructions burned: 575 (million)
% 8.18/1.61 % (821449)dis+1010_3:2_anc=all_dependent:sil=128000:si=on:sos=on:lma=off:spb=goal_then_units:bce=on:fd=off:random_seed=1344626281:uwa_fpi=on:avsq=on:i=136:avsqr=1,32:hud=15:nm=0:rtra=on:ntd=on_2987 on theBenchmark for (2987ds/136Mi)
% 8.18/1.61 % (821450)dis+1002_1_sil=128000:fde=unused:e2e=on:si=on:cbe=off:uwa=off:random_seed=2926461397:hsq=on:st=2:i=232:kws=inv_frequency:rtra=on:ss=axioms:ntd=on_2987 on theBenchmark for (2987ds/232Mi)
% 8.18/1.61 % (821433)Instruction limit reached!
% 8.18/1.61 % (821433)------------------------------
% 8.18/1.61 % (821433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.18/1.61 % (821433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/1.61 % (821433)CaDiCaL version: 2.1.3
% 8.18/1.61 % (821433)Termination reason: Instruction limit
% 8.18/1.61 % (821433)Termination phase: Saturation
% 8.18/1.61 % (821433)Time elapsed: 0.200 s
% 8.18/1.61 % (821433)Peak memory usage: 15 MB
% 8.18/1.61 % (821433)Instructions burned: 423 (million)
% 8.18/1.61 % (821447)Instruction limit reached!
% 8.18/1.61 % (821447)------------------------------
% 8.18/1.61 % (821447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.18/1.61 % (821447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/1.61 % (821447)CaDiCaL version: 2.1.3
% 8.18/1.61 % (821447)Termination reason: Instruction limit
% 8.18/1.61 % (821447)Termination phase: Saturation
% 8.18/1.61 % (821447)Time elapsed: 0.053 s
% 8.18/1.61 % (821447)Peak memory usage: 13 MB
% 8.18/1.61 % (821447)Instructions burned: 124 (million)
% 8.18/1.61 % (821453)lrs+1010_8:1_sil=128000:tgt=ground:plsq=on:plsqc=1:cnfonf=lazy_gen:si=on:sos=on:plsqr=256,1:uwa=off:random_seed=813960718:i=1254:kws=precedence:bd=preordered:av=off:rtra=on_2987 on theBenchmark for (2987ds/1254Mi)
% 8.18/1.61 % (821454)WARNING Broken Constraint: if lrs_weight_limit_only(on) has been set then saturation_algorithm(discount) is equal to lrs
% 8.18/1.61 % (821454)dis+1002_5:4_sil=128000:plsq=on:plsqc=1:cnfonf=lazy_simp:si=on:plsqr=878,253:plsql=on:uwa=interpreted_only:lwlo=on:random_seed=1574388489:s2a=on:i=281:add=on:rtra=on:fe=axiom:fdi=1024_2987 on theBenchmark for (2987ds/281Mi)
% 8.18/1.61 % (821449)Instruction limit reached!
% 8.18/1.61 % (821449)------------------------------
% 8.18/1.61 % (821449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.18/1.61 % (821449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/1.61 % (821449)CaDiCaL version: 2.1.3
% 8.18/1.61 % (821449)Termination reason: Instruction limit
% 8.18/1.61 % (821449)Termination phase: Saturation
% 8.18/1.61 % (821449)Time elapsed: 0.061 s
% 8.18/1.61 % (821449)Peak memory usage: 14 MB
% 8.18/1.61 % (821449)Instructions burned: 137 (million)
% 8.18/1.61 % (821457)dis+1010_1_to=lpo:sil=128000:cnfonf=lazy_pi_sigma_gen:sas=cadical:si=on:sos=all:uwa=off:sac=on:random_seed=1259860538:i=619:add=on:rtra=on_2986 on theBenchmark for (2986ds/619Mi)
% 8.18/1.61 % (821432) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-821262-821432"...
% 8.18/1.61 % (821432)...printing done.
% 8.18/1.61 % (821432)Refutation found. Thanks to Tanya!
% 8.18/1.61 % SZS status Theorem for theBenchmark
% 8.18/1.61 % SZS output start Proof for theBenchmark
% See solution above
% 8.18/1.62 % (821432)------------------------------
% 8.18/1.62 % (821432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.18/1.62 % (821432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.18/1.62 % (821432)CaDiCaL version: 2.1.3
% 8.18/1.62 % (821432)Termination reason: Refutation
% 8.18/1.62 % (821432)Time elapsed: 0.285 s
% 8.18/1.62 % (821432)Peak memory usage: 20 MB
% 8.18/1.62 % (821432)Instructions burned: 704 (million)
% 8.18/1.62 % (821262)Success in time 1.344 s
% 8.18/1.62 % Vampire exiting
%------------------------------------------------------------------------------