%------------------------------------------------------------------------------
% File : iProver-SAT---3.9.4
% Problem : SYO581+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p SAT
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:53:14 PM UTC 2026
% Result : CounterSatisfiable 1.33s 1.18s
% Output : Model 3.74s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
%------ Positive definition of k04_buttercup10048
fof(lit_def,axiom,
! [X0] :
( k04_buttercup10048(X0)
<=> ( X0 = sK513
| X0 = sK511
| X0 = sK326
| X0 = sK306
| X0 = sK185
| X0 = sK184 ) ) ).
%------ Positive definition of k04_buttercup10049
fof(lit_def_001,axiom,
! [X0] :
( k04_buttercup10049(X0)
<=> ( X0 = sK511
| X0 = sK184 ) ) ).
%------ Positive definition of k04_buttercup10051
fof(lit_def_002,axiom,
! [X0] :
( k04_buttercup10051(X0)
<=> ( X0 = sK513
| X0 = sK306 ) ) ).
%------ Positive definition of k04_buttercup10095
fof(lit_def_003,axiom,
! [X0] :
( k04_buttercup10095(X0)
<=> ( X0 = sK421
| X0 = sK379
| X0 = sK282
| X0 = sK247
| X0 = sK246
| X0 = sK154
| X0 = sK125 ) ) ).
%------ Positive definition of k04_buttercup10096
fof(lit_def_004,axiom,
! [X0] :
( k04_buttercup10096(X0)
<=> ( X0 = sK421
| X0 = sK246 ) ) ).
%------ Positive definition of k04_buttercup10097
fof(lit_def_005,axiom,
! [X0] :
( k04_buttercup10097(X0)
<=> ( X0 = sK379
| X0 = sK247 ) ) ).
%------ Positive definition of k04_buttercup10337
fof(lit_def_006,axiom,
! [X0] :
( k04_buttercup10337(X0)
<=> ( X0 = sK529
| X0 = sK497
| X0 = sK496
| X0 = sK492
| X0 = sK462
| X0 = sK419
| X0 = sK351
| X0 = sK315
| X0 = sK314
| X0 = sK295
| X0 = sK275
| X0 = sK158
| X0 = sK139
| X0 = sK88
| X0 = sK87
| X0 = sK85 ) ) ).
%------ Positive definition of k04_buttercup10342
fof(lit_def_007,axiom,
! [X0] :
( k04_buttercup10342(X0)
<=> ( X0 = sK419
| X0 = sK295 ) ) ).
%------ Positive definition of k04_buttercup10347
fof(lit_def_008,axiom,
! [X0] :
( k04_buttercup10347(X0)
<=> ( X0 = sK529
| X0 = sK497
| X0 = sK496
| X0 = sK492
| X0 = sK315
| X0 = sK158
| X0 = sK139
| X0 = sK88
| X0 = sK87 ) ) ).
%------ Positive definition of k04_buttercup10351
fof(lit_def_009,axiom,
! [X0] :
( k04_buttercup10351(X0)
<=> ( X0 = sK351
| X0 = sK314 ) ) ).
%------ Positive definition of k04_buttercup10449
fof(lit_def_010,axiom,
! [X0] :
( k04_buttercup10449(X0)
<=> ( X0 = sK523
| X0 = sK503
| X0 = sK478
| X0 = sK391
| X0 = sK390
| X0 = sK389
| X0 = sK388
| X0 = sK337
| X0 = sK310
| X0 = sK272
| X0 = sK252
| X0 = sK225
| X0 = sK224
| X0 = sK108
| X0 = sK103
| X0 = sK35
| X0 = sK34
| X0 = sK33
| X0 = sK32
| X0 = sK31
| X0 = sK30 ) ) ).
%------ Positive definition of k04_buttercup10453
fof(lit_def_011,axiom,
! [X0] :
( k04_buttercup10453(X0)
<=> ( X0 = sK523
| X0 = sK310 ) ) ).
%------ Positive definition of k04_buttercup10462
fof(lit_def_012,axiom,
! [X0] :
( k04_buttercup10462(X0)
<=> ( X0 = sK388
| X0 = sK224 ) ) ).
%------ Positive definition of k04_buttercup10464
fof(lit_def_013,axiom,
! [X0] :
( k04_buttercup10464(X0)
<=> ( X0 = sK503
| X0 = sK478
| X0 = sK391
| X0 = sK390
| X0 = sK389
| X0 = sK225
| X0 = sK103
| X0 = sK35
| X0 = sK34
| X0 = sK33
| X0 = sK32
| X0 = sK31
| X0 = sK30 ) ) ).
%------ Positive definition of k04_buttercup10477
fof(lit_def_014,axiom,
! [X0] :
( k04_buttercup10477(X0)
<=> ( X0 = sK533
| X0 = sK435
| X0 = sK398
| X0 = sK375
| X0 = sK358
| X0 = sK355
| X0 = sK260
| X0 = sK213
| X0 = sK202
| X0 = sK124
| X0 = sK123
| X0 = sK47
| X0 = sK46 ) ) ).
%------ Positive definition of k04_buttercup10482
fof(lit_def_015,axiom,
! [X0] :
( k04_buttercup10482(X0)
<=> ( X0 = sK533
| X0 = sK260 ) ) ).
%------ Positive definition of k04_buttercup10486
fof(lit_def_016,axiom,
! [X0] :
( k04_buttercup10486(X0)
<=> ( X0 = sK435
| X0 = sK398
| X0 = sK375
| X0 = sK355
| X0 = sK213
| X0 = sK124
| X0 = sK123
| X0 = sK47
| X0 = sK46 ) ) ).
%------ Positive definition of k04_buttercup10544
fof(lit_def_017,axiom,
! [X0] :
( k04_buttercup10544(X0)
<=> ( X0 = sK467
| X0 = sK466
| X0 = sK464
| X0 = sK279
| X0 = sK278
| X0 = sK277 ) ) ).
%------ Positive definition of k04_buttercup10546
fof(lit_def_018,axiom,
! [X0] :
( k04_buttercup10546(X0)
<=> ( X0 = sK466
| X0 = sK278 ) ) ).
%------ Positive definition of k04_buttercup10547
fof(lit_def_019,axiom,
! [X0] :
( k04_buttercup10547(X0)
<=> ( X0 = sK467
| X0 = sK279 ) ) ).
%------ Positive definition of k04_buttercup10404
fof(lit_def_020,axiom,
! [X0] :
( k04_buttercup10404(X0)
<=> ( X0 = sK452
| X0 = sK448
| X0 = sK429
| X0 = sK267
| X0 = sK266
| X0 = sK264 ) ) ).
%------ Positive definition of k04_buttercup10406
fof(lit_def_021,axiom,
! [X0] :
( k04_buttercup10406(X0)
<=> ( X0 = sK448
| X0 = sK267 ) ) ).
%------ Positive definition of k04_buttercup10408
fof(lit_def_022,axiom,
! [X0] :
( k04_buttercup10408(X0)
<=> ( X0 = sK429
| X0 = sK264 ) ) ).
%------ Positive definition of k04_buttercup10593
fof(lit_def_023,axiom,
! [X0] :
( k04_buttercup10593(X0)
<=> ( X0 = sK420
| X0 = sK402
| X0 = sK363
| X0 = sK242
| X0 = sK228
| X0 = sK227 ) ) ).
%------ Positive definition of k04_buttercup10599
fof(lit_def_024,axiom,
! [X0] :
( k04_buttercup10599(X0)
<=> ( X0 = sK402
| X0 = sK227 ) ) ).
%------ Positive definition of k04_buttercup10602
fof(lit_def_025,axiom,
! [X0] :
( k04_buttercup10602(X0)
<=> ( X0 = sK420
| X0 = sK242 ) ) ).
%------ Positive definition of k04_buttercup10234
fof(lit_def_026,axiom,
! [X0] :
( k04_buttercup10234(X0)
<=> ( X0 = sK465
| X0 = sK281
| X0 = sK208
| X0 = sK201 ) ) ).
%------ Positive definition of k04_buttercup10236
fof(lit_def_027,axiom,
! [X0] :
( k04_buttercup10236(X0)
<=> X0 = sK201 ) ).
%------ Positive definition of k04_buttercup10238
fof(lit_def_028,axiom,
! [X0] :
( k04_buttercup10238(X0)
<=> X0 = sK281 ) ).
%------ Positive definition of k04_buttercup10369
fof(lit_def_029,axiom,
! [X0] :
( k04_buttercup10369(X0)
<=> ( X0 = sK365
| X0 = sK362
| X0 = sK360
| X0 = sK343
| X0 = sK209
| X0 = sK207
| X0 = sK205
| X0 = sK188 ) ) ).
%------ Positive definition of k04_buttercup10371
fof(lit_def_030,axiom,
! [X0] :
( k04_buttercup10371(X0)
<=> ( X0 = sK365
| X0 = sK209 ) ) ).
%------ Positive definition of k04_buttercup10373
fof(lit_def_031,axiom,
! [X0] :
( k04_buttercup10373(X0)
<=> ( X0 = sK360
| X0 = sK207 ) ) ).
%------ Positive definition of k04_buttercup10376
fof(lit_def_032,axiom,
! [X0] :
( k04_buttercup10376(X0)
<=> ( X0 = sK362
| X0 = sK205 ) ) ).
%------ Positive definition of k04_buttercup10293
fof(lit_def_033,axiom,
! [X0] :
( k04_buttercup10293(X0)
<=> ( X0 = sK501
| X0 = sK499
| X0 = sK413
| X0 = sK300
| X0 = sK298
| X0 = sK297 ) ) ).
%------ Positive definition of k04_buttercup10296
fof(lit_def_034,axiom,
! [X0] :
( k04_buttercup10296(X0)
<=> ( X0 = sK499
| X0 = sK297 ) ) ).
%------ Positive definition of k04_buttercup10298
fof(lit_def_035,axiom,
! [X0] :
( k04_buttercup10298(X0)
<=> ( X0 = sK413
| X0 = sK300 ) ) ).
%------ Positive definition of k04_buttercup10635
fof(lit_def_036,axiom,
! [X0] :
( k04_buttercup10635(X0)
<=> ( X0 = sK510
| X0 = sK476
| X0 = sK342
| X0 = sK336
| X0 = sK303
| X0 = sK233
| X0 = sK195
| X0 = sK189 ) ) ).
%------ Positive definition of k04_buttercup10637
fof(lit_def_037,axiom,
! [X0] :
( k04_buttercup10637(X0)
<=> ( X0 = sK476
| X0 = sK233 ) ) ).
%------ Positive definition of k04_buttercup10639
fof(lit_def_038,axiom,
! [X0] :
( k04_buttercup10639(X0)
<=> ( X0 = sK342
| X0 = sK195 ) ) ).
%------ Positive definition of k04_buttercup10641
fof(lit_def_039,axiom,
! [X0] :
( k04_buttercup10641(X0)
<=> ( X0 = sK510
| X0 = sK303 ) ) ).
%------ Positive definition of k04_buttercup10026
fof(lit_def_040,axiom,
! [X0] :
( k04_buttercup10026(X0)
<=> ( X0 = sK456
| X0 = sK454
| X0 = sK285
| X0 = sK284
| X0 = sK270 ) ) ).
%------ Positive definition of k04_buttercup10028
fof(lit_def_041,axiom,
! [X0] :
( k04_buttercup10028(X0)
<=> ( X0 = sK454
| X0 = sK285 ) ) ).
%------ Positive definition of k04_buttercup10033
fof(lit_def_042,axiom,
! [X0] :
( k04_buttercup10033(X0)
<=> ( X0 = sK456
| X0 = sK270 ) ) ).
%------ Positive definition of k04_buttercup10424
fof(lit_def_043,axiom,
! [X0] :
( k04_buttercup10424(X0)
<=> ( X0 = sK292
| X0 = sK291 ) ) ).
%------ Positive definition of k04_buttercup10425
fof(lit_def_044,axiom,
! [X0] :
( k04_buttercup10425(X0)
<=> X0 = sK291 ) ).
%------ Positive definition of k04_buttercup10204
fof(lit_def_045,axiom,
! [X0] :
( k04_buttercup10204(X0)
<=> ( X0 = sK517
| X0 = sK516
| X0 = sK489
| X0 = sK309
| X0 = sK305
| X0 = sK230
| X0 = sK187 ) ) ).
%------ Positive definition of k04_buttercup10206
fof(lit_def_046,axiom,
! [X0] :
( k04_buttercup10206(X0)
<=> ( X0 = sK489
| X0 = sK230 ) ) ).
%------ Positive definition of k04_buttercup10213
fof(lit_def_047,axiom,
! [X0] :
( k04_buttercup10213(X0)
<=> ( X0 = sK517
| X0 = sK309 ) ) ).
%------ Positive definition of k04_buttercup10219
fof(lit_def_048,axiom,
! [X0] :
( k04_buttercup10219(X0)
<=> ( X0 = sK516
| X0 = sK305 ) ) ).
%------ Positive definition of k04_buttercup10057
fof(lit_def_049,axiom,
! [X0] :
( k04_buttercup10057(X0)
<=> ( X0 = sK518
| X0 = sK509
| X0 = sK378
| X0 = sK376
| X0 = sK356
| X0 = sK353
| X0 = sK352
| X0 = sK302
| X0 = sK269
| X0 = sK219
| X0 = sK218
| X0 = sK200
| X0 = sK90
| X0 = sK89
| X0 = sK86 ) ) ).
%------ Positive definition of k04_buttercup10061
fof(lit_def_050,axiom,
! [X0] :
( k04_buttercup10061(X0)
<=> ( X0 = sK518
| X0 = sK219 ) ) ).
%------ Positive definition of k04_buttercup10064
fof(lit_def_051,axiom,
! [X0] :
( k04_buttercup10064(X0)
<=> ( X0 = sK376
| X0 = sK356
| X0 = sK352
| X0 = sK218
| X0 = sK90
| X0 = sK89
| X0 = sK86 ) ) ).
%------ Positive definition of k04_buttercup10067
fof(lit_def_052,axiom,
! [X0] :
( k04_buttercup10067(X0)
<=> ( X0 = sK378
| X0 = sK269 ) ) ).
%------ Positive definition of k04_buttercup10074
fof(lit_def_053,axiom,
! [X0] :
( k04_buttercup10074(X0)
<=> ( X0 = sK353
| X0 = sK200 ) ) ).
%------ Positive definition of k04_buttercup10555
fof(lit_def_054,axiom,
! [X0] :
( k04_buttercup10555(X0)
<=> ( X0 = sK487
| X0 = sK425
| X0 = sK423
| X0 = sK288
| X0 = sK287 ) ) ).
%------ Positive definition of k04_buttercup10559
fof(lit_def_055,axiom,
! [X0] :
( k04_buttercup10559(X0)
<=> ( X0 = sK423
| X0 = sK287 ) ) ).
%------ Positive definition of k04_buttercup10619
fof(lit_def_056,axiom,
! [X0] :
( k04_buttercup10619(X0)
<=> ( X0 = sK507
| X0 = sK483
| X0 = sK482
| X0 = sK480
| X0 = sK479
| X0 = sK296
| X0 = sK229
| X0 = sK210
| X0 = sK122
| X0 = sK121
| X0 = sK120
| X0 = sK51 ) ) ).
%------ Positive definition of k04_buttercup10620
fof(lit_def_057,axiom,
! [X0] :
( k04_buttercup10620(X0)
<=> ( X0 = sK482
| X0 = sK296 ) ) ).
%------ Positive definition of k04_buttercup10622
fof(lit_def_058,axiom,
! [X0] :
( k04_buttercup10622(X0)
<=> ( X0 = sK507
| X0 = sK483
| X0 = sK480
| X0 = sK479
| X0 = sK210
| X0 = sK122
| X0 = sK121
| X0 = sK120
| X0 = sK51 ) ) ).
%------ Positive definition of k04_buttercup10504
fof(lit_def_059,axiom,
! [X0] :
( k04_buttercup10504(X0)
<=> ( X0 = sK318
| X0 = sK199
| X0 = sK198 ) ) ).
%------ Positive definition of k04_buttercup10506
fof(lit_def_060,axiom,
! [X0] :
( k04_buttercup10506(X0)
<=> ( X0 = sK318
| X0 = sK199 ) ) ).
%------ Positive definition of k04_buttercup10139
fof(lit_def_061,axiom,
! [X0] :
( k04_buttercup10139(X0)
<=> ( X0 = sK445
| X0 = sK215
| X0 = sK193
| X0 = sK106 ) ) ).
%------ Positive definition of k04_buttercup10142
fof(lit_def_062,axiom,
! [X0] :
( k04_buttercup10142(X0)
<=> ( X0 = sK445
| X0 = sK215 ) ) ).
%------ Positive definition of k04_buttercup10516
fof(lit_def_063,axiom,
! [X0] :
( k04_buttercup10516(X0)
<=> ( X0 = sK515
| X0 = sK486
| X0 = sK444
| X0 = sK387
| X0 = sK385
| X0 = sK344
| X0 = sK223
| X0 = sK222
| X0 = sK91 ) ) ).
%------ Positive definition of k04_buttercup10517
fof(lit_def_064,axiom,
! [X0] :
( k04_buttercup10517(X0)
<=> ( X0 = sK344
| X0 = sK222 ) ) ).
%------ Positive definition of k04_buttercup10012
fof(lit_def_065,axiom,
! [X0] :
( k04_buttercup10012(X0)
<=> ( X0 = sK533
| X0 = sK530
| X0 = sK528
| X0 = sK523
| X0 = sK518
| X0 = sK517
| X0 = sK516
| X0 = sK513
| X0 = sK511
| X0 = sK510
| X0 = sK509
| X0 = sK508
| X0 = sK507
| X0 = sK503
| X0 = sK501
| X0 = sK499
| X0 = sK489
| X0 = sK488
| X0 = sK487
| X0 = sK483
| X0 = sK482
| X0 = sK481
| X0 = sK480
| X0 = sK479
| X0 = sK478
| X0 = sK477
| X0 = sK476
| X0 = sK472
| X0 = sK470
| X0 = sK468
| X0 = sK467
| X0 = sK466
| X0 = sK465
| X0 = sK464
| X0 = sK456
| X0 = sK455
| X0 = sK454
| X0 = sK453
| X0 = sK452
| X0 = sK451
| X0 = sK449
| X0 = sK448
| X0 = sK447
| X0 = sK441
| X0 = sK439
| X0 = sK438
| X0 = sK437
| X0 = sK435
| X0 = sK434
| X0 = sK432
| X0 = sK430
| X0 = sK429
| X0 = sK428
| X0 = sK425
| X0 = sK423
| X0 = sK420
| X0 = sK417
| X0 = sK416
| X0 = sK415
| X0 = sK414
| X0 = sK413
| X0 = sK412
| X0 = sK404
| X0 = sK402
| X0 = sK398
| X0 = sK396
| X0 = sK394
| X0 = sK391
| X0 = sK390
| X0 = sK389
| X0 = sK388
| X0 = sK383
| X0 = sK380
| X0 = sK378
| X0 = sK377
| X0 = sK376
| X0 = sK375
| X0 = sK374
| X0 = sK373
| X0 = sK372
| X0 = sK370
| X0 = sK365
| X0 = sK363
| X0 = sK362
| X0 = sK361
| X0 = sK360
| X0 = sK359
| X0 = sK358
| X0 = sK357
| X0 = sK356
| X0 = sK355
| X0 = sK354
| X0 = sK353
| X0 = sK352
| X0 = sK343
| X0 = sK342
| X0 = sK337
| X0 = sK336
| X0 = sK334
| X0 = sK329
| X0 = sK328
| X0 = sK326
| X0 = sK319
| X0 = sK318
| X0 = sK313
| X0 = sK310
| X0 = sK309
| X0 = sK308
| X0 = sK306
| X0 = sK305
| X0 = sK304
| X0 = sK303
| X0 = sK302
| X0 = sK301
| X0 = sK300
| X0 = sK298
| X0 = sK297
| X0 = sK296
| X0 = sK294
| X0 = sK292
| X0 = sK291
| X0 = sK290
| X0 = sK289
| X0 = sK288
| X0 = sK287
| X0 = sK285
| X0 = sK284
| X0 = sK283
| X0 = sK281
| X0 = sK280
| X0 = sK279
| X0 = sK278
| X0 = sK277
| X0 = sK274
| X0 = sK272
| X0 = sK271
| X0 = sK270
| X0 = sK269
| X0 = sK268
| X0 = sK267
| X0 = sK266
| X0 = sK265
| X0 = sK264
| X0 = sK263
| X0 = sK262
| X0 = sK261
| X0 = sK260
| X0 = sK259
| X0 = sK258
| X0 = sK254
| X0 = sK253
| X0 = sK252
| X0 = sK250
| X0 = sK249
| X0 = sK245
| X0 = sK243
| X0 = sK242
| X0 = sK240
| X0 = sK239
| X0 = sK238
| X0 = sK237
| X0 = sK235
| X0 = sK234
| X0 = sK233
| X0 = sK231
| X0 = sK230
| X0 = sK229
| X0 = sK228
| X0 = sK227
| X0 = sK225
| X0 = sK224
| X0 = sK221
| X0 = sK220
| X0 = sK219
| X0 = sK218
| X0 = sK217
| X0 = sK216
| X0 = sK214
| X0 = sK213
| X0 = sK212
| X0 = sK211
| X0 = sK210
| X0 = sK209
| X0 = sK208
| X0 = sK207
| X0 = sK206
| X0 = sK205
| X0 = sK204
| X0 = sK203
| X0 = sK202
| X0 = sK201
| X0 = sK200
| X0 = sK199
| X0 = sK198
| X0 = sK196
| X0 = sK195
| X0 = sK191
| X0 = sK190
| X0 = sK189
| X0 = sK188
| X0 = sK187
| X0 = sK186
| X0 = sK185
| X0 = sK184
| X0 = sK183
| X0 = sK181
| X0 = sK176
| X0 = sK174
| X0 = sK124
| X0 = sK123
| X0 = sK122
| X0 = sK121
| X0 = sK120
| X0 = sK108
| X0 = sK103
| X0 = sK90
| X0 = sK89
| X0 = sK86
| X0 = sK51
| X0 = sK47
| X0 = sK46
| X0 = sK35
| X0 = sK34
| X0 = sK33
| X0 = sK32
| X0 = sK31
| X0 = sK30
| X0 != sK110 ) ) ).
%------ Positive definition of k04_buttercup10184
fof(lit_def_066,axiom,
! [X0] :
( k04_buttercup10184(X0)
<=> X0 = sK176 ) ).
%------ Positive definition of k04_buttercup10190
fof(lit_def_067,axiom,
! [X0] :
( k04_buttercup10190(X0)
<=> ( X0 = sK526
| X0 = sK524
| X0 = sK522
| X0 = sK498
| X0 = sK311
| X0 = sK157
| X0 = sK50
| X0 = sK49 ) ) ).
%------ Positive definition of k04_buttercup10200
fof(lit_def_068,axiom,
! [X0] :
( k04_buttercup10200(X0)
<=> ( X0 = sK528
| X0 = sK183 ) ) ).
%------ Positive definition of k04_buttercup10221
fof(lit_def_069,axiom,
! [X0] :
( k04_buttercup10221(X0)
<=> ( X0 = sK374
| X0 = sK290 ) ) ).
%------ Positive definition of k04_buttercup10225
fof(lit_def_070,axiom,
! [X0] :
( k04_buttercup10225(X0)
<=> ( X0 = sK525
| X0 = sK494
| X0 = sK293
| X0 = sK29
| X0 = sK28 ) ) ).
%------ Positive definition of k04_buttercup10244
fof(lit_def_071,axiom,
! [X0] :
( k04_buttercup10244(X0)
<=> ( X0 = sK447
| X0 = sK263 ) ) ).
%------ Positive definition of k04_buttercup10252
fof(lit_def_072,axiom,
! [X0] :
( k04_buttercup10252(X0)
<=> ( X0 = sK439
| X0 = sK249 ) ) ).
%------ Positive definition of k04_buttercup10282
fof(lit_def_073,axiom,
! [X0] :
( k04_buttercup10282(X0)
<=> X0 = sK174 ) ).
%------ Positive definition of k04_buttercup10303
fof(lit_def_074,axiom,
! [X0] :
( k04_buttercup10303(X0)
<=> ( X0 = sK536
| X0 = sK534
| X0 = sK532
| X0 = sK395
| X0 = sK226
| X0 = sK145
| X0 = sK25
| X0 = sK24
| X0 != sK110 ) ) ).
%------ Positive definition of k04_buttercup10312
fof(lit_def_075,axiom,
! [X0] :
( k04_buttercup10312(X0)
<=> ( X0 = sK481
| X0 = sK245 ) ) ).
%------ Positive definition of k04_buttercup10316
fof(lit_def_076,axiom,
! [X0] :
( k04_buttercup10316(X0)
<=> ( X0 = sK440
| X0 = sK426
| X0 = sK422
| X0 = sK307
| X0 = sK138 ) ) ).
%------ Positive definition of k04_buttercup10325
fof(lit_def_077,axiom,
! [X0] :
( k04_buttercup10325(X0)
<=> ( X0 = sK441
| X0 = sK261 ) ) ).
%------ Positive definition of k04_buttercup10329
fof(lit_def_078,axiom,
! [X0] :
( k04_buttercup10329(X0)
<=> ( X0 = sK438
| X0 = sK259 ) ) ).
%------ Positive definition of k04_buttercup10333
fof(lit_def_079,axiom,
! [X0] :
( k04_buttercup10333(X0)
<=> ( X0 = sK328
| X0 = sK274 ) ) ).
%------ Positive definition of k04_buttercup10356
fof(lit_def_080,axiom,
! [X0] :
( k04_buttercup10356(X0)
<=> ( X0 = sK453
| X0 = sK313 ) ) ).
%------ Positive definition of k04_buttercup10016
fof(lit_def_081,axiom,
! [X0] :
( k04_buttercup10016(X0)
<=> ( X0 = sK474
| X0 = sK473
| X0 = sK408
| X0 = sK384
| X0 = sK236
| X0 = sK44
| X0 = sK43
| X0 = sK42 ) ) ).
%------ Positive definition of k04_buttercup10039
fof(lit_def_082,axiom,
! [X0] :
( k04_buttercup10039(X0)
<=> ( X0 = sK455
| X0 = sK271 ) ) ).
%------ Positive definition of k04_buttercup10053
fof(lit_def_083,axiom,
! [X0] :
( k04_buttercup10053(X0)
<=> ( X0 = sK477
| X0 = sK253 ) ) ).
%------ Positive definition of k04_buttercup10079
fof(lit_def_084,axiom,
! [X0] :
( k04_buttercup10079(X0)
<=> ( X0 = sK357
| X0 = sK196 ) ) ).
%------ Positive definition of k04_buttercup10084
fof(lit_def_085,axiom,
! [X0] :
( k04_buttercup10084(X0)
<=> ( X0 = sK415
| X0 = sK181 ) ) ).
%------ Positive definition of k04_buttercup10089
fof(lit_def_086,axiom,
! [X0] :
( k04_buttercup10089(X0)
<=> ( X0 = sK428
| X0 = sK265 ) ) ).
%------ Positive definition of k04_buttercup10100
fof(lit_def_087,axiom,
! [X0] :
( k04_buttercup10100(X0)
<=> ( X0 = sK506
| X0 = sK484
| X0 = sK286
| X0 = sK84
| X0 = sK78 ) ) ).
%------ Positive definition of k04_buttercup10117
fof(lit_def_088,axiom,
! [X0] :
( k04_buttercup10117(X0)
<=> ( X0 = sK504
| X0 = sK502
| X0 = sK436
| X0 = sK299
| X0 = sK159 ) ) ).
%------ Positive definition of k04_buttercup10125
fof(lit_def_089,axiom,
! [X0] :
( k04_buttercup10125(X0)
<=> ( X0 = sK437
| X0 = sK258 ) ) ).
%------ Positive definition of k04_buttercup10132
fof(lit_def_090,axiom,
! [X0] :
( k04_buttercup10132(X0)
<=> ( X0 = sK460
| X0 = sK459
| X0 = sK458
| X0 = sK273
| X0 = sK144
| X0 = sK143 ) ) ).
%------ Positive definition of k04_buttercup10135
fof(lit_def_091,axiom,
! [X0] :
( k04_buttercup10135(X0)
<=> X0 = sK272 ) ).
%------ Positive definition of k04_buttercup10147
fof(lit_def_092,axiom,
! [X0] :
( k04_buttercup10147(X0)
<=> ( X0 = sK472
| X0 = sK254 ) ) ).
%------ Positive definition of k04_buttercup10153
fof(lit_def_093,axiom,
! [X0] :
( k04_buttercup10153(X0)
<=> ( X0 = sK410
| X0 = sK409
| X0 = sK407
| X0 = sK406
| X0 = sK405
| X0 = sK345
| X0 = sK232
| X0 = sK118
| X0 = sK117
| X0 = sK116
| X0 = sK27
| X0 = sK26 ) ) ).
%------ Positive definition of k04_buttercup10164
fof(lit_def_094,axiom,
! [X0] :
( k04_buttercup10164(X0)
<=> ( X0 = sK322
| X0 = sK321
| X0 = sK320
| X0 = sK317
| X0 = sK178
| X0 = sK149
| X0 = sK148
| X0 = sK147 ) ) ).
%------ Positive definition of k04_buttercup10172
fof(lit_def_095,axiom,
! [X0] :
( k04_buttercup10172(X0)
<=> ( X0 = sK350
| X0 = sK349
| X0 = sK348
| X0 = sK197
| X0 = sK150
| X0 = sK146 ) ) ).
%------ Positive definition of k04_buttercup10181
fof(lit_def_096,axiom,
! [X0] :
( k04_buttercup10181(X0)
<=> ( X0 = sK530
| X0 = sK294 ) ) ).
%------ Positive definition of k04_buttercup10364
fof(lit_def_097,axiom,
! [X0] :
( k04_buttercup10364(X0)
<=> ( X0 = sK339
| X0 = sK332
| X0 = sK194
| X0 = sK136
| X0 = sK135
| X0 = sK133
| X0 = sK132 ) ) ).
%------ Positive definition of k04_buttercup10380
fof(lit_def_098,axiom,
! [X0] :
( k04_buttercup10380(X0)
<=> ( X0 = sK373
| X0 = sK217 ) ) ).
%------ Positive definition of k04_buttercup10382
fof(lit_def_099,axiom,
! [X0] :
( k04_buttercup10382(X0)
<=> ( X0 = sK377
| X0 = sK216 ) ) ).
%------ Positive definition of k04_buttercup10385
fof(lit_def_100,axiom,
! [X0] :
( k04_buttercup10385(X0)
<=> ( X0 = sK394
| X0 = sK220 ) ) ).
%------ Positive definition of k04_buttercup10389
fof(lit_def_101,axiom,
! [X0] :
( k04_buttercup10389(X0)
<=> ( X0 = sK380
| X0 = sK214 ) ) ).
%------ Positive definition of k04_buttercup10391
fof(lit_def_102,axiom,
! [X0] :
( k04_buttercup10391(X0)
<=> ( X0 = sK396
| X0 = sK231 ) ) ).
%------ Positive definition of k04_buttercup10397
fof(lit_def_103,axiom,
! [X0] :
( k04_buttercup10397(X0)
<=> ( X0 = sK412
| X0 = sK237 ) ) ).
%------ Positive definition of k04_buttercup10400
fof(lit_def_104,axiom,
! [X0] :
( k04_buttercup10400(X0)
<=> ( X0 = sK411
| X0 = sK346
| X0 = sK257
| X0 = sK105
| X0 = sK104 ) ) ).
%------ Positive definition of k04_buttercup10415
fof(lit_def_105,axiom,
! [X0] :
( k04_buttercup10415(X0)
<=> ( X0 = sK430
| X0 = sK250 ) ) ).
%------ Positive definition of k04_buttercup10419
fof(lit_def_106,axiom,
! [X0] :
( k04_buttercup10419(X0)
<=> ( X0 = sK495
| X0 = sK491
| X0 = sK248
| X0 = sK172
| X0 = sK171
| X0 = sK170
| X0 = sK168
| X0 = sK167
| X0 = sK161 ) ) ).
%------ Positive definition of k04_buttercup10430
fof(lit_def_107,axiom,
! [X0] :
( k04_buttercup10430(X0)
<=> ( X0 = sK488
| X0 = sK280 ) ) ).
%------ Positive definition of k04_buttercup10437
fof(lit_def_108,axiom,
! [X0] :
( k04_buttercup10437(X0)
<=> ( X0 = sK470
| X0 = sK283 ) ) ).
%------ Positive definition of k04_buttercup10445
fof(lit_def_109,axiom,
! [X0] :
( k04_buttercup10445(X0)
<=> ( X0 = sK334
| X0 = sK190 ) ) ).
%------ Positive definition of k04_buttercup10470
fof(lit_def_110,axiom,
! [X0] :
( k04_buttercup10470(X0)
<=> ( X0 = sK383
| X0 = sK203 ) ) ).
%------ Positive definition of k04_buttercup10473
fof(lit_def_111,axiom,
! [X0] :
( k04_buttercup10473(X0)
<=> ( X0 = sK359
| X0 = sK204 ) ) ).
%------ Positive definition of k04_buttercup10492
fof(lit_def_112,axiom,
! [X0] :
( k04_buttercup10492(X0)
<=> ( X0 = sK417
| X0 = sK239 ) ) ).
%------ Positive definition of k04_buttercup10495
fof(lit_def_113,axiom,
! [X0] :
( k04_buttercup10495(X0)
<=> ( X0 = sK416
| X0 = sK238 ) ) ).
%------ Positive definition of k04_buttercup10499
fof(lit_def_114,axiom,
! [X0] :
( k04_buttercup10499(X0)
<=> ( X0 = sK414
| X0 = sK243 ) ) ).
%------ Positive definition of k04_buttercup10510
fof(lit_def_115,axiom,
! [X0] :
( k04_buttercup10510(X0)
<=> ( X0 = sK354
| X0 = sK221 ) ) ).
%------ Positive definition of k04_buttercup10524
fof(lit_def_116,axiom,
! [X0] :
( k04_buttercup10524(X0)
<=> X0 = sK308 ) ).
%------ Positive definition of k04_buttercup10529
fof(lit_def_117,axiom,
! [X0] :
( k04_buttercup10529(X0)
<=> ( X0 = sK449
| X0 = sK304 ) ) ).
%------ Positive definition of k04_buttercup10535
fof(lit_def_118,axiom,
! [X0] :
( k04_buttercup10535(X0)
<=> ( X0 = sK329
| X0 = sK186 ) ) ).
%------ Positive definition of k04_buttercup10551
fof(lit_def_119,axiom,
! [X0] :
( k04_buttercup10551(X0)
<=> ( X0 = sK468
| X0 = sK289 ) ) ).
%------ Positive definition of k04_buttercup10567
fof(lit_def_120,axiom,
! [X0] :
( k04_buttercup10567(X0)
<=> ( X0 = sK531
| X0 = sK446
| X0 = sK443
| X0 = sK424
| X0 = sK241
| X0 = sK160
| X0 = sK142
| X0 = sK141 ) ) ).
%------ Positive definition of k04_buttercup10578
fof(lit_def_121,axiom,
! [X0] :
( k04_buttercup10578(X0)
<=> ( X0 = sK404
| X0 = sK268 ) ) ).
%------ Positive definition of k04_buttercup10581
fof(lit_def_122,axiom,
! [X0] :
( k04_buttercup10581(X0)
<=> ( X0 = sK451
| X0 = sK262 ) ) ).
%------ Positive definition of k04_buttercup10586
fof(lit_def_123,axiom,
! [X0] :
( k04_buttercup10586(X0)
<=> ( X0 = sK372
| X0 = sK211 ) ) ).
%------ Positive definition of k04_buttercup10608
fof(lit_def_124,axiom,
! [X0] :
( k04_buttercup10608(X0)
<=> ( X0 = sK434
| X0 = sK240 ) ) ).
%------ Positive definition of k04_buttercup10611
fof(lit_def_125,axiom,
! [X0] :
( k04_buttercup10611(X0)
<=> ( X0 = sK432
| X0 = sK235 ) ) ).
%------ Positive definition of k04_buttercup10626
fof(lit_def_126,axiom,
! [X0] :
( k04_buttercup10626(X0)
<=> ( X0 = sK361
| X0 = sK206 ) ) ).
%------ Positive definition of k04_buttercup10628
fof(lit_def_127,axiom,
! [X0] :
( k04_buttercup10628(X0)
<=> ( X0 = sK319
| X0 = sK212 ) ) ).
%------ Positive definition of k04_buttercup10631
fof(lit_def_128,axiom,
! [X0] :
( k04_buttercup10631(X0)
<=> ( X0 = sK370
| X0 = sK191 ) ) ).
%------ Positive definition of k04_buttercup10643
fof(lit_def_129,axiom,
! [X0] :
( k04_buttercup10643(X0)
<=> ( X0 = sK508
| X0 = sK301 ) ) ).
%------ Positive definition of b48_buttercup10046
fof(lit_def_130,axiom,
! [X0] :
( b48_buttercup10046(X0)
<=> ( X0 = sK513
| X0 = sK511
| X0 = sK326
| X0 = sK306
| X0 = sK185
| X0 = sK184 ) ) ).
%------ Positive definition of b48_buttercup10050
fof(lit_def_131,axiom,
! [X0] :
( b48_buttercup10050(X0)
<=> ( X0 = sK513
| X0 = sK306 ) ) ).
%------ Positive definition of b48_buttercup10052
fof(lit_def_132,axiom,
! [X0] :
( b48_buttercup10052(X0)
<=> ( X0 = sK511
| X0 = sK184 ) ) ).
%------ Positive definition of b48_buttercup10300
fof(lit_def_133,axiom,
! [X0] :
( b48_buttercup10300(X0)
<=> ( X0 = sK505
| X0 != sK110 ) ) ).
%------ Positive definition of b48_buttercup10305
fof(lit_def_134,axiom,
! [X0] :
( b48_buttercup10305(X0)
<=> ( X0 = sK536
| X0 = sK397 ) ) ).
%------ Positive definition of b48_buttercup10307
fof(lit_def_135,axiom,
! [X0] :
( b48_buttercup10307(X0)
<=> X0 = sK395 ) ).
%------ Positive definition of b48_buttercup10308
fof(lit_def_136,axiom,
! [X0] :
( b48_buttercup10308(X0)
<=> X0 = sK532 ) ).
%------ Positive definition of b48_buttercup10222
fof(lit_def_137,axiom,
! [X0] :
( b48_buttercup10222(X0)
<=> ( X0 = sK525
| X0 = sK495
| X0 = sK494
| X0 = sK490
| X0 = sK293
| X0 = sK169
| X0 = sK167
| X0 = sK153
| X0 = sK29
| X0 = sK28 ) ) ).
%------ Positive definition of b48_buttercup10227
fof(lit_def_138,axiom,
! [X0] :
( b48_buttercup10227(X0)
<=> X0 = sK525 ) ).
%------ Positive definition of b48_buttercup10228
fof(lit_def_139,axiom,
! [X0] :
( b48_buttercup10228(X0)
<=> X0 = sK495 ) ).
%------ Positive definition of b48_buttercup10229
fof(lit_def_140,axiom,
! [X0] :
( b48_buttercup10229(X0)
<=> X0 = sK494 ) ).
%------ Positive definition of b48_buttercup10186
fof(lit_def_141,axiom,
! [X0] :
( b48_buttercup10186(X0)
<=> ( X0 = sK526
| X0 = sK524
| X0 = sK522
| X0 = sK498
| X0 = sK311
| X0 = sK157
| X0 = sK50
| X0 = sK49 ) ) ).
%------ Positive definition of b48_buttercup10191
fof(lit_def_142,axiom,
! [X0] :
( b48_buttercup10191(X0)
<=> X0 = sK526 ) ).
%------ Positive definition of b48_buttercup10193
fof(lit_def_143,axiom,
! [X0] :
( b48_buttercup10193(X0)
<=> X0 = sK524 ) ).
%------ Positive definition of b48_buttercup10195
fof(lit_def_144,axiom,
! [X0] :
( b48_buttercup10195(X0)
<=> X0 = sK522 ) ).
%------ Positive definition of b48_buttercup10130
fof(lit_def_145,axiom,
! [X0] :
( b48_buttercup10130(X0)
<=> ( X0 = sK460
| X0 = sK459
| X0 = sK458
| X0 = sK273
| X0 = sK144
| X0 = sK143 ) ) ).
%------ Positive definition of b48_buttercup10133
fof(lit_def_146,axiom,
! [X0] :
( b48_buttercup10133(X0)
<=> X0 = sK460 ) ).
%------ Positive definition of b48_buttercup10134
fof(lit_def_147,axiom,
! [X0] :
( b48_buttercup10134(X0)
<=> X0 = sK458 ) ).
%------ Positive definition of b48_buttercup10334
fof(lit_def_148,axiom,
! [X0] :
( b48_buttercup10334(X0)
<=> ( X0 = sK529
| X0 = sK497
| X0 = sK496
| X0 = sK492
| X0 = sK462 ) ) ).
%------ Positive definition of b48_buttercup10343
fof(lit_def_149,axiom,
! [X0] :
( b48_buttercup10343(X0)
<=> X0 = sK497 ) ).
%------ Positive definition of b48_buttercup10344
fof(lit_def_150,axiom,
! [X0] :
( b48_buttercup10344(X0)
<=> X0 = sK496 ) ).
%------ Positive definition of b48_buttercup10348
fof(lit_def_151,axiom,
! [X0] :
( b48_buttercup10348(X0)
<=> X0 = sK492 ) ).
%------ Positive definition of b48_buttercup10352
fof(lit_def_152,axiom,
! [X0] :
( b48_buttercup10352(X0)
<=> X0 = sK529 ) ).
%------ Positive definition of b48_buttercup10266
fof(lit_def_153,axiom,
! [X0] :
( b48_buttercup10266(X0)
<=> ( X0 = sK519
| X0 = sK400
| X0 = sK399 ) ) ).
%------ Positive definition of b48_buttercup10267
fof(lit_def_154,axiom,
! [X0] :
( b48_buttercup10267(X0)
<=> X0 = sK399 ) ).
%------ Positive definition of b48_buttercup10268
fof(lit_def_155,axiom,
! [X0] :
( b48_buttercup10268(X0)
<=> X0 = sK519 ) ).
%------ Positive definition of b48_buttercup10098
fof(lit_def_156,axiom,
! [X0] :
( b48_buttercup10098(X0)
<=> ( X0 = sK507
| X0 = sK506
| X0 = sK484
| X0 = sK483
| X0 = sK482
| X0 = sK480
| X0 = sK479
| X0 = sK427
| X0 = sK296
| X0 = sK286
| X0 = sK229
| X0 = sK210
| X0 = sK126
| X0 = sK122
| X0 = sK121
| X0 = sK120
| X0 = sK84
| X0 = sK78
| X0 = sK62
| X0 = sK51 ) ) ).
%------ Positive definition of b48_buttercup10102
fof(lit_def_157,axiom,
! [X0] :
( b48_buttercup10102(X0)
<=> X0 = sK479 ) ).
%------ Positive definition of b48_buttercup10104
fof(lit_def_158,axiom,
! [X0] :
( b48_buttercup10104(X0)
<=> X0 = sK480 ) ).
%------ Positive definition of b48_buttercup10107
fof(lit_def_159,axiom,
! [X0] :
( b48_buttercup10107(X0)
<=> ( X0 = sK482
| X0 = sK296 ) ) ).
%------ Positive definition of b48_buttercup10108
fof(lit_def_160,axiom,
! [X0] :
( b48_buttercup10108(X0)
<=> X0 = sK483 ) ).
%------ Positive definition of b48_buttercup10109
fof(lit_def_161,axiom,
! [X0] :
( b48_buttercup10109(X0)
<=> X0 = sK484 ) ).
%------ Positive definition of b48_buttercup10110
fof(lit_def_162,axiom,
! [X0] :
( b48_buttercup10110(X0)
<=> X0 = sK507 ) ).
%------ Positive definition of b48_buttercup10111
fof(lit_def_163,axiom,
! [X0] :
( b48_buttercup10111(X0)
<=> X0 = sK506 ) ).
%------ Positive definition of b48_buttercup10440
fof(lit_def_164,axiom,
! [X0] :
( b48_buttercup10440(X0)
<=> ( X0 = sK335
| X0 = sK333
| X0 = sK332
| X0 = sK134
| X0 = sK132 ) ) ).
%------ Positive definition of b48_buttercup10441
fof(lit_def_165,axiom,
! [X0] :
( b48_buttercup10441(X0)
<=> X0 = sK332 ) ).
%------ Positive definition of b48_buttercup10442
fof(lit_def_166,axiom,
! [X0] :
( b48_buttercup10442(X0)
<=> X0 = sK335 ) ).
%------ Positive definition of b48_buttercup10474
fof(lit_def_167,axiom,
! [X0] :
( b48_buttercup10474(X0)
<=> ( X0 = sK533
| X0 = sK435
| X0 = sK398
| X0 = sK375
| X0 = sK358
| X0 = sK355
| X0 = sK260
| X0 = sK213
| X0 = sK202
| X0 = sK124
| X0 = sK123
| X0 = sK47
| X0 = sK46 ) ) ).
%------ Positive definition of b48_buttercup10478
fof(lit_def_168,axiom,
! [X0] :
( b48_buttercup10478(X0)
<=> X0 = sK355 ) ).
%------ Positive definition of b48_buttercup10479
fof(lit_def_169,axiom,
! [X0] :
( b48_buttercup10479(X0)
<=> ( X0 = sK533
| X0 = sK260 ) ) ).
%------ Positive definition of b48_buttercup10483
fof(lit_def_170,axiom,
! [X0] :
( b48_buttercup10483(X0)
<=> X0 = sK375 ) ).
%------ Positive definition of b48_buttercup10487
fof(lit_def_171,axiom,
! [X0] :
( b48_buttercup10487(X0)
<=> X0 = sK435 ) ).
%------ Positive definition of b48_buttercup10489
fof(lit_def_172,axiom,
! [X0] :
( b48_buttercup10489(X0)
<=> X0 = sK398 ) ).
%------ Positive definition of b48_buttercup10542
fof(lit_def_173,axiom,
! [X0] :
( b48_buttercup10542(X0)
<=> ( X0 = sK467
| X0 = sK466
| X0 = sK464
| X0 = sK279
| X0 = sK278
| X0 = sK277 ) ) ).
%------ Positive definition of b48_buttercup10545
fof(lit_def_174,axiom,
! [X0] :
( b48_buttercup10545(X0)
<=> ( X0 = sK466
| X0 = sK278 ) ) ).
%------ Positive definition of b48_buttercup10548
fof(lit_def_175,axiom,
! [X0] :
( b48_buttercup10548(X0)
<=> ( X0 = sK467
| X0 = sK279 ) ) ).
%------ Positive definition of b48_buttercup10274
fof(lit_def_176,axiom,
! [X0] :
( b48_buttercup10274(X0)
<=> ( X0 = sK369
| X0 = sK368
| X0 = sK367
| X0 = sK366
| X0 = sK364 ) ) ).
%------ Positive definition of b48_buttercup10275
fof(lit_def_177,axiom,
! [X0] :
( b48_buttercup10275(X0)
<=> X0 = sK369 ) ).
%------ Positive definition of b48_buttercup10276
fof(lit_def_178,axiom,
! [X0] :
( b48_buttercup10276(X0)
<=> X0 = sK366 ) ).
%------ Positive definition of b48_buttercup10277
fof(lit_def_179,axiom,
! [X0] :
( b48_buttercup10277(X0)
<=> X0 = sK367 ) ).
%------ Positive definition of b48_buttercup10278
fof(lit_def_180,axiom,
! [X0] :
( b48_buttercup10278(X0)
<=> X0 = sK364 ) ).
%------ Positive definition of b48_buttercup10402
fof(lit_def_181,axiom,
! [X0] :
( b48_buttercup10402(X0)
<=> ( X0 = sK452
| X0 = sK448
| X0 = sK429
| X0 = sK267
| X0 = sK266
| X0 = sK264 ) ) ).
%------ Positive definition of b48_buttercup10405
fof(lit_def_182,axiom,
! [X0] :
( b48_buttercup10405(X0)
<=> ( X0 = sK448
| X0 = sK267 ) ) ).
%------ Positive definition of b48_buttercup10410
fof(lit_def_183,axiom,
! [X0] :
( b48_buttercup10410(X0)
<=> ( X0 = sK429
| X0 = sK264 ) ) ).
%------ Positive definition of b48_buttercup10161
fof(lit_def_184,axiom,
! [X0] :
( b48_buttercup10161(X0)
<=> ( X0 = sK322
| X0 = sK321
| X0 = sK320
| X0 = sK317
| X0 = sK178
| X0 = sK149
| X0 = sK148
| X0 = sK147 ) ) ).
%------ Positive definition of b48_buttercup10166
fof(lit_def_185,axiom,
! [X0] :
( b48_buttercup10166(X0)
<=> X0 = sK321 ) ).
%------ Positive definition of b48_buttercup10167
fof(lit_def_186,axiom,
! [X0] :
( b48_buttercup10167(X0)
<=> X0 = sK322 ) ).
%------ Positive definition of b48_buttercup10169
fof(lit_def_187,axiom,
! [X0] :
( b48_buttercup10169(X0)
<=> X0 = sK317 ) ).
%------ Positive definition of b48_buttercup10115
fof(lit_def_188,axiom,
! [X0] :
( b48_buttercup10115(X0)
<=> ( X0 = sK504
| X0 = sK502
| X0 = sK436
| X0 = sK299
| X0 = sK159 ) ) ).
%------ Positive definition of b48_buttercup10119
fof(lit_def_189,axiom,
! [X0] :
( b48_buttercup10119(X0)
<=> X0 = sK502 ) ).
%------ Positive definition of b48_buttercup10120
fof(lit_def_190,axiom,
! [X0] :
( b48_buttercup10120(X0)
<=> X0 = sK436 ) ).
%------ Positive definition of b48_buttercup10589
fof(lit_def_191,axiom,
! [X0] :
( b48_buttercup10589(X0)
<=> ( X0 = sK420
| X0 = sK402
| X0 = sK363
| X0 = sK242
| X0 = sK228
| X0 = sK227 ) ) ).
%------ Positive definition of b48_buttercup10596
fof(lit_def_192,axiom,
! [X0] :
( b48_buttercup10596(X0)
<=> ( X0 = sK402
| X0 = sK227 ) ) ).
%------ Positive definition of b48_buttercup10604
fof(lit_def_193,axiom,
! [X0] :
( b48_buttercup10604(X0)
<=> ( X0 = sK420
| X0 = sK242 ) ) ).
%------ Positive definition of b48_buttercup10367
fof(lit_def_194,axiom,
! [X0] :
( b48_buttercup10367(X0)
<=> ( X0 = sK365
| X0 = sK362
| X0 = sK360
| X0 = sK343
| X0 = sK209
| X0 = sK207
| X0 = sK205
| X0 = sK188 ) ) ).
%------ Positive definition of b48_buttercup10370
fof(lit_def_195,axiom,
! [X0] :
( b48_buttercup10370(X0)
<=> ( X0 = sK365
| X0 = sK209 ) ) ).
%------ Positive definition of b48_buttercup10374
fof(lit_def_196,axiom,
! [X0] :
( b48_buttercup10374(X0)
<=> ( X0 = sK362
| X0 = sK205 ) ) ).
%------ Positive definition of b48_buttercup10377
fof(lit_def_197,axiom,
! [X0] :
( b48_buttercup10377(X0)
<=> ( X0 = sK360
| X0 = sK207 ) ) ).
%------ Positive definition of b48_buttercup10291
fof(lit_def_198,axiom,
! [X0] :
( b48_buttercup10291(X0)
<=> ( X0 = sK501
| X0 = sK499
| X0 = sK413
| X0 = sK300
| X0 = sK298
| X0 = sK297 ) ) ).
%------ Positive definition of b48_buttercup10294
fof(lit_def_199,axiom,
! [X0] :
( b48_buttercup10294(X0)
<=> ( X0 = sK499
| X0 = sK297 ) ) ).
%------ Positive definition of b48_buttercup10299
fof(lit_def_200,axiom,
! [X0] :
( b48_buttercup10299(X0)
<=> ( X0 = sK413
| X0 = sK300 ) ) ).
%------ Positive definition of b48_buttercup10313
fof(lit_def_201,axiom,
! [X0] :
( b48_buttercup10313(X0)
<=> ( X0 = sK440
| X0 = sK426
| X0 = sK422
| X0 = sK307
| X0 = sK138 ) ) ).
%------ Positive definition of b48_buttercup10318
fof(lit_def_202,axiom,
! [X0] :
( b48_buttercup10318(X0)
<=> X0 = sK426 ) ).
%------ Positive definition of b48_buttercup10320
fof(lit_def_203,axiom,
! [X0] :
( b48_buttercup10320(X0)
<=> X0 = sK440 ) ).
%------ Positive definition of b48_buttercup10170
fof(lit_def_204,axiom,
! [X0] :
( b48_buttercup10170(X0)
<=> ( X0 = sK350
| X0 = sK349
| X0 = sK348
| X0 = sK197
| X0 = sK150
| X0 = sK146 ) ) ).
%------ Positive definition of b48_buttercup10173
fof(lit_def_205,axiom,
! [X0] :
( b48_buttercup10173(X0)
<=> X0 = sK349 ) ).
%------ Positive definition of b48_buttercup10174
fof(lit_def_206,axiom,
! [X0] :
( b48_buttercup10174(X0)
<=> X0 = sK350 ) ).
%------ Positive definition of b48_buttercup10632
fof(lit_def_207,axiom,
! [X0] :
( b48_buttercup10632(X0)
<=> ( X0 = sK510
| X0 = sK476
| X0 = sK342
| X0 = sK336
| X0 = sK303
| X0 = sK233
| X0 = sK195
| X0 = sK189 ) ) ).
%------ Positive definition of b48_buttercup10636
fof(lit_def_208,axiom,
! [X0] :
( b48_buttercup10636(X0)
<=> ( X0 = sK476
| X0 = sK233 ) ) ).
%------ Positive definition of b48_buttercup10638
fof(lit_def_209,axiom,
! [X0] :
( b48_buttercup10638(X0)
<=> ( X0 = sK342
| X0 = sK195 ) ) ).
%------ Positive definition of b48_buttercup10640
fof(lit_def_210,axiom,
! [X0] :
( b48_buttercup10640(X0)
<=> ( X0 = sK510
| X0 = sK303 ) ) ).
%------ Positive definition of b48_buttercup10024
fof(lit_def_211,axiom,
! [X0] :
( b48_buttercup10024(X0)
<=> ( X0 = sK477
| X0 = sK456
| X0 = sK454
| X0 = sK450
| X0 = sK285
| X0 = sK284
| X0 = sK270
| X0 = sK253
| X0 = sK140
| X0 = sK45 ) ) ).
%------ Positive definition of b48_buttercup10029
fof(lit_def_212,axiom,
! [X0] :
( b48_buttercup10029(X0)
<=> ( X0 = sK477
| X0 = sK253 ) ) ).
%------ Positive definition of b48_buttercup10031
fof(lit_def_213,axiom,
! [X0] :
( b48_buttercup10031(X0)
<=> ( X0 = sK456
| X0 = sK270 ) ) ).
%------ Positive definition of b48_buttercup10034
fof(lit_def_214,axiom,
! [X0] :
( b48_buttercup10034(X0)
<=> ( X0 = sK454
| X0 = sK285 ) ) ).
%------ Positive definition of b48_buttercup10563
fof(lit_def_215,axiom,
! [X0] :
( b48_buttercup10563(X0)
<=> ( X0 = sK531
| X0 = sK446
| X0 = sK443
| X0 = sK424
| X0 = sK241
| X0 = sK160
| X0 = sK142
| X0 = sK141 ) ) ).
%------ Positive definition of b48_buttercup10574
fof(lit_def_216,axiom,
! [X0] :
( b48_buttercup10574(X0)
<=> X0 = sK443 ) ).
%------ Positive definition of b48_buttercup10150
fof(lit_def_217,axiom,
! [X0] :
( b48_buttercup10150(X0)
<=> ( X0 = sK410
| X0 = sK409
| X0 = sK407
| X0 = sK406
| X0 = sK405
| X0 = sK345
| X0 = sK232
| X0 = sK118
| X0 = sK117
| X0 = sK116
| X0 = sK27
| X0 = sK26 ) ) ).
%------ Positive definition of b48_buttercup10154
fof(lit_def_218,axiom,
! [X0] :
( b48_buttercup10154(X0)
<=> X0 = sK407 ) ).
%------ Positive definition of b48_buttercup10156
fof(lit_def_219,axiom,
! [X0] :
( b48_buttercup10156(X0)
<=> X0 = sK406 ) ).
%------ Positive definition of b48_buttercup10158
fof(lit_def_220,axiom,
! [X0] :
( b48_buttercup10158(X0)
<=> X0 = sK410 ) ).
%------ Positive definition of b48_buttercup10159
fof(lit_def_221,axiom,
! [X0] :
( b48_buttercup10159(X0)
<=> X0 = sK409 ) ).
%------ Positive definition of b48_buttercup10160
fof(lit_def_222,axiom,
! [X0] :
( b48_buttercup10160(X0)
<=> X0 = sK345 ) ).
%------ Positive definition of b48_buttercup10201
fof(lit_def_223,axiom,
! [X0] :
( b48_buttercup10201(X0)
<=> ( X0 = sK517
| X0 = sK516
| X0 = sK489
| X0 = sK434
| X0 = sK374
| X0 = sK331
| X0 = sK309
| X0 = sK305
| X0 = sK290
| X0 = sK240
| X0 = sK230
| X0 = sK187
| X0 = sK152
| X0 = sK151
| X0 = sK48 ) ) ).
%------ Positive definition of b48_buttercup10208
fof(lit_def_224,axiom,
! [X0] :
( b48_buttercup10208(X0)
<=> ( X0 = sK374
| X0 = sK290 ) ) ).
%------ Positive definition of b48_buttercup10210
fof(lit_def_225,axiom,
! [X0] :
( b48_buttercup10210(X0)
<=> ( X0 = sK517
| X0 = sK309 ) ) ).
%------ Positive definition of b48_buttercup10214
fof(lit_def_226,axiom,
! [X0] :
( b48_buttercup10214(X0)
<=> ( X0 = sK434
| X0 = sK240 ) ) ).
%------ Positive definition of b48_buttercup10217
fof(lit_def_227,axiom,
! [X0] :
( b48_buttercup10217(X0)
<=> ( X0 = sK516
| X0 = sK305 ) ) ).
%------ Positive definition of b48_buttercup10220
fof(lit_def_228,axiom,
! [X0] :
( b48_buttercup10220(X0)
<=> ( X0 = sK489
| X0 = sK230 ) ) ).
%------ Positive definition of b48_buttercup10512
fof(lit_def_229,axiom,
! [X0] :
( b48_buttercup10512(X0)
<=> ( X0 = sK386
| X0 = sK382
| X0 = sK381 ) ) ).
%------ Positive definition of b48_buttercup10513
fof(lit_def_230,axiom,
! [X0] :
( b48_buttercup10513(X0)
<=> X0 = sK381 ) ).
%------ Positive definition of b48_buttercup10514
fof(lit_def_231,axiom,
! [X0] :
( b48_buttercup10514(X0)
<=> X0 = sK386 ) ).
%------ Positive definition of b48_buttercup10054
fof(lit_def_232,axiom,
! [X0] :
( b48_buttercup10054(X0)
<=> ( X0 = sK518
| X0 = sK509
| X0 = sK378
| X0 = sK376
| X0 = sK356
| X0 = sK353
| X0 = sK352
| X0 = sK302
| X0 = sK269
| X0 = sK219
| X0 = sK218
| X0 = sK200
| X0 = sK90
| X0 = sK89
| X0 = sK86 ) ) ).
%------ Positive definition of b48_buttercup10058
fof(lit_def_233,axiom,
! [X0] :
( b48_buttercup10058(X0)
<=> ( X0 = sK518
| X0 = sK219 ) ) ).
%------ Positive definition of b48_buttercup10065
fof(lit_def_234,axiom,
! [X0] :
( b48_buttercup10065(X0)
<=> ( X0 = sK378
| X0 = sK269 ) ) ).
%------ Positive definition of b48_buttercup10068
fof(lit_def_235,axiom,
! [X0] :
( b48_buttercup10068(X0)
<=> X0 = sK376 ) ).
%------ Positive definition of b48_buttercup10070
fof(lit_def_236,axiom,
! [X0] :
( b48_buttercup10070(X0)
<=> X0 = sK352 ) ).
%------ Positive definition of b48_buttercup10072
fof(lit_def_237,axiom,
! [X0] :
( b48_buttercup10072(X0)
<=> ( X0 = sK353
| X0 = sK200 ) ) ).
%------ Positive definition of b48_buttercup10075
fof(lit_def_238,axiom,
! [X0] :
( b48_buttercup10075(X0)
<=> X0 = sK356 ) ).
%------ Positive definition of b48_buttercup10552
fof(lit_def_239,axiom,
! [X0] :
( b48_buttercup10552(X0)
<=> ( X0 = sK487
| X0 = sK425
| X0 = sK423
| X0 = sK288
| X0 = sK287 ) ) ).
%------ Positive definition of b48_buttercup10561
fof(lit_def_240,axiom,
! [X0] :
( b48_buttercup10561(X0)
<=> X0 = sK425 ) ).
%------ Positive definition of b48_buttercup10562
fof(lit_def_241,axiom,
! [X0] :
( b48_buttercup10562(X0)
<=> ( X0 = sK423
| X0 = sK287 ) ) ).
%------ Positive definition of b48_buttercup10515
fof(lit_def_242,axiom,
! [X0] :
( b48_buttercup10515(X0)
<=> ( X0 = sK515
| X0 = sK486
| X0 = sK444
| X0 = sK387
| X0 = sK385 ) ) ).
%------ Positive definition of b48_buttercup10518
fof(lit_def_243,axiom,
! [X0] :
( b48_buttercup10518(X0)
<=> X0 = sK486 ) ).
%------ Positive definition of b48_buttercup10519
fof(lit_def_244,axiom,
! [X0] :
( b48_buttercup10519(X0)
<=> X0 = sK387 ) ).
%------ Positive definition of b48_buttercup10520
fof(lit_def_245,axiom,
! [X0] :
( b48_buttercup10520(X0)
<=> X0 = sK515 ) ).
%------ Positive definition of b48_buttercup10521
fof(lit_def_246,axiom,
! [X0] :
( b48_buttercup10521(X0)
<=> X0 = sK444 ) ).
%------ Positive definition of b48_buttercup10271
fof(lit_def_247,axiom,
! [X0] :
( b48_buttercup10271(X0)
<=> ( X0 = sK431
| X0 = sK371 ) ) ).
%------ Positive definition of b48_buttercup10273
fof(lit_def_248,axiom,
! [X0] :
( b48_buttercup10273(X0)
<=> X0 = sK371 ) ).
%------ Positive definition of b48_buttercup10007
fof(lit_def_249,axiom,
! [X0] :
( b48_buttercup10007(X0)
<=> $true ) ).
%------ Positive definition of b48_buttercup10196
fof(lit_def_250,axiom,
! [X0] :
( b48_buttercup10196(X0)
<=> X0 = sK521 ) ).
%------ Positive definition of b48_buttercup10197
fof(lit_def_251,axiom,
! [X0] :
( b48_buttercup10197(X0)
<=> X0 = sK520 ) ).
%------ Positive definition of b48_buttercup10198
fof(lit_def_252,axiom,
! [X0] :
( b48_buttercup10198(X0)
<=> X0 = sK485 ) ).
%------ Positive definition of b48_buttercup10199
fof(lit_def_253,axiom,
! [X0] :
( b48_buttercup10199(X0)
<=> ( X0 = sK528
| X0 = sK183 ) ) ).
%------ Positive definition of b48_buttercup10231
fof(lit_def_254,axiom,
! [X0] :
( b48_buttercup10231(X0)
<=> ( X0 = sK465
| X0 = sK281
| X0 = sK208
| X0 = sK201 ) ) ).
%------ Positive definition of b48_buttercup10240
fof(lit_def_255,axiom,
! [X0] :
( b48_buttercup10240(X0)
<=> ( X0 = sK447
| X0 = sK263 ) ) ).
%------ Positive definition of b48_buttercup10247
fof(lit_def_256,axiom,
! [X0] :
( b48_buttercup10247(X0)
<=> X0 = sK442 ) ).
%------ Positive definition of b48_buttercup10248
fof(lit_def_257,axiom,
! [X0] :
( b48_buttercup10248(X0)
<=> ( X0 = sK439
| X0 = sK249 ) ) ).
%------ Positive definition of b48_buttercup10269
fof(lit_def_258,axiom,
! [X0] :
( b48_buttercup10269(X0)
<=> ( X0 = sK394
| X0 = sK220 ) ) ).
%------ Positive definition of b48_buttercup10272
fof(lit_def_259,axiom,
! [X0] :
( b48_buttercup10272(X0)
<=> X0 = sK392 ) ).
%------ Positive definition of b48_buttercup10279
fof(lit_def_260,axiom,
! [X0] :
( b48_buttercup10279(X0)
<=> ( X0 = sK347
| X0 = sK174
| X0 = sK137 ) ) ).
%------ Positive definition of b48_buttercup10309
fof(lit_def_261,axiom,
! [X0] :
( b48_buttercup10309(X0)
<=> ( X0 = sK481
| X0 = sK245 ) ) ).
%------ Positive definition of b48_buttercup10322
fof(lit_def_262,axiom,
! [X0] :
( b48_buttercup10322(X0)
<=> ( X0 = sK441
| X0 = sK261 ) ) ).
%------ Positive definition of b48_buttercup10326
fof(lit_def_263,axiom,
! [X0] :
( b48_buttercup10326(X0)
<=> ( X0 = sK438
| X0 = sK259 ) ) ).
%------ Positive definition of b48_buttercup10332
fof(lit_def_264,axiom,
! [X0] :
( b48_buttercup10332(X0)
<=> ( X0 = sK328
| X0 = sK274 ) ) ).
%------ Positive definition of b48_buttercup10353
fof(lit_def_265,axiom,
! [X0] :
( b48_buttercup10353(X0)
<=> ( X0 = sK453
| X0 = sK313 ) ) ).
%------ Positive definition of b48_buttercup10362
fof(lit_def_266,axiom,
! [X0] :
( b48_buttercup10362(X0)
<=> X0 = sK339 ) ).
%------ Positive definition of b48_buttercup10013
fof(lit_def_267,axiom,
! [X0] :
( b48_buttercup10013(X0)
<=> ( X0 = sK474
| X0 = sK473
| X0 = sK408
| X0 = sK384
| X0 = sK236
| X0 = sK44
| X0 = sK43
| X0 = sK42 ) ) ).
%------ Positive definition of b48_buttercup10035
fof(lit_def_268,axiom,
! [X0] :
( b48_buttercup10035(X0)
<=> ( X0 = sK455
| X0 = sK271 ) ) ).
%------ Positive definition of b48_buttercup10076
fof(lit_def_269,axiom,
! [X0] :
( b48_buttercup10076(X0)
<=> ( X0 = sK357
| X0 = sK196 ) ) ).
%------ Positive definition of b48_buttercup10082
fof(lit_def_270,axiom,
! [X0] :
( b48_buttercup10082(X0)
<=> ( X0 = sK415
| X0 = sK181 ) ) ).
%------ Positive definition of b48_buttercup10085
fof(lit_def_271,axiom,
! [X0] :
( b48_buttercup10085(X0)
<=> ( X0 = sK445
| X0 = sK215 ) ) ).
%------ Positive definition of b48_buttercup10086
fof(lit_def_272,axiom,
! [X0] :
( b48_buttercup10086(X0)
<=> ( X0 = sK428
| X0 = sK265 ) ) ).
%------ Positive definition of b48_buttercup10092
fof(lit_def_273,axiom,
! [X0] :
( b48_buttercup10092(X0)
<=> ( X0 = sK421
| X0 = sK246 ) ) ).
%------ Positive definition of b48_buttercup10121
fof(lit_def_274,axiom,
! [X0] :
( b48_buttercup10121(X0)
<=> ( X0 = sK437
| X0 = sK258 ) ) ).
%------ Positive definition of b48_buttercup10143
fof(lit_def_275,axiom,
! [X0] :
( b48_buttercup10143(X0)
<=> ( X0 = sK472
| X0 = sK254 ) ) ).
%------ Positive definition of b48_buttercup10176
fof(lit_def_276,axiom,
! [X0] :
( b48_buttercup10176(X0)
<=> ( X0 = sK351
| X0 = sK314 ) ) ).
%------ Positive definition of b48_buttercup10180
fof(lit_def_277,axiom,
! [X0] :
( b48_buttercup10180(X0)
<=> ( X0 = sK530
| X0 = sK294 ) ) ).
%------ Positive definition of b48_buttercup10182
fof(lit_def_278,axiom,
! [X0] :
( b48_buttercup10182(X0)
<=> X0 = sK403 ) ).
%------ Positive definition of b48_buttercup10365
fof(lit_def_279,axiom,
! [X0] :
( b48_buttercup10365(X0)
<=> X0 = sK341 ) ).
%------ Positive definition of b48_buttercup10378
fof(lit_def_280,axiom,
! [X0] :
( b48_buttercup10378(X0)
<=> ( X0 = sK373
| X0 = sK217 ) ) ).
%------ Positive definition of b48_buttercup10381
fof(lit_def_281,axiom,
! [X0] :
( b48_buttercup10381(X0)
<=> ( X0 = sK379
| X0 = sK247 ) ) ).
%------ Positive definition of b48_buttercup10383
fof(lit_def_282,axiom,
! [X0] :
( b48_buttercup10383(X0)
<=> ( X0 = sK377
| X0 = sK216 ) ) ).
%------ Positive definition of b48_buttercup10386
fof(lit_def_283,axiom,
! [X0] :
( b48_buttercup10386(X0)
<=> ( X0 = sK380
| X0 = sK214 ) ) ).
%------ Positive definition of b48_buttercup10394
fof(lit_def_284,axiom,
! [X0] :
( b48_buttercup10394(X0)
<=> ( X0 = sK412
| X0 = sK237 ) ) ).
%------ Positive definition of b48_buttercup10398
fof(lit_def_285,axiom,
! [X0] :
( b48_buttercup10398(X0)
<=> X0 = sK411 ) ).
%------ Positive definition of b48_buttercup10411
fof(lit_def_286,axiom,
! [X0] :
( b48_buttercup10411(X0)
<=> ( X0 = sK430
| X0 = sK250 ) ) ).
%------ Positive definition of b48_buttercup10417
fof(lit_def_287,axiom,
! [X0] :
( b48_buttercup10417(X0)
<=> ( X0 = sK515
| X0 = sK486
| X0 = sK471
| X0 = sK444
| X0 = sK387
| X0 = sK385
| X0 = sK344
| X0 = sK223
| X0 = sK222
| X0 = sK173
| X0 = sK171
| X0 = sK92
| X0 = sK91 ) ) ).
%------ Positive definition of b48_buttercup10420
fof(lit_def_288,axiom,
! [X0] :
( b48_buttercup10420(X0)
<=> X0 = sK493 ) ).
%------ Positive definition of b48_buttercup10427
fof(lit_def_289,axiom,
! [X0] :
( b48_buttercup10427(X0)
<=> ( X0 = sK488
| X0 = sK280 ) ) ).
%------ Positive definition of b48_buttercup10433
fof(lit_def_290,axiom,
! [X0] :
( b48_buttercup10433(X0)
<=> X0 = sK469 ) ).
%------ Positive definition of b48_buttercup10434
fof(lit_def_291,axiom,
! [X0] :
( b48_buttercup10434(X0)
<=> ( X0 = sK470
| X0 = sK283 ) ) ).
%------ Positive definition of b48_buttercup10443
fof(lit_def_292,axiom,
! [X0] :
( b48_buttercup10443(X0)
<=> ( X0 = sK334
| X0 = sK190 ) ) ).
%------ Positive definition of b48_buttercup10446
fof(lit_def_293,axiom,
! [X0] :
( b48_buttercup10446(X0)
<=> ( X0 = sK523
| X0 = sK503
| X0 = sK478
| X0 = sK391
| X0 = sK390
| X0 = sK389
| X0 = sK388
| X0 = sK337
| X0 = sK310
| X0 = sK272
| X0 = sK252
| X0 = sK225
| X0 = sK224
| X0 = sK108
| X0 = sK103
| X0 = sK35
| X0 = sK34
| X0 = sK33
| X0 = sK32
| X0 = sK31
| X0 = sK30 ) ) ).
%------ Positive definition of b48_buttercup10450
fof(lit_def_294,axiom,
! [X0] :
( b48_buttercup10450(X0)
<=> X0 = sK457 ) ).
%------ Positive definition of b48_buttercup10469
fof(lit_def_295,axiom,
! [X0] :
( b48_buttercup10469(X0)
<=> ( X0 = sK383
| X0 = sK203 ) ) ).
%------ Positive definition of b48_buttercup10471
fof(lit_def_296,axiom,
! [X0] :
( b48_buttercup10471(X0)
<=> ( X0 = sK359
| X0 = sK204 ) ) ).
%------ Positive definition of b48_buttercup10490
fof(lit_def_297,axiom,
! [X0] :
( b48_buttercup10490(X0)
<=> ( X0 = sK417
| X0 = sK239 ) ) ).
%------ Positive definition of b48_buttercup10493
fof(lit_def_298,axiom,
! [X0] :
( b48_buttercup10493(X0)
<=> ( X0 = sK416
| X0 = sK238 ) ) ).
%------ Positive definition of b48_buttercup10496
fof(lit_def_299,axiom,
! [X0] :
( b48_buttercup10496(X0)
<=> ( X0 = sK414
| X0 = sK243 ) ) ).
%------ Positive definition of b48_buttercup10502
fof(lit_def_300,axiom,
! [X0] :
( b48_buttercup10502(X0)
<=> ( X0 = sK318
| X0 = sK199 ) ) ).
%------ Positive definition of b48_buttercup10507
fof(lit_def_301,axiom,
! [X0] :
( b48_buttercup10507(X0)
<=> ( X0 = sK354
| X0 = sK221 ) ) ).
%------ Positive definition of b48_buttercup10522
fof(lit_def_302,axiom,
! [X0] :
( b48_buttercup10522(X0)
<=> X0 = sK514 ) ).
%------ Positive definition of b48_buttercup10526
fof(lit_def_303,axiom,
! [X0] :
( b48_buttercup10526(X0)
<=> ( X0 = sK449
| X0 = sK304 ) ) ).
%------ Positive definition of b48_buttercup10530
fof(lit_def_304,axiom,
! [X0] :
( b48_buttercup10530(X0)
<=> X0 = sK330 ) ).
%------ Positive definition of b48_buttercup10531
fof(lit_def_305,axiom,
! [X0] :
( b48_buttercup10531(X0)
<=> ( X0 = sK329
| X0 = sK186 ) ) ).
%------ Positive definition of b48_buttercup10549
fof(lit_def_306,axiom,
! [X0] :
( b48_buttercup10549(X0)
<=> ( X0 = sK468
| X0 = sK289 ) ) ).
%------ Positive definition of b48_buttercup10570
fof(lit_def_307,axiom,
! [X0] :
( b48_buttercup10570(X0)
<=> X0 = sK446 ) ).
%------ Positive definition of b48_buttercup10572
fof(lit_def_308,axiom,
! [X0] :
( b48_buttercup10572(X0)
<=> X0 = sK531 ) ).
%------ Positive definition of b48_buttercup10575
fof(lit_def_309,axiom,
! [X0] :
( b48_buttercup10575(X0)
<=> ( X0 = sK404
| X0 = sK268 ) ) ).
%------ Positive definition of b48_buttercup10579
fof(lit_def_310,axiom,
! [X0] :
( b48_buttercup10579(X0)
<=> ( X0 = sK451
| X0 = sK262 ) ) ).
%------ Positive definition of b48_buttercup10582
fof(lit_def_311,axiom,
! [X0] :
( b48_buttercup10582(X0)
<=> ( X0 = sK372
| X0 = sK211 ) ) ).
%------ Positive definition of b48_buttercup10605
fof(lit_def_312,axiom,
! [X0] :
( b48_buttercup10605(X0)
<=> ( X0 = sK419
| X0 = sK295 ) ) ).
%------ Positive definition of b48_buttercup10606
fof(lit_def_313,axiom,
! [X0] :
( b48_buttercup10606(X0)
<=> X0 = sK418 ) ).
%------ Positive definition of b48_buttercup10609
fof(lit_def_314,axiom,
! [X0] :
( b48_buttercup10609(X0)
<=> ( X0 = sK432
| X0 = sK235 ) ) ).
%------ Positive definition of b48_buttercup10612
fof(lit_def_315,axiom,
! [X0] :
( b48_buttercup10612(X0)
<=> X0 = sK393 ) ).
%------ Positive definition of b48_buttercup10616
fof(lit_def_316,axiom,
! [X0] :
( b48_buttercup10616(X0)
<=> ( X0 = sK396
| X0 = sK231 ) ) ).
%------ Positive definition of b48_buttercup10624
fof(lit_def_317,axiom,
! [X0] :
( b48_buttercup10624(X0)
<=> ( X0 = sK361
| X0 = sK206 ) ) ).
%------ Positive definition of b48_buttercup10629
fof(lit_def_318,axiom,
! [X0] :
( b48_buttercup10629(X0)
<=> ( X0 = sK370
| X0 = sK191 ) ) ).
%------ Positive definition of b48_buttercup10642
fof(lit_def_319,axiom,
! [X0] :
( b48_buttercup10642(X0)
<=> ( X0 = sK508
| X0 = sK301 ) ) ).
%------ Positive definition of b48_buttercup10646
fof(lit_def_320,axiom,
! [X0] :
( b48_buttercup10646(X0)
<=> X0 = sK512 ) ).
%------ Positive definition of b48_buttercup10465
fof(lit_def_321,axiom,
! [X0] :
( b48_buttercup10465(X0)
<=> X0 = sK391 ) ).
%------ Positive definition of b48_buttercup10466
fof(lit_def_322,axiom,
! [X0] :
( b48_buttercup10466(X0)
<=> X0 = sK390 ) ).
%------ Positive definition of b48_buttercup10467
fof(lit_def_323,axiom,
! [X0] :
( b48_buttercup10467(X0)
<=> X0 = sK389 ) ).
%------ Positive definition of b48_buttercup10456
fof(lit_def_324,axiom,
! [X0] :
( b48_buttercup10456(X0)
<=> X0 = sK478 ) ).
%------ Positive definition of b48_buttercup10458
fof(lit_def_325,axiom,
! [X0] :
( b48_buttercup10458(X0)
<=> ( X0 = sK527
| X0 = sK272
| X0 = sK107
| X0 = sK36
| X0 = sK34 ) ) ).
%------ Positive definition of sP1
fof(lit_def_326,axiom,
( sP1
<=> $false ) ).
%------ Positive definition of sP0
fof(lit_def_327,axiom,
( sP0
<=> $false ) ).
%------ Positive definition of b48_buttercup10022
fof(lit_def_328,axiom,
! [X0] :
( b48_buttercup10022(X0)
<=> X0 = sK473 ) ).
%------ Positive definition of b48_buttercup10021
fof(lit_def_329,axiom,
! [X0] :
( b48_buttercup10021(X0)
<=> X0 = sK474 ) ).
%------ Positive definition of b48_buttercup10019
fof(lit_def_330,axiom,
! [X0] :
( b48_buttercup10019(X0)
<=> X0 = sK384 ) ).
%------ Positive definition of k04_buttercup10288
fof(lit_def_331,axiom,
! [X0] :
( k04_buttercup10288(X0)
<=> ( X0 = sK500
| X0 = sK177 ) ) ).
%------ Positive definition of b48_buttercup10290
fof(lit_def_332,axiom,
! [X0] :
( b48_buttercup10290(X0)
<=> ( X0 = sK500
| X0 = sK177 ) ) ).
%------ Positive definition of sP3
fof(lit_def_333,axiom,
( sP3
<=> $false ) ).
%------ Positive definition of sP2
fof(lit_def_334,axiom,
( sP2
<=> $false ) ).
%------ Positive definition of sP5
fof(lit_def_335,axiom,
( sP5
<=> $false ) ).
%------ Positive definition of sP4
fof(lit_def_336,axiom,
( sP4
<=> $false ) ).
%------ Positive definition of sP7
fof(lit_def_337,axiom,
( sP7
<=> $false ) ).
%------ Positive definition of sP6
fof(lit_def_338,axiom,
( sP6
<=> $false ) ).
%------ Positive definition of sP9
fof(lit_def_339,axiom,
( sP9
<=> $false ) ).
%------ Positive definition of sP8
fof(lit_def_340,axiom,
( sP8
<=> $false ) ).
%------ Positive definition of sP11
fof(lit_def_341,axiom,
( sP11
<=> $false ) ).
%------ Positive definition of sP10
fof(lit_def_342,axiom,
( sP10
<=> $false ) ).
%------ Positive definition of sP13
fof(lit_def_343,axiom,
( sP13
<=> $false ) ).
%------ Positive definition of sP12
fof(lit_def_344,axiom,
( sP12
<=> $false ) ).
%------ Positive definition of k04_buttercup10357
fof(lit_def_345,axiom,
! [X0] :
( k04_buttercup10357(X0)
<=> ( X0 = sK338
| X0 = sK312 ) ) ).
%------ Positive definition of b48_buttercup10361
fof(lit_def_346,axiom,
! [X0] :
( b48_buttercup10361(X0)
<=> ( X0 = sK338
| X0 = sK312 ) ) ).
%------ Positive definition of b48_buttercup10289
fof(lit_def_347,axiom,
! [X0] :
( b48_buttercup10289(X0)
<=> ( X0 = sK319
| X0 = sK212 ) ) ).
%------ Positive definition of b48_buttercup10421
fof(lit_def_348,axiom,
! [X0] :
( b48_buttercup10421(X0)
<=> ( X0 = sK344
| X0 = sK222 ) ) ).
%------ Positive definition of sP15
fof(lit_def_349,axiom,
( sP15
<=> $false ) ).
%------ Positive definition of sP14
fof(lit_def_350,axiom,
( sP14
<=> $false ) ).
%------ Positive definition of sP17
fof(lit_def_351,axiom,
( sP17
<=> $false ) ).
%------ Positive definition of sP16
fof(lit_def_352,axiom,
( sP16
<=> $false ) ).
%------ Positive definition of b48_buttercup10454
fof(lit_def_353,axiom,
! [X0] :
( b48_buttercup10454(X0)
<=> X0 = sK503 ) ).
%------ Positive definition of b48_buttercup10460
fof(lit_def_354,axiom,
! [X0] :
( b48_buttercup10460(X0)
<=> ( X0 = sK388
| X0 = sK224 ) ) ).
%------ Positive definition of b48_buttercup10179
fof(lit_def_355,axiom,
! [X0] :
( b48_buttercup10179(X0)
<=> X0 = sK346 ) ).
%------ Positive definition of k04_buttercup10004
fof(lit_def_356,axiom,
! [X0] :
( k04_buttercup10004(X0)
<=> X0 = sK256 ) ).
%------ Positive definition of sP19
fof(lit_def_357,axiom,
( sP19
<=> $false ) ).
%------ Positive definition of sP18
fof(lit_def_358,axiom,
( sP18
<=> $false ) ).
%------ Positive definition of k04_buttercup10286
fof(lit_def_359,axiom,
! [X0] :
( k04_buttercup10286(X0)
<=> ( X0 = sK316
| X0 = sK175 ) ) ).
%------ Positive definition of b48_buttercup10283
fof(lit_def_360,axiom,
! [X0] :
( b48_buttercup10283(X0)
<=> ( X0 = sK316
| X0 = sK175 ) ) ).
%------ Positive definition of k04_buttercup10000
fof(lit_def_361,axiom,
! [X0] :
( k04_buttercup10000(X0)
<=> X0 = sK255 ) ).
%------ Positive definition of sP21
fof(lit_def_362,axiom,
( sP21
<=> $false ) ).
%------ Positive definition of sP20
fof(lit_def_363,axiom,
( sP20
<=> $false ) ).
%------ Positive definition of k04_buttercup10360
fof(lit_def_364,axiom,
! [X0] :
( k04_buttercup10360(X0)
<=> ( X0 = sK461
| X0 = sK192 ) ) ).
%------ Positive definition of b48_buttercup10359
fof(lit_def_365,axiom,
! [X0] :
( b48_buttercup10359(X0)
<=> ( X0 = sK461
| X0 = sK192 ) ) ).
%------ Positive definition of k04_buttercup10540
fof(lit_def_366,axiom,
! [X0] :
( k04_buttercup10540(X0)
<=> ( X0 = sK463
| X0 = sK276 ) ) ).
%------ Positive definition of b48_buttercup10541
fof(lit_def_367,axiom,
! [X0] :
( b48_buttercup10541(X0)
<=> ( X0 = sK463
| X0 = sK276 ) ) ).
%------ Positive definition of k04_buttercup10539
fof(lit_def_368,axiom,
! [X0] :
( k04_buttercup10539(X0)
<=> ( X0 = sK325
| X0 = sK179 ) ) ).
%------ Positive definition of b48_buttercup10538
fof(lit_def_369,axiom,
! [X0] :
( b48_buttercup10538(X0)
<=> ( X0 = sK325
| X0 = sK179 ) ) ).
%------ Positive definition of b48_buttercup10451
fof(lit_def_370,axiom,
! [X0] :
( b48_buttercup10451(X0)
<=> ( X0 = sK523
| X0 = sK310 ) ) ).
%------ Positive definition of k04_buttercup10044
fof(lit_def_371,axiom,
! [X0] :
( k04_buttercup10044(X0)
<=> ( X0 = sK327
| X0 = sK180 ) ) ).
%------ Positive definition of b48_buttercup10043
fof(lit_def_372,axiom,
! [X0] :
( b48_buttercup10043(X0)
<=> ( X0 = sK327
| X0 = sK180 ) ) ).
%------ Positive definition of k04_buttercup10042
fof(lit_def_373,axiom,
! [X0] :
( k04_buttercup10042(X0)
<=> ( X0 = sK324
| X0 = sK182 ) ) ).
%------ Positive definition of b48_buttercup10045
fof(lit_def_374,axiom,
! [X0] :
( b48_buttercup10045(X0)
<=> ( X0 = sK324
| X0 = sK182 ) ) ).
%------ Positive definition of k04_buttercup10259
fof(lit_def_375,axiom,
! [X0] :
( k04_buttercup10259(X0)
<=> ( X0 = sK401
| X0 = sK323
| X0 = sK244
| X0 = sK156
| X0 = sK155 ) ) ).
%------ Positive definition of b48_buttercup10261
fof(lit_def_376,axiom,
! [X0] :
( b48_buttercup10261(X0)
<=> X0 = sK401 ) ).
%------ Positive definition of k04_buttercup10255
fof(lit_def_377,axiom,
! [X0] :
( k04_buttercup10255(X0)
<=> ( X0 = sK475
| X0 = sK251 ) ) ).
%------ Positive definition of b48_buttercup10253
fof(lit_def_378,axiom,
! [X0] :
( b48_buttercup10253(X0)
<=> ( X0 = sK475
| X0 = sK251 ) ) ).
%------ Positive definition of b48_buttercup10260
fof(lit_def_379,axiom,
! [X0] :
( b48_buttercup10260(X0)
<=> X0 = sK323 ) ).
%------ Positive definition of b48_buttercup10422
fof(lit_def_380,axiom,
! [X0] :
( b48_buttercup10422(X0)
<=> X0 = sK491 ) ).
%------ Positive definition of sP23
fof(lit_def_381,axiom,
( sP23
<=> $false ) ).
%------ Positive definition of sP22
fof(lit_def_382,axiom,
( sP22
<=> $false ) ).
%------ Positive definition of b48_buttercup10358
fof(lit_def_383,axiom,
! [X0] :
( b48_buttercup10358(X0)
<=> X0 = sK340 ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO581+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p SAT
% 0.09/0.36 % Computer : n003.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 03:08:22 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p SAT
% 0.13/0.40 Running model finding
% 0.13/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fnt_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.41
% 0.13/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.41
% 0.13/0.41 % Detected problem language: tptp
% 0.13/0.42 % Proving...
% 1.33/1.18 % SZS status Started for theBenchmark.p
% 1.33/1.18 % SZS status CounterSatisfiable for theBenchmark.p
% 1.33/1.18
% 1.33/1.18 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 1.33/1.18
% 1.33/1.18 ------ iProver source info
% 1.33/1.18
% 1.33/1.18 git: date: 2026-07-19 20:42:38 +0200
% 1.33/1.18 git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 1.33/1.18 git: non_committed_changes: false
% 1.33/1.18
% 1.33/1.18 ------ Parsing...
% 1.33/1.18 ------ Clausification by vclausify_rel & Parsing by iProver...------ preprocesses with Option_epr_non_horn_non_eq
% 1.33/1.18
% 1.33/1.18 ------ Proving...
% 1.33/1.18 ------ Problem Properties
% 1.33/1.18
% 1.33/1.18
% 1.33/1.18 clauses 1312
% 1.33/1.18 conjectures 7
% 1.33/1.18 EPR 1312
% 1.33/1.18 Horn 1273
% 1.33/1.18 unary 542
% 1.33/1.18 binary 719
% 1.33/1.18 lits 2220
% 1.33/1.18 lits eq 0
% 1.33/1.18 fd_pure 0
% 1.33/1.18 fd_pseudo 0
% 1.33/1.18 fd_cond 0
% 1.33/1.18 fd_pseudo_cond 0
% 1.33/1.18 AC symbols 0
% 1.33/1.18
% 1.33/1.18 ------ Schedule EPR non Horn non eq is on
% 1.33/1.18
% 1.33/1.18 ------ no equalities: superposition off
% 1.33/1.18
% 1.33/1.18 ------ Input Options "--resolution_flag false" Time Limit: 70.
% 1.33/1.18
% 1.33/1.18
% 1.33/1.18 ------
% 1.33/1.18 Current options:
% 1.33/1.18 ------
% 1.33/1.18
% 1.33/1.18 ------ Input Options
% 1.33/1.18
% 1.33/1.18 --out_options all
% 1.33/1.18 --tptp_safe_out true
% 1.33/1.18 --problem_path ""
% 1.33/1.18 --include_path ""
% 1.33/1.18 --clausifier res/vclausify_rel
% 1.33/1.18 --clausifier_options --mode clausify -t 101.67 -updr off
% 1.33/1.18 --stdin false
% 1.33/1.18 --proof_out true
% 1.33/1.18 --proof_dot_file ""
% 1.33/1.18 --proof_reduce_dot []
% 1.33/1.18 --suppress_sat_res false
% 1.33/1.18 --suppress_unsat_res true
% 1.33/1.18 --stats_out none
% 1.33/1.18 --stats_mem false
% 1.33/1.18 --theory_stats_out false
% 1.33/1.18
% 1.33/1.18 ------ General Options
% 1.33/1.18
% 1.33/1.18 --fof false
% 1.33/1.18 --time_out_real 305.
% 1.33/1.18 --time_out_virtual -1.
% 1.33/1.18 --rnd_seed 13
% 1.33/1.18 --symbol_type_check false
% 1.33/1.18 --clausify_out false
% 1.33/1.18 --sig_cnt_out false
% 1.33/1.18 --trig_cnt_out false
% 1.33/1.18 --trig_cnt_out_tolerance 1.
% 1.33/1.18 --trig_cnt_out_sk_spl false
% 1.33/1.18 --abstr_cl_out false
% 1.33/1.18
% 1.33/1.18 ------ Interactive Mode
% 1.33/1.18
% 1.33/1.18 --interactive_mode false
% 1.33/1.18 --external_ip_address ""
% 1.33/1.18 --external_port 0
% 1.33/1.18
% 1.33/1.18 ------ Global Options
% 1.33/1.18
% 1.33/1.18 --schedule default
% 1.33/1.18 --add_important_lit false
% 1.33/1.18 --prop_solver_per_cl 500
% 1.33/1.18 --subs_bck_mult 8
% 1.33/1.18 --min_unsat_core false
% 1.33/1.18 --soft_assumptions false
% 1.33/1.18 --soft_lemma_size 3
% 1.33/1.18 --prop_impl_unit_size 0
% 1.33/1.18 --prop_impl_unit []
% 1.33/1.18 --share_sel_clauses true
% 1.33/1.18 --reset_solvers false
% 1.33/1.18 --bc_imp_inh [conj_cone]
% 1.33/1.18 --conj_cone_tolerance 3.
% 1.33/1.18 --extra_neg_conj none
% 1.33/1.18 --large_theory_mode true
% 1.33/1.18 --prolific_symb_bound 200
% 1.33/1.18 --lt_threshold 2000
% 1.33/1.18 --clause_weak_htbl true
% 1.33/1.18 --gc_record_bc_elim false
% 1.33/1.18
% 1.33/1.18 ------ Preprocessing Options
% 1.33/1.18
% 1.33/1.18 --preprocessing_flag false
% 1.33/1.18 --time_out_prep_mult 0.1
% 1.33/1.18 --splitting_mode input
% 1.33/1.18 --splitting_grd true
% 1.33/1.18 --splitting_cvd false
% 1.33/1.18 --splitting_cvd_svl false
% 1.33/1.18 --splitting_nvd 32
% 1.33/1.18 --sub_typing false
% 1.33/1.18 --prep_eq_flat_conj false
% 1.33/1.18 --prep_ineq_split false
% 1.33/1.18 --prep_eq_flat_all_gr false
% 1.33/1.18 --prep_gs_sim true
% 1.33/1.18 --prep_unflatten true
% 1.33/1.18 --prep_res_sim true
% 1.33/1.18 --prep_sup_sim_all true
% 1.33/1.18 --prep_sup_sim_sup false
% 1.33/1.18 --prep_upred true
% 1.33/1.18 --prep_well_definedness true
% 1.33/1.18 --prep_sem_filter exhaustive
% 1.33/1.18 --prep_sem_filter_out false
% 1.33/1.18 --pred_elim true
% 1.33/1.18 --res_sim_input true
% 1.33/1.18 --eq_ax_congr_red true
% 1.33/1.18 --pure_diseq_elim true
% 1.33/1.18 --brand_transform false
% 1.33/1.18 --non_eq_to_eq false
% 1.33/1.18 --prep_eq_proxy false
% 1.33/1.18 --prep_def_merge true
% 1.33/1.18 --prep_def_merge_prop_impl false
% 1.33/1.18 --prep_def_merge_mbd true
% 1.33/1.18 --prep_def_merge_tr_red false
% 1.33/1.18 --prep_def_merge_tr_cl false
% 1.33/1.18 --smt_preprocessing false
% 1.33/1.18 --smt_ac_axioms fast
% 1.33/1.18 --preprocessed_out false
% 1.33/1.18 --preprocessed_stats false
% 1.33/1.18
% 1.33/1.18 ------ Abstraction refinement Options
% 1.33/1.18
% 1.33/1.18 --abstr_ref []
% 1.33/1.18 --abstr_ref_prep false
% 1.33/1.18 --abstr_ref_until_sat false
% 1.33/1.18 --abstr_ref_sig_restrict funpre
% 1.33/1.18 --abstr_ref_af_restrict_to_split_sk false
% 1.33/1.18 --abstr_ref_under []
% 1.33/1.18
% 1.33/1.18 ------ SAT Options
% 1.33/1.18
% 1.33/1.18 --sat_mode false
% 1.33/1.18 --sat_fm_restart_options ""
% 1.33/1.18 --sat_gr_def false
% 1.33/1.18 --sat_epr_types true
% 1.33/1.18 --sat_non_cyclic_types false
% 1.33/1.18 --sat_finite_models false
% 1.33/1.18 --sat_fm_lemmas false
% 1.33/1.18 --sat_fm_prep false
% 1.33/1.18 --sat_fm_uc_incr true
% 1.33/1.18 --sat_out_model pos
% 1.33/1.18 --sat_out_clauses false
% 1.33/1.18
% 1.33/1.18 ------ QBF Options
% 1.33/1.18
% 1.33/1.18 --qbf_mode false
% 1.33/1.18 --qbf_elim_univ false
% 1.33/1.18 --qbf_dom_inst none
% 1.33/1.18 --qbf_dom_pre_inst false
% 1.33/1.18 --qbf_sk_in false
% 1.33/1.18 --qbf_pred_elim true
% 1.33/1.18 --qbf_split 512
% 1.33/1.18
% 1.33/1.18 ------ BMC1 Options
% 1.33/1.18
% 1.33/1.18 --bmc1_incremental false
% 1.33/1.18 --bmc1_axioms reachable_all
% 1.33/1.18 --bmc1_min_bound 0
% 1.33/1.18 --bmc1_max_bound -1
% 1.33/1.18 --bmc1_max_bound_default -1
% 1.33/1.18 --bmc1_symbol_reachability true
% 1.33/1.18 --bmc1_property_lemmas false
% 1.33/1.18 --bmc1_k_induction false
% 1.33/1.18 --bmc1_non_equiv_states false
% 1.33/1.18 --bmc1_deadlock false
% 1.33/1.18 --bmc1_ucm false
% 1.33/1.18 --bmc1_add_unsat_core none
% 1.33/1.18 --bmc1_unsat_core_children false
% 1.33/1.18 --bmc1_unsat_core_extrapolate_axioms false
% 1.33/1.18 --bmc1_out_stat full
% 1.33/1.18 --bmc1_ground_init false
% 1.33/1.18 --bmc1_pre_inst_next_state false
% 1.33/1.18 --bmc1_pre_inst_state false
% 1.33/1.18 --bmc1_pre_inst_reach_state false
% 1.33/1.18 --bmc1_out_unsat_core false
% 1.33/1.18 --bmc1_aig_witness_out false
% 1.33/1.18 --bmc1_verbose false
% 1.33/1.18 --bmc1_dump_clauses_tptp false
% 1.33/1.18 --bmc1_dump_unsat_core_tptp false
% 1.33/1.18 --bmc1_dump_file -
% 1.33/1.18 --bmc1_ucm_expand_uc_limit 128
% 1.33/1.18 --bmc1_ucm_n_expand_iterations 6
% 1.33/1.18 --bmc1_ucm_extend_mode 1
% 1.33/1.18 --bmc1_ucm_init_mode 2
% 1.33/1.18 --bmc1_ucm_cone_mode none
% 1.33/1.18 --bmc1_ucm_reduced_relation_type 0
% 1.33/1.18 --bmc1_ucm_relax_model 4
% 1.33/1.18 --bmc1_ucm_full_tr_after_sat true
% 1.33/1.18 --bmc1_ucm_expand_neg_assumptions false
% 1.33/1.18 --bmc1_ucm_layered_model none
% 1.33/1.18 --bmc1_ucm_max_lemma_size 10
% 1.33/1.18
% 1.33/1.18 ------ AIG Options
% 1.33/1.18
% 1.33/1.18 --aig_mode false
% 1.33/1.18
% 1.33/1.18 ------ Instantiation Options
% 1.33/1.18
% 1.33/1.18 --instantiation_flag true
% 1.33/1.18 --inst_sos_flag false
% 1.33/1.18 --inst_sos_phase true
% 1.33/1.18 --inst_sos_sth_lit_sel [+prop;+non_prol_conj_symb;-eq;+ground;-num_var;-num_symb]
% 1.33/1.18 --inst_lit_sel [+prop;+num_symb;-sign;+num_var]
% 1.33/1.18 --inst_lit_sel_side num_symb
% 1.33/1.18 --inst_solver_per_active 1400
% 1.33/1.18 --inst_solver_calls_frac 1.
% 1.33/1.18 --inst_to_smt_solver true
% 1.33/1.18 --inst_passive_queue_type priority_queues
% 1.33/1.18 --inst_passive_queues [[-conj_dist;+conj_symb;-num_var];[+age;-num_symb]]
% 1.33/1.18 --inst_passive_queues_freq [25;2]
% 1.33/1.18 --inst_dismatching true
% 1.33/1.18 --inst_eager_unprocessed_to_passive true
% 1.33/1.18 --inst_unprocessed_bound 1000
% 1.33/1.18 --inst_prop_sim_given false
% 1.33/1.18 --inst_prop_sim_new false
% 1.33/1.18 --inst_subs_new false
% 1.33/1.18 --inst_eq_res_simp false
% 1.33/1.18 --inst_subs_given false
% 1.33/1.18 --inst_orphan_elimination true
% 1.33/1.18 --inst_learning_loop_flag true
% 1.33/1.18 --inst_learning_start 3000
% 1.33/1.18 --inst_learning_factor 2
% 1.33/1.18 --inst_start_prop_sim_after_learn 3
% 1.33/1.18 --inst_sel_renew solver
% 1.33/1.18 --inst_lit_activity_flag true
% 1.33/1.18 --inst_restr_to_given false
% 1.33/1.18 --inst_activity_threshold 500
% 1.33/1.18
% 1.33/1.18 ------ Resolution Options
% 1.33/1.18
% 1.33/1.18 --resolution_flag false
% 1.33/1.18 --res_lit_sel adaptive
% 1.33/1.18 --res_lit_sel_side none
% 1.33/1.18 --res_ordering kbo
% 1.33/1.18 --res_to_prop_solver active
% 1.33/1.18 --res_prop_simpl_new false
% 1.33/1.18 --res_prop_simpl_given true
% 1.33/1.18 --res_to_smt_solver true
% 1.33/1.18 --res_passive_queue_type priority_queues
% 1.33/1.18 --res_passive_queues [[-conj_dist;+conj_symb;-num_symb];[+age;-num_symb]]
% 1.33/1.18 --res_passive_queues_freq [15;5]
% 1.33/1.18 --res_forward_subs full
% 1.33/1.18 --res_backward_subs full
% 1.33/1.18 --res_forward_subs_resolution true
% 1.33/1.18 --res_backward_subs_resolution true
% 1.33/1.18 --res_orphan_elimination true
% 1.33/1.18 --res_time_limit 300.
% 1.33/1.18
% 1.33/1.18 ------ Superposition Options
% 1.33/1.18
% 1.33/1.18 --superposition_flag true
% 1.33/1.18 --sup_passive_queue_type priority_queues
% 1.33/1.18 --sup_passive_queues [[-conj_dist;-num_symb];[+score;+min_def_symb;-max_atom_input_occur;+conj_non_prolific_symb];[+age;-num_symb];[+score;-num_symb]]
% 1.33/1.18 --sup_passive_queues_freq [8;1;4;4]
% 1.33/1.18 --twee_lhs_weight 4
% 1.33/1.18 --sup_set_join false
% 1.33/1.18 --sup_set_join_goals true
% 1.33/1.18 --sup_set_join_limit 1000
% 1.33/1.18 --demod_completeness_check fast
% 1.33/1.18 --demod_use_ground true
% 1.33/1.18 --sup_unprocessed_bound 0
% 1.33/1.18 --sup_to_prop_solver passive
% 1.33/1.18 --sup_prop_simpl_new true
% 1.33/1.18 --sup_prop_simpl_given true
% 1.33/1.18 --sup_fun_splitting false
% 1.33/1.18 --sup_iter_deepening 2
% 1.33/1.18 --sup_restarts_mult 12
% 1.33/1.18 --sup_score sim_d_gen
% 1.33/1.18 --sup_share_score_frac 0.2
% 1.33/1.18 --sup_share_max_num_cl 500
% 1.33/1.18 --sup_ordering kbo
% 1.33/1.18 --sup_symb_ordering invfreq
% 1.33/1.18 --sup_term_weight default
% 1.33/1.18
% 1.33/1.18 ------ Superposition Simplification Setup
% 1.33/1.18
% 1.33/1.18 --sup_indices_passive [LightNormIndex;FwDemodIndex]
% 1.33/1.18 --sup_full_triv [SMTSimplify;PropSubs]
% 1.33/1.18 --sup_full_fw [ACNormalisation;FwLightNorm;FwDemod;FwUnitSubsAndRes;FwSubsumption;FwSubsumptionRes;FwGroundJoinability]
% 1.33/1.18 --sup_full_bw [BwDemod;BwUnitSubsAndRes;BwSubsumption;BwSubsumptionRes]
% 1.33/1.18 --sup_immed_triv []
% 1.33/1.18 --sup_immed_fw_main [ACNormalisation;FwLightNorm;FwUnitSubsAndRes]
% 1.33/1.18 --sup_immed_fw_immed [ACNormalisation;FwUnitSubsAndRes]
% 1.33/1.18 --sup_immed_bw_main [BwUnitSubsAndRes;BwDemod]
% 1.33/1.18 --sup_immed_bw_immed [BwUnitSubsAndRes;BwSubsumption;BwSubsumptionRes]
% 1.33/1.18 --sup_input_triv [Unflattening;SMTSimplify]
% 1.33/1.18 --sup_input_fw [FwACDemod;ACNormalisation;FwLightNorm;FwDemod;FwUnitSubsAndRes;FwSubsumption;FwSubsumptionRes;FwGroundJoinability]
% 1.33/1.18 --sup_input_bw [BwACDemod;BwDemod;BwUnitSubsAndRes;BwSubsumption;BwSubsumptionRes]
% 1.33/1.18 --sup_full_fixpoint true
% 1.33/1.18 --sup_main_fixpoint true
% 1.33/1.18 --sup_immed_fixpoint false
% 1.33/1.18 --sup_input_fixpoint true
% 1.33/1.18 --sup_cache_sim none
% 1.33/1.18 --sup_smt_interval 500
% 1.33/1.18 --sup_bw_gjoin_interval 0
% 1.33/1.18
% 1.33/1.18 ------ Combination Options
% 1.33/1.18
% 1.33/1.18 --comb_mode clause_based
% 1.33/1.18 --comb_inst_mult 5
% 1.33/1.18 --comb_res_mult 1
% 1.33/1.18 --comb_sup_mult 1
% 1.33/1.18 --comb_sup_deep_mult 1
% 1.33/1.18
% 1.33/1.18 ------ Debug Options
% 1.33/1.18
% 1.33/1.18 --dbg_backtrace false
% 1.33/1.18 --dbg_dump_prop_clauses false
% 1.33/1.18 --dbg_dump_prop_clauses_file -
% 1.33/1.18 --dbg_out_stat false
% 1.33/1.18 --dbg_just_parse false
% 1.33/1.18
% 1.33/1.18
% 1.33/1.18
% 1.33/1.18
% 1.33/1.18 ------ Proving...
% 1.33/1.18
% 1.33/1.18
% 1.33/1.18 % SZS status CounterSatisfiable for theBenchmark.p
% 1.33/1.18
% 1.33/1.18 ------ Building Model...Done
% 1.33/1.18
% 1.33/1.18 %------ The model is defined over ground terms (initial term algebra).
% 1.33/1.18 %------ Predicates are defined as (\forall x_1,..,x_n ((~)P(x_1,..,x_n) <=> (\phi(x_1,..,x_n))))
% 1.33/1.18 %------ where \phi is a formula over the term algebra.
% 1.33/1.18 %------ If we have equality in the problem then it is also defined as a predicate above,
% 1.33/1.18 %------ with "=" on the right-hand-side of the definition interpreted over the term algebra term_algebra_type
% 1.33/1.18 %------ See help for --sat_out_model for different model outputs.
% 1.33/1.18 %------ equality_sorted(X0,X1,X2) can be used in the place of usual "="
% 1.33/1.18 %------ where the first argument stands for the sort ($i in the unsorted case)
% 1.33/1.18 % SZS output start Model for theBenchmark.p
% See solution above
% 3.74/1.20
%------------------------------------------------------------------------------