%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN423-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n004.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 : Tue Sep 29 02:07:50 PM UTC 2026
% Result : Satisfiable 0.36s 0.29s
% Output : FiniteModel 0.36s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
tff('declare_$i1',type,
'fmb_$i_1': $i ).
tff('declare_$i2',type,
'fmb_$i_2': $i ).
tff('finite_domain_$i',axiom,
! [X: $i] :
( ( X = 'fmb_$i_1' )
| ( X = 'fmb_$i_2' ) ) ).
tff('distinct_domain_$i',axiom,
'fmb_$i_1' != 'fmb_$i_2' ).
tff(declare_a615,type,
a615: $i ).
tff(a615_definition,axiom,
a615 = 'fmb_$i_1' ).
tff(declare_a611,type,
a611: $i ).
tff(a611_definition,axiom,
a611 = 'fmb_$i_2' ).
tff(declare_a591,type,
a591: $i ).
tff(a591_definition,axiom,
a591 = 'fmb_$i_2' ).
tff(declare_a572,type,
a572: $i ).
tff(a572_definition,axiom,
a572 = 'fmb_$i_2' ).
tff(declare_a516,type,
a516: $i ).
tff(a516_definition,axiom,
a516 = 'fmb_$i_2' ).
tff(declare_a513,type,
a513: $i ).
tff(a513_definition,axiom,
a513 = 'fmb_$i_2' ).
tff(declare_a508,type,
a508: $i ).
tff(a508_definition,axiom,
a508 = 'fmb_$i_2' ).
tff(declare_a501,type,
a501: $i ).
tff(a501_definition,axiom,
a501 = 'fmb_$i_2' ).
tff(declare_a479,type,
a479: $i ).
tff(a479_definition,axiom,
a479 = 'fmb_$i_2' ).
tff(declare_a470,type,
a470: $i ).
tff(a470_definition,axiom,
a470 = 'fmb_$i_2' ).
tff(declare_a465,type,
a465: $i ).
tff(a465_definition,axiom,
a465 = 'fmb_$i_2' ).
tff(declare_a457,type,
a457: $i ).
tff(a457_definition,axiom,
a457 = 'fmb_$i_2' ).
tff(declare_a455,type,
a455: $i ).
tff(a455_definition,axiom,
a455 = 'fmb_$i_2' ).
tff(declare_a453,type,
a453: $i ).
tff(a453_definition,axiom,
a453 = 'fmb_$i_2' ).
tff(declare_a617,type,
a617: $i ).
tff(a617_definition,axiom,
a617 = 'fmb_$i_2' ).
tff(declare_a616,type,
a616: $i ).
tff(a616_definition,axiom,
a616 = 'fmb_$i_2' ).
tff(declare_a613,type,
a613: $i ).
tff(a613_definition,axiom,
a613 = 'fmb_$i_2' ).
tff(declare_a610,type,
a610: $i ).
tff(a610_definition,axiom,
a610 = 'fmb_$i_2' ).
tff(declare_a608,type,
a608: $i ).
tff(a608_definition,axiom,
a608 = 'fmb_$i_2' ).
tff(declare_a586,type,
a586: $i ).
tff(a586_definition,axiom,
a586 = 'fmb_$i_2' ).
tff(declare_a579,type,
a579: $i ).
tff(a579_definition,axiom,
a579 = 'fmb_$i_2' ).
tff(declare_a571,type,
a571: $i ).
tff(a571_definition,axiom,
a571 = 'fmb_$i_2' ).
tff(declare_a566,type,
a566: $i ).
tff(a566_definition,axiom,
a566 = 'fmb_$i_2' ).
tff(declare_a543,type,
a543: $i ).
tff(a543_definition,axiom,
a543 = 'fmb_$i_2' ).
tff(declare_a515,type,
a515: $i ).
tff(a515_definition,axiom,
a515 = 'fmb_$i_2' ).
tff(declare_a499,type,
a499: $i ).
tff(a499_definition,axiom,
a499 = 'fmb_$i_2' ).
tff(declare_a490,type,
a490: $i ).
tff(a490_definition,axiom,
a490 = 'fmb_$i_2' ).
tff(declare_a449,type,
a449: $i ).
tff(a449_definition,axiom,
a449 = 'fmb_$i_2' ).
tff(declare_a434,type,
a434: $i ).
tff(a434_definition,axiom,
a434 = 'fmb_$i_2' ).
tff(declare_a619,type,
a619: $i ).
tff(a619_definition,axiom,
a619 = 'fmb_$i_2' ).
tff(declare_a612,type,
a612: $i ).
tff(a612_definition,axiom,
a612 = 'fmb_$i_1' ).
tff(declare_a604,type,
a604: $i ).
tff(a604_definition,axiom,
a604 = 'fmb_$i_2' ).
tff(declare_a592,type,
a592: $i ).
tff(a592_definition,axiom,
a592 = 'fmb_$i_2' ).
tff(declare_a574,type,
a574: $i ).
tff(a574_definition,axiom,
a574 = 'fmb_$i_2' ).
tff(declare_a573,type,
a573: $i ).
tff(a573_definition,axiom,
a573 = 'fmb_$i_2' ).
tff(declare_a564,type,
a564: $i ).
tff(a564_definition,axiom,
a564 = 'fmb_$i_2' ).
tff(declare_a528,type,
a528: $i ).
tff(a528_definition,axiom,
a528 = 'fmb_$i_2' ).
tff(declare_a524,type,
a524: $i ).
tff(a524_definition,axiom,
a524 = 'fmb_$i_2' ).
tff(declare_a521,type,
a521: $i ).
tff(a521_definition,axiom,
a521 = 'fmb_$i_2' ).
tff(declare_a502,type,
a502: $i ).
tff(a502_definition,axiom,
a502 = 'fmb_$i_2' ).
tff(declare_a500,type,
a500: $i ).
tff(a500_definition,axiom,
a500 = 'fmb_$i_1' ).
tff(declare_a491,type,
a491: $i ).
tff(a491_definition,axiom,
a491 = 'fmb_$i_2' ).
tff(declare_a489,type,
a489: $i ).
tff(a489_definition,axiom,
a489 = 'fmb_$i_2' ).
tff(declare_a485,type,
a485: $i ).
tff(a485_definition,axiom,
a485 = 'fmb_$i_2' ).
tff(declare_a481,type,
a481: $i ).
tff(a481_definition,axiom,
a481 = 'fmb_$i_1' ).
tff(declare_a480,type,
a480: $i ).
tff(a480_definition,axiom,
a480 = 'fmb_$i_2' ).
tff(declare_a474,type,
a474: $i ).
tff(a474_definition,axiom,
a474 = 'fmb_$i_2' ).
tff(declare_a471,type,
a471: $i ).
tff(a471_definition,axiom,
a471 = 'fmb_$i_2' ).
tff(declare_a468,type,
a468: $i ).
tff(a468_definition,axiom,
a468 = 'fmb_$i_2' ).
tff(declare_a466,type,
a466: $i ).
tff(a466_definition,axiom,
a466 = 'fmb_$i_2' ).
tff(declare_a460,type,
a460: $i ).
tff(a460_definition,axiom,
a460 = 'fmb_$i_2' ).
tff(declare_a459,type,
a459: $i ).
tff(a459_definition,axiom,
a459 = 'fmb_$i_2' ).
tff(declare_a458,type,
a458: $i ).
tff(a458_definition,axiom,
a458 = 'fmb_$i_2' ).
tff(declare_a456,type,
a456: $i ).
tff(a456_definition,axiom,
a456 = 'fmb_$i_2' ).
tff(declare_a454,type,
a454: $i ).
tff(a454_definition,axiom,
a454 = 'fmb_$i_2' ).
tff(declare_a451,type,
a451: $i ).
tff(a451_definition,axiom,
a451 = 'fmb_$i_2' ).
tff(declare_a437,type,
a437: $i ).
tff(a437_definition,axiom,
a437 = 'fmb_$i_2' ).
tff(declare_a436,type,
a436: $i ).
tff(a436_definition,axiom,
a436 = 'fmb_$i_2' ).
tff(declare_a618,type,
a618: $i ).
tff(a618_definition,axiom,
a618 = 'fmb_$i_2' ).
tff(declare_a603,type,
a603: $i ).
tff(a603_definition,axiom,
a603 = 'fmb_$i_2' ).
tff(declare_a601,type,
a601: $i ).
tff(a601_definition,axiom,
a601 = 'fmb_$i_2' ).
tff(declare_a598,type,
a598: $i ).
tff(a598_definition,axiom,
a598 = 'fmb_$i_2' ).
tff(declare_a593,type,
a593: $i ).
tff(a593_definition,axiom,
a593 = 'fmb_$i_2' ).
tff(declare_a587,type,
a587: $i ).
tff(a587_definition,axiom,
a587 = 'fmb_$i_2' ).
tff(declare_a567,type,
a567: $i ).
tff(a567_definition,axiom,
a567 = 'fmb_$i_2' ).
tff(declare_a560,type,
a560: $i ).
tff(a560_definition,axiom,
a560 = 'fmb_$i_2' ).
tff(declare_a551,type,
a551: $i ).
tff(a551_definition,axiom,
a551 = 'fmb_$i_2' ).
tff(declare_a547,type,
a547: $i ).
tff(a547_definition,axiom,
a547 = 'fmb_$i_2' ).
tff(declare_a540,type,
a540: $i ).
tff(a540_definition,axiom,
a540 = 'fmb_$i_1' ).
tff(declare_a534,type,
a534: $i ).
tff(a534_definition,axiom,
a534 = 'fmb_$i_2' ).
tff(declare_a496,type,
a496: $i ).
tff(a496_definition,axiom,
a496 = 'fmb_$i_1' ).
tff(declare_a494,type,
a494: $i ).
tff(a494_definition,axiom,
a494 = 'fmb_$i_2' ).
tff(declare_a475,type,
a475: $i ).
tff(a475_definition,axiom,
a475 = 'fmb_$i_1' ).
tff(declare_a472,type,
a472: $i ).
tff(a472_definition,axiom,
a472 = 'fmb_$i_2' ).
tff(declare_a450,type,
a450: $i ).
tff(a450_definition,axiom,
a450 = 'fmb_$i_2' ).
tff(declare_a446,type,
a446: $i ).
tff(a446_definition,axiom,
a446 = 'fmb_$i_2' ).
tff(declare_a431,type,
a431: $i ).
tff(a431_definition,axiom,
a431 = 'fmb_$i_1' ).
tff(declare_a609,type,
a609: $i ).
tff(a609_definition,axiom,
a609 = 'fmb_$i_2' ).
tff(declare_a606,type,
a606: $i ).
tff(a606_definition,axiom,
a606 = 'fmb_$i_2' ).
tff(declare_a605,type,
a605: $i ).
tff(a605_definition,axiom,
a605 = 'fmb_$i_2' ).
tff(declare_a568,type,
a568: $i ).
tff(a568_definition,axiom,
a568 = 'fmb_$i_2' ).
tff(declare_a565,type,
a565: $i ).
tff(a565_definition,axiom,
a565 = 'fmb_$i_2' ).
tff(declare_a558,type,
a558: $i ).
tff(a558_definition,axiom,
a558 = 'fmb_$i_2' ).
tff(declare_a548,type,
a548: $i ).
tff(a548_definition,axiom,
a548 = 'fmb_$i_1' ).
tff(declare_a546,type,
a546: $i ).
tff(a546_definition,axiom,
a546 = 'fmb_$i_2' ).
tff(declare_a544,type,
a544: $i ).
tff(a544_definition,axiom,
a544 = 'fmb_$i_2' ).
tff(declare_a539,type,
a539: $i ).
tff(a539_definition,axiom,
a539 = 'fmb_$i_2' ).
tff(declare_a531,type,
a531: $i ).
tff(a531_definition,axiom,
a531 = 'fmb_$i_2' ).
tff(declare_a529,type,
a529: $i ).
tff(a529_definition,axiom,
a529 = 'fmb_$i_2' ).
tff(declare_a525,type,
a525: $i ).
tff(a525_definition,axiom,
a525 = 'fmb_$i_2' ).
tff(declare_a522,type,
a522: $i ).
tff(a522_definition,axiom,
a522 = 'fmb_$i_1' ).
tff(declare_a517,type,
a517: $i ).
tff(a517_definition,axiom,
a517 = 'fmb_$i_2' ).
tff(declare_a509,type,
a509: $i ).
tff(a509_definition,axiom,
a509 = 'fmb_$i_2' ).
tff(declare_a503,type,
a503: $i ).
tff(a503_definition,axiom,
a503 = 'fmb_$i_1' ).
tff(declare_a498,type,
a498: $i ).
tff(a498_definition,axiom,
a498 = 'fmb_$i_1' ).
tff(declare_a493,type,
a493: $i ).
tff(a493_definition,axiom,
a493 = 'fmb_$i_2' ).
tff(declare_a492,type,
a492: $i ).
tff(a492_definition,axiom,
a492 = 'fmb_$i_1' ).
tff(declare_a486,type,
a486: $i ).
tff(a486_definition,axiom,
a486 = 'fmb_$i_2' ).
tff(declare_a483,type,
a483: $i ).
tff(a483_definition,axiom,
a483 = 'fmb_$i_2' ).
tff(declare_a482,type,
a482: $i ).
tff(a482_definition,axiom,
a482 = 'fmb_$i_2' ).
tff(declare_a477,type,
a477: $i ).
tff(a477_definition,axiom,
a477 = 'fmb_$i_2' ).
tff(declare_a469,type,
a469: $i ).
tff(a469_definition,axiom,
a469 = 'fmb_$i_1' ).
tff(declare_a461,type,
a461: $i ).
tff(a461_definition,axiom,
a461 = 'fmb_$i_2' ).
tff(declare_a452,type,
a452: $i ).
tff(a452_definition,axiom,
a452 = 'fmb_$i_2' ).
tff(declare_a448,type,
a448: $i ).
tff(a448_definition,axiom,
a448 = 'fmb_$i_2' ).
tff(declare_a443,type,
a443: $i ).
tff(a443_definition,axiom,
a443 = 'fmb_$i_2' ).
tff(declare_a438,type,
a438: $i ).
tff(a438_definition,axiom,
a438 = 'fmb_$i_2' ).
tff(declare_a614,type,
a614: $i ).
tff(a614_definition,axiom,
a614 = 'fmb_$i_2' ).
tff(declare_a580,type,
a580: $i ).
tff(a580_definition,axiom,
a580 = 'fmb_$i_2' ).
tff(declare_a435,type,
a435: $i ).
tff(a435_definition,axiom,
a435 = 'fmb_$i_2' ).
tff(declare_a570,type,
a570: $i ).
tff(a570_definition,axiom,
a570 = 'fmb_$i_2' ).
tff(declare_a569,type,
a569: $i ).
tff(a569_definition,axiom,
a569 = 'fmb_$i_2' ).
tff(declare_a553,type,
a553: $i ).
tff(a553_definition,axiom,
a553 = 'fmb_$i_2' ).
tff(declare_a549,type,
a549: $i ).
tff(a549_definition,axiom,
a549 = 'fmb_$i_1' ).
tff(declare_a541,type,
a541: $i ).
tff(a541_definition,axiom,
a541 = 'fmb_$i_1' ).
tff(declare_a536,type,
a536: $i ).
tff(a536_definition,axiom,
a536 = 'fmb_$i_2' ).
tff(declare_a532,type,
a532: $i ).
tff(a532_definition,axiom,
a532 = 'fmb_$i_2' ).
tff(declare_a526,type,
a526: $i ).
tff(a526_definition,axiom,
a526 = 'fmb_$i_2' ).
tff(declare_a487,type,
a487: $i ).
tff(a487_definition,axiom,
a487 = 'fmb_$i_2' ).
tff(declare_a445,type,
a445: $i ).
tff(a445_definition,axiom,
a445 = 'fmb_$i_2' ).
tff(declare_a444,type,
a444: $i ).
tff(a444_definition,axiom,
a444 = 'fmb_$i_2' ).
tff(declare_a554,type,
a554: $i ).
tff(a554_definition,axiom,
a554 = 'fmb_$i_2' ).
tff(declare_a537,type,
a537: $i ).
tff(a537_definition,axiom,
a537 = 'fmb_$i_2' ).
tff(declare_a527,type,
a527: $i ).
tff(a527_definition,axiom,
a527 = 'fmb_$i_2' ).
tff(declare_a462,type,
a462: $i ).
tff(a462_definition,axiom,
a462 = 'fmb_$i_2' ).
tff(declare_a484,type,
a484: $i ).
tff(a484_definition,axiom,
a484 = 'fmb_$i_2' ).
tff(declare_a597,type,
a597: $i ).
tff(a597_definition,axiom,
a597 = 'fmb_$i_2' ).
tff(declare_a504,type,
a504: $i ).
tff(a504_definition,axiom,
a504 = 'fmb_$i_2' ).
tff(declare_a523,type,
a523: $i ).
tff(a523_definition,axiom,
a523 = 'fmb_$i_1' ).
tff(declare_a594,type,
a594: $i ).
tff(a594_definition,axiom,
a594 = 'fmb_$i_2' ).
tff(declare_a476,type,
a476: $i ).
tff(a476_definition,axiom,
a476 = 'fmb_$i_1' ).
tff(declare_a533,type,
a533: $i ).
tff(a533_definition,axiom,
a533 = 'fmb_$i_2' ).
tff(declare_a442,type,
a442: $i ).
tff(a442_definition,axiom,
a442 = 'fmb_$i_2' ).
tff(declare_a602,type,
a602: $i ).
tff(a602_definition,axiom,
a602 = 'fmb_$i_2' ).
tff(declare_a599,type,
a599: $i ).
tff(a599_definition,axiom,
a599 = 'fmb_$i_2' ).
tff(declare_a596,type,
a596: $i ).
tff(a596_definition,axiom,
a596 = 'fmb_$i_2' ).
tff(declare_a576,type,
a576: $i ).
tff(a576_definition,axiom,
a576 = 'fmb_$i_2' ).
tff(declare_a557,type,
a557: $i ).
tff(a557_definition,axiom,
a557 = 'fmb_$i_2' ).
tff(declare_a555,type,
a555: $i ).
tff(a555_definition,axiom,
a555 = 'fmb_$i_2' ).
tff(declare_a538,type,
a538: $i ).
tff(a538_definition,axiom,
a538 = 'fmb_$i_1' ).
tff(declare_a507,type,
a507: $i ).
tff(a507_definition,axiom,
a507 = 'fmb_$i_2' ).
tff(declare_a497,type,
a497: $i ).
tff(a497_definition,axiom,
a497 = 'fmb_$i_2' ).
tff(declare_a473,type,
a473: $i ).
tff(a473_definition,axiom,
a473 = 'fmb_$i_2' ).
tff(declare_a447,type,
a447: $i ).
tff(a447_definition,axiom,
a447 = 'fmb_$i_2' ).
tff(declare_a478,type,
a478: $i ).
tff(a478_definition,axiom,
a478 = 'fmb_$i_2' ).
tff(declare_a432,type,
a432: $i ).
tff(a432_definition,axiom,
a432 = 'fmb_$i_2' ).
tff(declare_a530,type,
a530: $i ).
tff(a530_definition,axiom,
a530 = 'fmb_$i_2' ).
tff(declare_a488,type,
a488: $i ).
tff(a488_definition,axiom,
a488 = 'fmb_$i_2' ).
tff(declare_a588,type,
a588: $i ).
tff(a588_definition,axiom,
a588 = 'fmb_$i_1' ).
tff(declare_a581,type,
a581: $i ).
tff(a581_definition,axiom,
a581 = 'fmb_$i_2' ).
tff(declare_a542,type,
a542: $i ).
tff(a542_definition,axiom,
a542 = 'fmb_$i_2' ).
tff(declare_a519,type,
a519: $i ).
tff(a519_definition,axiom,
a519 = 'fmb_$i_2' ).
tff(declare_a439,type,
a439: $i ).
tff(a439_definition,axiom,
a439 = 'fmb_$i_2' ).
tff(declare_a575,type,
a575: $i ).
tff(a575_definition,axiom,
a575 = 'fmb_$i_2' ).
tff(declare_a589,type,
a589: $i ).
tff(a589_definition,axiom,
a589 = 'fmb_$i_2' ).
tff(declare_a582,type,
a582: $i ).
tff(a582_definition,axiom,
a582 = 'fmb_$i_2' ).
tff(declare_a561,type,
a561: $i ).
tff(a561_definition,axiom,
a561 = 'fmb_$i_2' ).
tff(declare_a518,type,
a518: $i ).
tff(a518_definition,axiom,
a518 = 'fmb_$i_2' ).
tff(declare_a433,type,
a433: $i ).
tff(a433_definition,axiom,
a433 = 'fmb_$i_1' ).
tff(declare_a556,type,
a556: $i ).
tff(a556_definition,axiom,
a556 = 'fmb_$i_2' ).
tff(declare_a584,type,
a584: $i ).
tff(a584_definition,axiom,
a584 = 'fmb_$i_2' ).
tff(declare_a559,type,
a559: $i ).
tff(a559_definition,axiom,
a559 = 'fmb_$i_2' ).
tff(declare_a585,type,
a585: $i ).
tff(a585_definition,axiom,
a585 = 'fmb_$i_2' ).
tff(declare_a552,type,
a552: $i ).
tff(a552_definition,axiom,
a552 = 'fmb_$i_2' ).
tff(declare_a511,type,
a511: $i ).
tff(a511_definition,axiom,
a511 = 'fmb_$i_2' ).
tff(declare_a467,type,
a467: $i ).
tff(a467_definition,axiom,
a467 = 'fmb_$i_2' ).
tff(declare_a545,type,
a545: $i ).
tff(a545_definition,axiom,
a545 = 'fmb_$i_2' ).
tff(declare_a607,type,
a607: $i ).
tff(a607_definition,axiom,
a607 = 'fmb_$i_2' ).
tff(declare_a583,type,
a583: $i ).
tff(a583_definition,axiom,
a583 = 'fmb_$i_2' ).
tff(declare_a520,type,
a520: $i ).
tff(a520_definition,axiom,
a520 = 'fmb_$i_2' ).
tff(declare_a505,type,
a505: $i ).
tff(a505_definition,axiom,
a505 = 'fmb_$i_2' ).
tff(declare_a595,type,
a595: $i ).
tff(a595_definition,axiom,
a595 = 'fmb_$i_2' ).
tff(declare_a562,type,
a562: $i ).
tff(a562_definition,axiom,
a562 = 'fmb_$i_2' ).
tff(declare_a535,type,
a535: $i ).
tff(a535_definition,axiom,
a535 = 'fmb_$i_2' ).
tff(declare_a510,type,
a510: $i ).
tff(a510_definition,axiom,
a510 = 'fmb_$i_2' ).
tff(declare_a463,type,
a463: $i ).
tff(a463_definition,axiom,
a463 = 'fmb_$i_2' ).
tff(declare_a590,type,
a590: $i ).
tff(a590_definition,axiom,
a590 = 'fmb_$i_2' ).
tff(declare_a550,type,
a550: $i ).
tff(a550_definition,axiom,
a550 = 'fmb_$i_2' ).
tff(declare_a464,type,
a464: $i ).
tff(a464_definition,axiom,
a464 = 'fmb_$i_2' ).
tff(declare_a512,type,
a512: $i ).
tff(a512_definition,axiom,
a512 = 'fmb_$i_2' ).
tff(declare_a514,type,
a514: $i ).
tff(a514_definition,axiom,
a514 = 'fmb_$i_2' ).
tff(declare_a506,type,
a506: $i ).
tff(a506_definition,axiom,
a506 = 'fmb_$i_2' ).
tff(declare_a495,type,
a495: $i ).
tff(a495_definition,axiom,
a495 = 'fmb_$i_2' ).
tff(declare_a563,type,
a563: $i ).
tff(a563_definition,axiom,
a563 = 'fmb_$i_2' ).
tff(declare_a577,type,
a577: $i ).
tff(a577_definition,axiom,
a577 = 'fmb_$i_2' ).
tff(declare_a600,type,
a600: $i ).
tff(a600_definition,axiom,
a600 = 'fmb_$i_2' ).
tff(declare_a578,type,
a578: $i ).
tff(a578_definition,axiom,
a578 = 'fmb_$i_2' ).
tff(declare_c6_0,type,
c6_0: $o ).
tff(c6_0_definition,axiom,
c6_0 ).
tff(declare_ssSkC39,type,
ssSkC39: $o ).
tff(ssSkC39_definition,axiom,
ssSkC39 ).
tff(declare_ndr1_0,type,
ndr1_0: $o ).
tff(ndr1_0_definition,axiom,
ndr1_0 ).
tff(declare_ssSkC38,type,
ssSkC38: $o ).
tff(ssSkC38_definition,axiom,
~ ssSkC38 ).
tff(declare_ssSkC30,type,
ssSkC30: $o ).
tff(ssSkC30_definition,axiom,
~ ssSkC30 ).
tff(declare_ssSkC25,type,
ssSkC25: $o ).
tff(ssSkC25_definition,axiom,
~ ssSkC25 ).
tff(declare_ssSkC12,type,
ssSkC12: $o ).
tff(ssSkC12_definition,axiom,
ssSkC12 ).
tff(declare_ssSkC11,type,
ssSkC11: $o ).
tff(ssSkC11_definition,axiom,
~ ssSkC11 ).
tff(declare_ssSkC10,type,
ssSkC10: $o ).
tff(ssSkC10_definition,axiom,
~ ssSkC10 ).
tff(declare_c7_0,type,
c7_0: $o ).
tff(c7_0_definition,axiom,
~ c7_0 ).
tff(declare_c5_0,type,
c5_0: $o ).
tff(c5_0_definition,axiom,
~ c5_0 ).
tff(declare_c4_0,type,
c4_0: $o ).
tff(c4_0_definition,axiom,
c4_0 ).
tff(declare_c3_0,type,
c3_0: $o ).
tff(c3_0_definition,axiom,
c3_0 ).
tff(declare_c10_0,type,
c10_0: $o ).
tff(c10_0_definition,axiom,
c10_0 ).
tff(declare_c8_0,type,
c8_0: $o ).
tff(c8_0_definition,axiom,
~ c8_0 ).
tff(declare_ssSkC41,type,
ssSkC41: $o ).
tff(ssSkC41_definition,axiom,
ssSkC41 ).
tff(declare_ssSkC40,type,
ssSkC40: $o ).
tff(ssSkC40_definition,axiom,
ssSkC40 ).
tff(declare_ssSkC37,type,
ssSkC37: $o ).
tff(ssSkC37_definition,axiom,
ssSkC37 ).
tff(declare_ssSkC35,type,
ssSkC35: $o ).
tff(ssSkC35_definition,axiom,
ssSkC35 ).
tff(declare_ssSkC29,type,
ssSkC29: $o ).
tff(ssSkC29_definition,axiom,
ssSkC29 ).
tff(declare_ssSkC27,type,
ssSkC27: $o ).
tff(ssSkC27_definition,axiom,
ssSkC27 ).
tff(declare_ssSkC24,type,
ssSkC24: $o ).
tff(ssSkC24_definition,axiom,
ssSkC24 ).
tff(declare_ssSkC20,type,
ssSkC20: $o ).
tff(ssSkC20_definition,axiom,
ssSkC20 ).
tff(declare_ssSkC18,type,
ssSkC18: $o ).
tff(ssSkC18_definition,axiom,
~ ssSkC18 ).
tff(declare_ssSkC17,type,
ssSkC17: $o ).
tff(ssSkC17_definition,axiom,
ssSkC17 ).
tff(declare_ssSkC8,type,
ssSkC8: $o ).
tff(ssSkC8_definition,axiom,
ssSkC8 ).
tff(declare_ssSkC6,type,
ssSkC6: $o ).
tff(ssSkC6_definition,axiom,
ssSkC6 ).
tff(declare_ssSkC2,type,
ssSkC2: $o ).
tff(ssSkC2_definition,axiom,
ssSkC2 ).
tff(declare_ssSkC0,type,
ssSkC0: $o ).
tff(ssSkC0_definition,axiom,
ssSkC0 ).
tff(declare_ssSkC36,type,
ssSkC36: $o ).
tff(ssSkC36_definition,axiom,
~ ssSkC36 ).
tff(declare_ssSkC34,type,
ssSkC34: $o ).
tff(ssSkC34_definition,axiom,
~ ssSkC34 ).
tff(declare_c9_0,type,
c9_0: $o ).
tff(c9_0_definition,axiom,
~ c9_0 ).
tff(declare_c1_0,type,
c1_0: $o ).
tff(c1_0_definition,axiom,
~ c1_0 ).
tff(declare_ssSkC14,type,
ssSkC14: $o ).
tff(ssSkC14_definition,axiom,
~ ssSkC14 ).
tff(declare_ssSkC13,type,
ssSkC13: $o ).
tff(ssSkC13_definition,axiom,
ssSkC13 ).
tff(declare_ssSkC19,type,
ssSkC19: $o ).
tff(ssSkC19_definition,axiom,
~ ssSkC19 ).
tff(declare_c2_0,type,
c2_0: $o ).
tff(c2_0_definition,axiom,
c2_0 ).
tff(declare_ssSkC5,type,
ssSkC5: $o ).
tff(ssSkC5_definition,axiom,
~ ssSkC5 ).
tff(declare_ssSkC4,type,
ssSkC4: $o ).
tff(ssSkC4_definition,axiom,
~ ssSkC4 ).
tff(declare_ssSkC3,type,
ssSkC3: $o ).
tff(ssSkC3_definition,axiom,
~ ssSkC3 ).
tff(declare_ssSkC22,type,
ssSkC22: $o ).
tff(ssSkC22_definition,axiom,
~ ssSkC22 ).
tff(declare_ssSkC16,type,
ssSkC16: $o ).
tff(ssSkC16_definition,axiom,
~ ssSkC16 ).
tff(declare_ssSkC15,type,
ssSkC15: $o ).
tff(ssSkC15_definition,axiom,
~ ssSkC15 ).
tff(declare_ssSkC7,type,
ssSkC7: $o ).
tff(ssSkC7_definition,axiom,
~ ssSkC7 ).
tff(declare_ssSkC1,type,
ssSkC1: $o ).
tff(ssSkC1_definition,axiom,
ssSkC1 ).
tff(declare_ssSkC32,type,
ssSkC32: $o ).
tff(ssSkC32_definition,axiom,
~ ssSkC32 ).
tff(declare_ssSkC31,type,
ssSkC31: $o ).
tff(ssSkC31_definition,axiom,
ssSkC31 ).
tff(declare_ssSkC33,type,
ssSkC33: $o ).
tff(ssSkC33_definition,axiom,
ssSkC33 ).
tff(declare_ssSkC26,type,
ssSkC26: $o ).
tff(ssSkC26_definition,axiom,
ssSkC26 ).
tff(declare_ssSkC21,type,
ssSkC21: $o ).
tff(ssSkC21_definition,axiom,
ssSkC21 ).
tff(declare_ssSkC23,type,
ssSkC23: $o ).
tff(ssSkC23_definition,axiom,
ssSkC23 ).
tff(declare_ssSkC28,type,
ssSkC28: $o ).
tff(ssSkC28_definition,axiom,
~ ssSkC28 ).
tff(declare_ssSkC9,type,
ssSkC9: $o ).
tff(ssSkC9_definition,axiom,
~ ssSkC9 ).
tff(declare_c7_1,type,
c7_1: $i > $o ).
tff(predicate_c7_1,axiom,
( c7_1('fmb_$i_1')
& c7_1('fmb_$i_2') ) ).
tff(declare_ndr1_1,type,
ndr1_1: $i > $o ).
tff(predicate_ndr1_1,axiom,
( ndr1_1('fmb_$i_1')
& ndr1_1('fmb_$i_2') ) ).
tff(declare_c6_1,type,
c6_1: $i > $o ).
tff(predicate_c6_1,axiom,
( ~ c6_1('fmb_$i_1')
& c6_1('fmb_$i_2') ) ).
tff(declare_c9_1,type,
c9_1: $i > $o ).
tff(predicate_c9_1,axiom,
( c9_1('fmb_$i_1')
& ~ c9_1('fmb_$i_2') ) ).
tff(declare_c2_1,type,
c2_1: $i > $o ).
tff(predicate_c2_1,axiom,
( c2_1('fmb_$i_1')
& c2_1('fmb_$i_2') ) ).
tff(declare_c10_1,type,
c10_1: $i > $o ).
tff(predicate_c10_1,axiom,
( c10_1('fmb_$i_1')
& ~ c10_1('fmb_$i_2') ) ).
tff(declare_c3_1,type,
c3_1: $i > $o ).
tff(predicate_c3_1,axiom,
( ~ c3_1('fmb_$i_1')
& ~ c3_1('fmb_$i_2') ) ).
tff(declare_c8_1,type,
c8_1: $i > $o ).
tff(predicate_c8_1,axiom,
( ~ c8_1('fmb_$i_1')
& c8_1('fmb_$i_2') ) ).
tff(declare_c1_1,type,
c1_1: $i > $o ).
tff(predicate_c1_1,axiom,
( ~ c1_1('fmb_$i_1')
& c1_1('fmb_$i_2') ) ).
tff(declare_c4_1,type,
c4_1: $i > $o ).
tff(predicate_c4_1,axiom,
( c4_1('fmb_$i_1')
& ~ c4_1('fmb_$i_2') ) ).
tff(declare_ssSkP11,type,
ssSkP11: $i > $o ).
tff(predicate_ssSkP11,axiom,
( ssSkP11('fmb_$i_1')
& ssSkP11('fmb_$i_2') ) ).
tff(declare_ssSkP10,type,
ssSkP10: $i > $o ).
tff(predicate_ssSkP10,axiom,
( ssSkP10('fmb_$i_1')
& ssSkP10('fmb_$i_2') ) ).
tff(declare_ssSkP9,type,
ssSkP9: $i > $o ).
tff(predicate_ssSkP9,axiom,
( ssSkP9('fmb_$i_1')
& ssSkP9('fmb_$i_2') ) ).
tff(declare_ssSkP8,type,
ssSkP8: $i > $o ).
tff(predicate_ssSkP8,axiom,
( ssSkP8('fmb_$i_1')
& ssSkP8('fmb_$i_2') ) ).
tff(declare_ssSkP7,type,
ssSkP7: $i > $o ).
tff(predicate_ssSkP7,axiom,
( ssSkP7('fmb_$i_1')
& ssSkP7('fmb_$i_2') ) ).
tff(declare_ssSkP6,type,
ssSkP6: $i > $o ).
tff(predicate_ssSkP6,axiom,
( ssSkP6('fmb_$i_1')
& ssSkP6('fmb_$i_2') ) ).
tff(declare_ssSkP5,type,
ssSkP5: $i > $o ).
tff(predicate_ssSkP5,axiom,
( ~ ssSkP5('fmb_$i_1')
& ssSkP5('fmb_$i_2') ) ).
tff(declare_ssSkP4,type,
ssSkP4: $i > $o ).
tff(predicate_ssSkP4,axiom,
( ssSkP4('fmb_$i_1')
& ssSkP4('fmb_$i_2') ) ).
tff(declare_ssSkP3,type,
ssSkP3: $i > $o ).
tff(predicate_ssSkP3,axiom,
( ~ ssSkP3('fmb_$i_1')
& ssSkP3('fmb_$i_2') ) ).
tff(declare_ssSkP2,type,
ssSkP2: $i > $o ).
tff(predicate_ssSkP2,axiom,
( ssSkP2('fmb_$i_1')
& ssSkP2('fmb_$i_2') ) ).
tff(declare_ssSkP1,type,
ssSkP1: $i > $o ).
tff(predicate_ssSkP1,axiom,
( ssSkP1('fmb_$i_1')
& ssSkP1('fmb_$i_2') ) ).
tff(declare_ssSkP0,type,
ssSkP0: $i > $o ).
tff(predicate_ssSkP0,axiom,
( ~ ssSkP0('fmb_$i_1')
& ssSkP0('fmb_$i_2') ) ).
tff(declare_c1_2,type,
c1_2: ( $i * $i ) > $o ).
tff(predicate_c1_2,axiom,
( c1_2('fmb_$i_1','fmb_$i_1')
& ~ c1_2('fmb_$i_1','fmb_$i_2')
& ~ c1_2('fmb_$i_2','fmb_$i_1')
& c1_2('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_c4_2,type,
c4_2: ( $i * $i ) > $o ).
tff(predicate_c4_2,axiom,
( c4_2('fmb_$i_1','fmb_$i_1')
& ~ c4_2('fmb_$i_1','fmb_$i_2')
& ~ c4_2('fmb_$i_2','fmb_$i_1')
& c4_2('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_c8_2,type,
c8_2: ( $i * $i ) > $o ).
tff(predicate_c8_2,axiom,
( c8_2('fmb_$i_1','fmb_$i_1')
& c8_2('fmb_$i_1','fmb_$i_2')
& c8_2('fmb_$i_2','fmb_$i_1')
& ~ c8_2('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_c5_1,type,
c5_1: $i > $o ).
tff(predicate_c5_1,axiom,
( ~ c5_1('fmb_$i_1')
& ~ c5_1('fmb_$i_2') ) ).
tff(declare_c3_2,type,
c3_2: ( $i * $i ) > $o ).
tff(predicate_c3_2,axiom,
( ~ c3_2('fmb_$i_1','fmb_$i_1')
& ~ c3_2('fmb_$i_1','fmb_$i_2')
& c3_2('fmb_$i_2','fmb_$i_1')
& c3_2('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_c9_2,type,
c9_2: ( $i * $i ) > $o ).
tff(predicate_c9_2,axiom,
( c9_2('fmb_$i_1','fmb_$i_1')
& c9_2('fmb_$i_1','fmb_$i_2')
& c9_2('fmb_$i_2','fmb_$i_1')
& c9_2('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_c5_2,type,
c5_2: ( $i * $i ) > $o ).
tff(predicate_c5_2,axiom,
( ~ c5_2('fmb_$i_1','fmb_$i_1')
& ~ c5_2('fmb_$i_1','fmb_$i_2')
& c5_2('fmb_$i_2','fmb_$i_1')
& c5_2('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_c10_2,type,
c10_2: ( $i * $i ) > $o ).
tff(predicate_c10_2,axiom,
( ~ c10_2('fmb_$i_1','fmb_$i_1')
& ~ c10_2('fmb_$i_1','fmb_$i_2')
& ~ c10_2('fmb_$i_2','fmb_$i_1')
& c10_2('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_c7_2,type,
c7_2: ( $i * $i ) > $o ).
tff(predicate_c7_2,axiom,
( ~ c7_2('fmb_$i_1','fmb_$i_1')
& c7_2('fmb_$i_1','fmb_$i_2')
& ~ c7_2('fmb_$i_2','fmb_$i_1')
& ~ c7_2('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_c2_2,type,
c2_2: ( $i * $i ) > $o ).
tff(predicate_c2_2,axiom,
( ~ c2_2('fmb_$i_1','fmb_$i_1')
& ~ c2_2('fmb_$i_1','fmb_$i_2')
& c2_2('fmb_$i_2','fmb_$i_1')
& ~ c2_2('fmb_$i_2','fmb_$i_2') ) ).
tff(declare_c6_2,type,
c6_2: ( $i * $i ) > $o ).
tff(predicate_c6_2,axiom,
( c6_2('fmb_$i_1','fmb_$i_1')
& c6_2('fmb_$i_1','fmb_$i_2')
& ~ c6_2('fmb_$i_2','fmb_$i_1')
& c6_2('fmb_$i_2','fmb_$i_2') ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN423-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.17 % Computer : n004.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Mon Sep 28 15:55:52 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.20 Running first-order model finding
% 0.08/0.20 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/0.29 % (491039)Will run a generic schedule for satisfiability detection.
% 0.36/0.29 % (491050)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=343711747:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.36/0.29 % (491045)% WARNING: option uhcvi not known.
% 0.36/0.29 % (491044)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1436648304_2999 on theBenchmark for (2999ds/0Mi)
% 0.36/0.29 % (491045)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3455521499:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.36/0.29 % (491047)dis+10_1_sil=32000:sp=arity:random_seed=3183533455:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.36/0.29 % (491048)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2739662883:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.36/0.29 % (491049)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=720857661:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.36/0.29 % (491046)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3245914661:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.36/0.29 % Detected minimum model sizes of [1]
% 0.36/0.29 % Detected maximum model sizes of [187]
% 0.36/0.29 % TRYING [1]
% 0.36/0.29 % TRYING [2]
% 0.36/0.29 % Finite Model Found!
% 0.36/0.29 % SZS status Satisfiable for theBenchmark
% 0.36/0.29 % (491044) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-491039-491044"...
% 0.36/0.29 % (491044)...printing done.
% 0.36/0.29 % SZS output start FiniteModel for theBenchmark
% See solution above
% 0.36/0.29 % (491044)------------------------------
% 0.36/0.29 % (491044)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.36/0.29 % (491044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.36/0.29 % (491044)CaDiCaL version: 2.1.3
% 0.36/0.29 % (491044)Termination reason: Satisfiable
% 0.36/0.29 % (491044)Time elapsed: 0.038 s
% 0.36/0.29 % (491044)Peak memory usage: 14 MB
% 0.36/0.29 % (491044)Instructions burned: 78 (million)
% 0.36/0.29 % (491039)Success in time 0.084 s
% 0.36/0.29 % Vampire exiting
%------------------------------------------------------------------------------