%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL667+1.015 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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 11:59:46 AM UTC 2026
% Result : CounterSatisfiable 2.55s 0.86s
% Output : FiniteModel 2.55s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
tff('declare_$i1',type,
'fmb_$i_1': $i ).
tff('finite_domain_$i',axiom,
! [X: $i] : ( X = 'fmb_$i_1' ) ).
tff(declare_r1,type,
r1: ( $i * $i ) > $o ).
tff(predicate_r1,axiom,
r1('fmb_$i_1','fmb_$i_1') ).
tff(declare_p1615,type,
p1615: $i > $o ).
tff(predicate_p1615,axiom,
~ p1615('fmb_$i_1') ).
tff(declare_p1515,type,
p1515: $i > $o ).
tff(predicate_p1515,axiom,
~ p1515('fmb_$i_1') ).
tff(declare_p1415,type,
p1415: $i > $o ).
tff(predicate_p1415,axiom,
p1415('fmb_$i_1') ).
tff(declare_p1315,type,
p1315: $i > $o ).
tff(predicate_p1315,axiom,
~ p1315('fmb_$i_1') ).
tff(declare_p1215,type,
p1215: $i > $o ).
tff(predicate_p1215,axiom,
~ p1215('fmb_$i_1') ).
tff(declare_p1115,type,
p1115: $i > $o ).
tff(predicate_p1115,axiom,
~ p1115('fmb_$i_1') ).
tff(declare_p1015,type,
p1015: $i > $o ).
tff(predicate_p1015,axiom,
~ p1015('fmb_$i_1') ).
tff(declare_p915,type,
p915: $i > $o ).
tff(predicate_p915,axiom,
~ p915('fmb_$i_1') ).
tff(declare_p815,type,
p815: $i > $o ).
tff(predicate_p815,axiom,
~ p815('fmb_$i_1') ).
tff(declare_p715,type,
p715: $i > $o ).
tff(predicate_p715,axiom,
~ p715('fmb_$i_1') ).
tff(declare_p615,type,
p615: $i > $o ).
tff(predicate_p615,axiom,
~ p615('fmb_$i_1') ).
tff(declare_p515,type,
p515: $i > $o ).
tff(predicate_p515,axiom,
~ p515('fmb_$i_1') ).
tff(declare_p415,type,
p415: $i > $o ).
tff(predicate_p415,axiom,
~ p415('fmb_$i_1') ).
tff(declare_p315,type,
p315: $i > $o ).
tff(predicate_p315,axiom,
~ p315('fmb_$i_1') ).
tff(declare_p215,type,
p215: $i > $o ).
tff(predicate_p215,axiom,
~ p215('fmb_$i_1') ).
tff(declare_p115,type,
p115: $i > $o ).
tff(predicate_p115,axiom,
~ p115('fmb_$i_1') ).
tff(declare_p1614,type,
p1614: $i > $o ).
tff(predicate_p1614,axiom,
~ p1614('fmb_$i_1') ).
tff(declare_p1514,type,
p1514: $i > $o ).
tff(predicate_p1514,axiom,
~ p1514('fmb_$i_1') ).
tff(declare_p1414,type,
p1414: $i > $o ).
tff(predicate_p1414,axiom,
~ p1414('fmb_$i_1') ).
tff(declare_p1314,type,
p1314: $i > $o ).
tff(predicate_p1314,axiom,
~ p1314('fmb_$i_1') ).
tff(declare_p1214,type,
p1214: $i > $o ).
tff(predicate_p1214,axiom,
~ p1214('fmb_$i_1') ).
tff(declare_p1114,type,
p1114: $i > $o ).
tff(predicate_p1114,axiom,
~ p1114('fmb_$i_1') ).
tff(declare_p1014,type,
p1014: $i > $o ).
tff(predicate_p1014,axiom,
~ p1014('fmb_$i_1') ).
tff(declare_p914,type,
p914: $i > $o ).
tff(predicate_p914,axiom,
~ p914('fmb_$i_1') ).
tff(declare_p814,type,
p814: $i > $o ).
tff(predicate_p814,axiom,
~ p814('fmb_$i_1') ).
tff(declare_p714,type,
p714: $i > $o ).
tff(predicate_p714,axiom,
~ p714('fmb_$i_1') ).
tff(declare_p614,type,
p614: $i > $o ).
tff(predicate_p614,axiom,
~ p614('fmb_$i_1') ).
tff(declare_p514,type,
p514: $i > $o ).
tff(predicate_p514,axiom,
~ p514('fmb_$i_1') ).
tff(declare_p414,type,
p414: $i > $o ).
tff(predicate_p414,axiom,
~ p414('fmb_$i_1') ).
tff(declare_p314,type,
p314: $i > $o ).
tff(predicate_p314,axiom,
~ p314('fmb_$i_1') ).
tff(declare_p214,type,
p214: $i > $o ).
tff(predicate_p214,axiom,
p214('fmb_$i_1') ).
tff(declare_p114,type,
p114: $i > $o ).
tff(predicate_p114,axiom,
~ p114('fmb_$i_1') ).
tff(declare_p1613,type,
p1613: $i > $o ).
tff(predicate_p1613,axiom,
~ p1613('fmb_$i_1') ).
tff(declare_p1513,type,
p1513: $i > $o ).
tff(predicate_p1513,axiom,
~ p1513('fmb_$i_1') ).
tff(declare_p1413,type,
p1413: $i > $o ).
tff(predicate_p1413,axiom,
~ p1413('fmb_$i_1') ).
tff(declare_p1313,type,
p1313: $i > $o ).
tff(predicate_p1313,axiom,
~ p1313('fmb_$i_1') ).
tff(declare_p1213,type,
p1213: $i > $o ).
tff(predicate_p1213,axiom,
~ p1213('fmb_$i_1') ).
tff(declare_p1113,type,
p1113: $i > $o ).
tff(predicate_p1113,axiom,
~ p1113('fmb_$i_1') ).
tff(declare_p1013,type,
p1013: $i > $o ).
tff(predicate_p1013,axiom,
~ p1013('fmb_$i_1') ).
tff(declare_p913,type,
p913: $i > $o ).
tff(predicate_p913,axiom,
~ p913('fmb_$i_1') ).
tff(declare_p813,type,
p813: $i > $o ).
tff(predicate_p813,axiom,
~ p813('fmb_$i_1') ).
tff(declare_p713,type,
p713: $i > $o ).
tff(predicate_p713,axiom,
~ p713('fmb_$i_1') ).
tff(declare_p613,type,
p613: $i > $o ).
tff(predicate_p613,axiom,
~ p613('fmb_$i_1') ).
tff(declare_p513,type,
p513: $i > $o ).
tff(predicate_p513,axiom,
~ p513('fmb_$i_1') ).
tff(declare_p413,type,
p413: $i > $o ).
tff(predicate_p413,axiom,
~ p413('fmb_$i_1') ).
tff(declare_p313,type,
p313: $i > $o ).
tff(predicate_p313,axiom,
~ p313('fmb_$i_1') ).
tff(declare_p213,type,
p213: $i > $o ).
tff(predicate_p213,axiom,
~ p213('fmb_$i_1') ).
tff(declare_p113,type,
p113: $i > $o ).
tff(predicate_p113,axiom,
p113('fmb_$i_1') ).
tff(declare_p1612,type,
p1612: $i > $o ).
tff(predicate_p1612,axiom,
~ p1612('fmb_$i_1') ).
tff(declare_p1512,type,
p1512: $i > $o ).
tff(predicate_p1512,axiom,
~ p1512('fmb_$i_1') ).
tff(declare_p1412,type,
p1412: $i > $o ).
tff(predicate_p1412,axiom,
~ p1412('fmb_$i_1') ).
tff(declare_p1312,type,
p1312: $i > $o ).
tff(predicate_p1312,axiom,
~ p1312('fmb_$i_1') ).
tff(declare_p1212,type,
p1212: $i > $o ).
tff(predicate_p1212,axiom,
~ p1212('fmb_$i_1') ).
tff(declare_p1112,type,
p1112: $i > $o ).
tff(predicate_p1112,axiom,
~ p1112('fmb_$i_1') ).
tff(declare_p1012,type,
p1012: $i > $o ).
tff(predicate_p1012,axiom,
~ p1012('fmb_$i_1') ).
tff(declare_p912,type,
p912: $i > $o ).
tff(predicate_p912,axiom,
~ p912('fmb_$i_1') ).
tff(declare_p812,type,
p812: $i > $o ).
tff(predicate_p812,axiom,
p812('fmb_$i_1') ).
tff(declare_p712,type,
p712: $i > $o ).
tff(predicate_p712,axiom,
~ p712('fmb_$i_1') ).
tff(declare_p612,type,
p612: $i > $o ).
tff(predicate_p612,axiom,
~ p612('fmb_$i_1') ).
tff(declare_p512,type,
p512: $i > $o ).
tff(predicate_p512,axiom,
~ p512('fmb_$i_1') ).
tff(declare_p412,type,
p412: $i > $o ).
tff(predicate_p412,axiom,
~ p412('fmb_$i_1') ).
tff(declare_p312,type,
p312: $i > $o ).
tff(predicate_p312,axiom,
~ p312('fmb_$i_1') ).
tff(declare_p212,type,
p212: $i > $o ).
tff(predicate_p212,axiom,
~ p212('fmb_$i_1') ).
tff(declare_p112,type,
p112: $i > $o ).
tff(predicate_p112,axiom,
~ p112('fmb_$i_1') ).
tff(declare_p1611,type,
p1611: $i > $o ).
tff(predicate_p1611,axiom,
~ p1611('fmb_$i_1') ).
tff(declare_p1511,type,
p1511: $i > $o ).
tff(predicate_p1511,axiom,
~ p1511('fmb_$i_1') ).
tff(declare_p1411,type,
p1411: $i > $o ).
tff(predicate_p1411,axiom,
~ p1411('fmb_$i_1') ).
tff(declare_p1311,type,
p1311: $i > $o ).
tff(predicate_p1311,axiom,
~ p1311('fmb_$i_1') ).
tff(declare_p1211,type,
p1211: $i > $o ).
tff(predicate_p1211,axiom,
~ p1211('fmb_$i_1') ).
tff(declare_p1111,type,
p1111: $i > $o ).
tff(predicate_p1111,axiom,
p1111('fmb_$i_1') ).
tff(declare_p1011,type,
p1011: $i > $o ).
tff(predicate_p1011,axiom,
~ p1011('fmb_$i_1') ).
tff(declare_p911,type,
p911: $i > $o ).
tff(predicate_p911,axiom,
~ p911('fmb_$i_1') ).
tff(declare_p811,type,
p811: $i > $o ).
tff(predicate_p811,axiom,
~ p811('fmb_$i_1') ).
tff(declare_p711,type,
p711: $i > $o ).
tff(predicate_p711,axiom,
~ p711('fmb_$i_1') ).
tff(declare_p611,type,
p611: $i > $o ).
tff(predicate_p611,axiom,
p611('fmb_$i_1') ).
tff(declare_p511,type,
p511: $i > $o ).
tff(predicate_p511,axiom,
~ p511('fmb_$i_1') ).
tff(declare_p411,type,
p411: $i > $o ).
tff(predicate_p411,axiom,
~ p411('fmb_$i_1') ).
tff(declare_p311,type,
p311: $i > $o ).
tff(predicate_p311,axiom,
~ p311('fmb_$i_1') ).
tff(declare_p211,type,
p211: $i > $o ).
tff(predicate_p211,axiom,
~ p211('fmb_$i_1') ).
tff(declare_p111,type,
p111: $i > $o ).
tff(predicate_p111,axiom,
~ p111('fmb_$i_1') ).
tff(declare_p1610,type,
p1610: $i > $o ).
tff(predicate_p1610,axiom,
~ p1610('fmb_$i_1') ).
tff(declare_p1510,type,
p1510: $i > $o ).
tff(predicate_p1510,axiom,
~ p1510('fmb_$i_1') ).
tff(declare_p1410,type,
p1410: $i > $o ).
tff(predicate_p1410,axiom,
~ p1410('fmb_$i_1') ).
tff(declare_p1310,type,
p1310: $i > $o ).
tff(predicate_p1310,axiom,
~ p1310('fmb_$i_1') ).
tff(declare_p1210,type,
p1210: $i > $o ).
tff(predicate_p1210,axiom,
~ p1210('fmb_$i_1') ).
tff(declare_p1110,type,
p1110: $i > $o ).
tff(predicate_p1110,axiom,
~ p1110('fmb_$i_1') ).
tff(declare_p1010,type,
p1010: $i > $o ).
tff(predicate_p1010,axiom,
~ p1010('fmb_$i_1') ).
tff(declare_p910,type,
p910: $i > $o ).
tff(predicate_p910,axiom,
~ p910('fmb_$i_1') ).
tff(declare_p810,type,
p810: $i > $o ).
tff(predicate_p810,axiom,
~ p810('fmb_$i_1') ).
tff(declare_p710,type,
p710: $i > $o ).
tff(predicate_p710,axiom,
p710('fmb_$i_1') ).
tff(declare_p610,type,
p610: $i > $o ).
tff(predicate_p610,axiom,
~ p610('fmb_$i_1') ).
tff(declare_p510,type,
p510: $i > $o ).
tff(predicate_p510,axiom,
~ p510('fmb_$i_1') ).
tff(declare_p410,type,
p410: $i > $o ).
tff(predicate_p410,axiom,
~ p410('fmb_$i_1') ).
tff(declare_p310,type,
p310: $i > $o ).
tff(predicate_p310,axiom,
~ p310('fmb_$i_1') ).
tff(declare_p210,type,
p210: $i > $o ).
tff(predicate_p210,axiom,
~ p210('fmb_$i_1') ).
tff(declare_p110,type,
p110: $i > $o ).
tff(predicate_p110,axiom,
~ p110('fmb_$i_1') ).
tff(declare_p1609,type,
p1609: $i > $o ).
tff(predicate_p1609,axiom,
~ p1609('fmb_$i_1') ).
tff(declare_p1509,type,
p1509: $i > $o ).
tff(predicate_p1509,axiom,
~ p1509('fmb_$i_1') ).
tff(declare_p1409,type,
p1409: $i > $o ).
tff(predicate_p1409,axiom,
~ p1409('fmb_$i_1') ).
tff(declare_p1309,type,
p1309: $i > $o ).
tff(predicate_p1309,axiom,
p1309('fmb_$i_1') ).
tff(declare_p1209,type,
p1209: $i > $o ).
tff(predicate_p1209,axiom,
~ p1209('fmb_$i_1') ).
tff(declare_p1109,type,
p1109: $i > $o ).
tff(predicate_p1109,axiom,
~ p1109('fmb_$i_1') ).
tff(declare_p1009,type,
p1009: $i > $o ).
tff(predicate_p1009,axiom,
~ p1009('fmb_$i_1') ).
tff(declare_p909,type,
p909: $i > $o ).
tff(predicate_p909,axiom,
~ p909('fmb_$i_1') ).
tff(declare_p809,type,
p809: $i > $o ).
tff(predicate_p809,axiom,
~ p809('fmb_$i_1') ).
tff(declare_p709,type,
p709: $i > $o ).
tff(predicate_p709,axiom,
~ p709('fmb_$i_1') ).
tff(declare_p609,type,
p609: $i > $o ).
tff(predicate_p609,axiom,
~ p609('fmb_$i_1') ).
tff(declare_p509,type,
p509: $i > $o ).
tff(predicate_p509,axiom,
~ p509('fmb_$i_1') ).
tff(declare_p409,type,
p409: $i > $o ).
tff(predicate_p409,axiom,
~ p409('fmb_$i_1') ).
tff(declare_p309,type,
p309: $i > $o ).
tff(predicate_p309,axiom,
~ p309('fmb_$i_1') ).
tff(declare_p209,type,
p209: $i > $o ).
tff(predicate_p209,axiom,
~ p209('fmb_$i_1') ).
tff(declare_p109,type,
p109: $i > $o ).
tff(predicate_p109,axiom,
~ p109('fmb_$i_1') ).
tff(declare_p1608,type,
p1608: $i > $o ).
tff(predicate_p1608,axiom,
p1608('fmb_$i_1') ).
tff(declare_p1508,type,
p1508: $i > $o ).
tff(predicate_p1508,axiom,
~ p1508('fmb_$i_1') ).
tff(declare_p1408,type,
p1408: $i > $o ).
tff(predicate_p1408,axiom,
~ p1408('fmb_$i_1') ).
tff(declare_p1308,type,
p1308: $i > $o ).
tff(predicate_p1308,axiom,
~ p1308('fmb_$i_1') ).
tff(declare_p1208,type,
p1208: $i > $o ).
tff(predicate_p1208,axiom,
~ p1208('fmb_$i_1') ).
tff(declare_p1108,type,
p1108: $i > $o ).
tff(predicate_p1108,axiom,
~ p1108('fmb_$i_1') ).
tff(declare_p1008,type,
p1008: $i > $o ).
tff(predicate_p1008,axiom,
~ p1008('fmb_$i_1') ).
tff(declare_p908,type,
p908: $i > $o ).
tff(predicate_p908,axiom,
~ p908('fmb_$i_1') ).
tff(declare_p808,type,
p808: $i > $o ).
tff(predicate_p808,axiom,
~ p808('fmb_$i_1') ).
tff(declare_p708,type,
p708: $i > $o ).
tff(predicate_p708,axiom,
~ p708('fmb_$i_1') ).
tff(declare_p608,type,
p608: $i > $o ).
tff(predicate_p608,axiom,
~ p608('fmb_$i_1') ).
tff(declare_p508,type,
p508: $i > $o ).
tff(predicate_p508,axiom,
~ p508('fmb_$i_1') ).
tff(declare_p408,type,
p408: $i > $o ).
tff(predicate_p408,axiom,
~ p408('fmb_$i_1') ).
tff(declare_p308,type,
p308: $i > $o ).
tff(predicate_p308,axiom,
~ p308('fmb_$i_1') ).
tff(declare_p208,type,
p208: $i > $o ).
tff(predicate_p208,axiom,
~ p208('fmb_$i_1') ).
tff(declare_p108,type,
p108: $i > $o ).
tff(predicate_p108,axiom,
~ p108('fmb_$i_1') ).
tff(declare_p1607,type,
p1607: $i > $o ).
tff(predicate_p1607,axiom,
~ p1607('fmb_$i_1') ).
tff(declare_p1507,type,
p1507: $i > $o ).
tff(predicate_p1507,axiom,
~ p1507('fmb_$i_1') ).
tff(declare_p1407,type,
p1407: $i > $o ).
tff(predicate_p1407,axiom,
~ p1407('fmb_$i_1') ).
tff(declare_p1307,type,
p1307: $i > $o ).
tff(predicate_p1307,axiom,
~ p1307('fmb_$i_1') ).
tff(declare_p1207,type,
p1207: $i > $o ).
tff(predicate_p1207,axiom,
~ p1207('fmb_$i_1') ).
tff(declare_p1107,type,
p1107: $i > $o ).
tff(predicate_p1107,axiom,
~ p1107('fmb_$i_1') ).
tff(declare_p1007,type,
p1007: $i > $o ).
tff(predicate_p1007,axiom,
p1007('fmb_$i_1') ).
tff(declare_p907,type,
p907: $i > $o ).
tff(predicate_p907,axiom,
~ p907('fmb_$i_1') ).
tff(declare_p807,type,
p807: $i > $o ).
tff(predicate_p807,axiom,
~ p807('fmb_$i_1') ).
tff(declare_p707,type,
p707: $i > $o ).
tff(predicate_p707,axiom,
~ p707('fmb_$i_1') ).
tff(declare_p607,type,
p607: $i > $o ).
tff(predicate_p607,axiom,
~ p607('fmb_$i_1') ).
tff(declare_p507,type,
p507: $i > $o ).
tff(predicate_p507,axiom,
~ p507('fmb_$i_1') ).
tff(declare_p407,type,
p407: $i > $o ).
tff(predicate_p407,axiom,
~ p407('fmb_$i_1') ).
tff(declare_p307,type,
p307: $i > $o ).
tff(predicate_p307,axiom,
~ p307('fmb_$i_1') ).
tff(declare_p207,type,
p207: $i > $o ).
tff(predicate_p207,axiom,
~ p207('fmb_$i_1') ).
tff(declare_p107,type,
p107: $i > $o ).
tff(predicate_p107,axiom,
~ p107('fmb_$i_1') ).
tff(declare_p1606,type,
p1606: $i > $o ).
tff(predicate_p1606,axiom,
~ p1606('fmb_$i_1') ).
tff(declare_p1506,type,
p1506: $i > $o ).
tff(predicate_p1506,axiom,
~ p1506('fmb_$i_1') ).
tff(declare_p1406,type,
p1406: $i > $o ).
tff(predicate_p1406,axiom,
~ p1406('fmb_$i_1') ).
tff(declare_p1306,type,
p1306: $i > $o ).
tff(predicate_p1306,axiom,
~ p1306('fmb_$i_1') ).
tff(declare_p1206,type,
p1206: $i > $o ).
tff(predicate_p1206,axiom,
~ p1206('fmb_$i_1') ).
tff(declare_p1106,type,
p1106: $i > $o ).
tff(predicate_p1106,axiom,
~ p1106('fmb_$i_1') ).
tff(declare_p1006,type,
p1006: $i > $o ).
tff(predicate_p1006,axiom,
~ p1006('fmb_$i_1') ).
tff(declare_p906,type,
p906: $i > $o ).
tff(predicate_p906,axiom,
~ p906('fmb_$i_1') ).
tff(declare_p806,type,
p806: $i > $o ).
tff(predicate_p806,axiom,
~ p806('fmb_$i_1') ).
tff(declare_p706,type,
p706: $i > $o ).
tff(predicate_p706,axiom,
~ p706('fmb_$i_1') ).
tff(declare_p606,type,
p606: $i > $o ).
tff(predicate_p606,axiom,
~ p606('fmb_$i_1') ).
tff(declare_p506,type,
p506: $i > $o ).
tff(predicate_p506,axiom,
p506('fmb_$i_1') ).
tff(declare_p406,type,
p406: $i > $o ).
tff(predicate_p406,axiom,
~ p406('fmb_$i_1') ).
tff(declare_p306,type,
p306: $i > $o ).
tff(predicate_p306,axiom,
~ p306('fmb_$i_1') ).
tff(declare_p206,type,
p206: $i > $o ).
tff(predicate_p206,axiom,
~ p206('fmb_$i_1') ).
tff(declare_p106,type,
p106: $i > $o ).
tff(predicate_p106,axiom,
~ p106('fmb_$i_1') ).
tff(declare_p1605,type,
p1605: $i > $o ).
tff(predicate_p1605,axiom,
~ p1605('fmb_$i_1') ).
tff(declare_p1505,type,
p1505: $i > $o ).
tff(predicate_p1505,axiom,
~ p1505('fmb_$i_1') ).
tff(declare_p1405,type,
p1405: $i > $o ).
tff(predicate_p1405,axiom,
~ p1405('fmb_$i_1') ).
tff(declare_p1305,type,
p1305: $i > $o ).
tff(predicate_p1305,axiom,
~ p1305('fmb_$i_1') ).
tff(declare_p1205,type,
p1205: $i > $o ).
tff(predicate_p1205,axiom,
p1205('fmb_$i_1') ).
tff(declare_p1105,type,
p1105: $i > $o ).
tff(predicate_p1105,axiom,
~ p1105('fmb_$i_1') ).
tff(declare_p1005,type,
p1005: $i > $o ).
tff(predicate_p1005,axiom,
~ p1005('fmb_$i_1') ).
tff(declare_p905,type,
p905: $i > $o ).
tff(predicate_p905,axiom,
~ p905('fmb_$i_1') ).
tff(declare_p805,type,
p805: $i > $o ).
tff(predicate_p805,axiom,
~ p805('fmb_$i_1') ).
tff(declare_p705,type,
p705: $i > $o ).
tff(predicate_p705,axiom,
~ p705('fmb_$i_1') ).
tff(declare_p605,type,
p605: $i > $o ).
tff(predicate_p605,axiom,
~ p605('fmb_$i_1') ).
tff(declare_p505,type,
p505: $i > $o ).
tff(predicate_p505,axiom,
~ p505('fmb_$i_1') ).
tff(declare_p405,type,
p405: $i > $o ).
tff(predicate_p405,axiom,
~ p405('fmb_$i_1') ).
tff(declare_p305,type,
p305: $i > $o ).
tff(predicate_p305,axiom,
~ p305('fmb_$i_1') ).
tff(declare_p205,type,
p205: $i > $o ).
tff(predicate_p205,axiom,
~ p205('fmb_$i_1') ).
tff(declare_p105,type,
p105: $i > $o ).
tff(predicate_p105,axiom,
~ p105('fmb_$i_1') ).
tff(declare_p1604,type,
p1604: $i > $o ).
tff(predicate_p1604,axiom,
~ p1604('fmb_$i_1') ).
tff(declare_p1504,type,
p1504: $i > $o ).
tff(predicate_p1504,axiom,
~ p1504('fmb_$i_1') ).
tff(declare_p1404,type,
p1404: $i > $o ).
tff(predicate_p1404,axiom,
~ p1404('fmb_$i_1') ).
tff(declare_p1304,type,
p1304: $i > $o ).
tff(predicate_p1304,axiom,
~ p1304('fmb_$i_1') ).
tff(declare_p1204,type,
p1204: $i > $o ).
tff(predicate_p1204,axiom,
~ p1204('fmb_$i_1') ).
tff(declare_p1104,type,
p1104: $i > $o ).
tff(predicate_p1104,axiom,
~ p1104('fmb_$i_1') ).
tff(declare_p1004,type,
p1004: $i > $o ).
tff(predicate_p1004,axiom,
~ p1004('fmb_$i_1') ).
tff(declare_p904,type,
p904: $i > $o ).
tff(predicate_p904,axiom,
p904('fmb_$i_1') ).
tff(declare_p804,type,
p804: $i > $o ).
tff(predicate_p804,axiom,
~ p804('fmb_$i_1') ).
tff(declare_p704,type,
p704: $i > $o ).
tff(predicate_p704,axiom,
~ p704('fmb_$i_1') ).
tff(declare_p604,type,
p604: $i > $o ).
tff(predicate_p604,axiom,
~ p604('fmb_$i_1') ).
tff(declare_p504,type,
p504: $i > $o ).
tff(predicate_p504,axiom,
~ p504('fmb_$i_1') ).
tff(declare_p404,type,
p404: $i > $o ).
tff(predicate_p404,axiom,
~ p404('fmb_$i_1') ).
tff(declare_p304,type,
p304: $i > $o ).
tff(predicate_p304,axiom,
~ p304('fmb_$i_1') ).
tff(declare_p204,type,
p204: $i > $o ).
tff(predicate_p204,axiom,
~ p204('fmb_$i_1') ).
tff(declare_p104,type,
p104: $i > $o ).
tff(predicate_p104,axiom,
~ p104('fmb_$i_1') ).
tff(declare_p1603,type,
p1603: $i > $o ).
tff(predicate_p1603,axiom,
~ p1603('fmb_$i_1') ).
tff(declare_p1503,type,
p1503: $i > $o ).
tff(predicate_p1503,axiom,
p1503('fmb_$i_1') ).
tff(declare_p1403,type,
p1403: $i > $o ).
tff(predicate_p1403,axiom,
~ p1403('fmb_$i_1') ).
tff(declare_p1303,type,
p1303: $i > $o ).
tff(predicate_p1303,axiom,
~ p1303('fmb_$i_1') ).
tff(declare_p1203,type,
p1203: $i > $o ).
tff(predicate_p1203,axiom,
~ p1203('fmb_$i_1') ).
tff(declare_p1103,type,
p1103: $i > $o ).
tff(predicate_p1103,axiom,
~ p1103('fmb_$i_1') ).
tff(declare_p1003,type,
p1003: $i > $o ).
tff(predicate_p1003,axiom,
~ p1003('fmb_$i_1') ).
tff(declare_p903,type,
p903: $i > $o ).
tff(predicate_p903,axiom,
~ p903('fmb_$i_1') ).
tff(declare_p803,type,
p803: $i > $o ).
tff(predicate_p803,axiom,
~ p803('fmb_$i_1') ).
tff(declare_p703,type,
p703: $i > $o ).
tff(predicate_p703,axiom,
~ p703('fmb_$i_1') ).
tff(declare_p603,type,
p603: $i > $o ).
tff(predicate_p603,axiom,
~ p603('fmb_$i_1') ).
tff(declare_p503,type,
p503: $i > $o ).
tff(predicate_p503,axiom,
~ p503('fmb_$i_1') ).
tff(declare_p403,type,
p403: $i > $o ).
tff(predicate_p403,axiom,
~ p403('fmb_$i_1') ).
tff(declare_p303,type,
p303: $i > $o ).
tff(predicate_p303,axiom,
~ p303('fmb_$i_1') ).
tff(declare_p203,type,
p203: $i > $o ).
tff(predicate_p203,axiom,
~ p203('fmb_$i_1') ).
tff(declare_p103,type,
p103: $i > $o ).
tff(predicate_p103,axiom,
~ p103('fmb_$i_1') ).
tff(declare_p1602,type,
p1602: $i > $o ).
tff(predicate_p1602,axiom,
~ p1602('fmb_$i_1') ).
tff(declare_p1502,type,
p1502: $i > $o ).
tff(predicate_p1502,axiom,
~ p1502('fmb_$i_1') ).
tff(declare_p1402,type,
p1402: $i > $o ).
tff(predicate_p1402,axiom,
~ p1402('fmb_$i_1') ).
tff(declare_p1302,type,
p1302: $i > $o ).
tff(predicate_p1302,axiom,
~ p1302('fmb_$i_1') ).
tff(declare_p1202,type,
p1202: $i > $o ).
tff(predicate_p1202,axiom,
~ p1202('fmb_$i_1') ).
tff(declare_p1102,type,
p1102: $i > $o ).
tff(predicate_p1102,axiom,
~ p1102('fmb_$i_1') ).
tff(declare_p1002,type,
p1002: $i > $o ).
tff(predicate_p1002,axiom,
~ p1002('fmb_$i_1') ).
tff(declare_p902,type,
p902: $i > $o ).
tff(predicate_p902,axiom,
~ p902('fmb_$i_1') ).
tff(declare_p802,type,
p802: $i > $o ).
tff(predicate_p802,axiom,
~ p802('fmb_$i_1') ).
tff(declare_p702,type,
p702: $i > $o ).
tff(predicate_p702,axiom,
~ p702('fmb_$i_1') ).
tff(declare_p602,type,
p602: $i > $o ).
tff(predicate_p602,axiom,
~ p602('fmb_$i_1') ).
tff(declare_p502,type,
p502: $i > $o ).
tff(predicate_p502,axiom,
~ p502('fmb_$i_1') ).
tff(declare_p402,type,
p402: $i > $o ).
tff(predicate_p402,axiom,
p402('fmb_$i_1') ).
tff(declare_p302,type,
p302: $i > $o ).
tff(predicate_p302,axiom,
~ p302('fmb_$i_1') ).
tff(declare_p202,type,
p202: $i > $o ).
tff(predicate_p202,axiom,
~ p202('fmb_$i_1') ).
tff(declare_p102,type,
p102: $i > $o ).
tff(predicate_p102,axiom,
~ p102('fmb_$i_1') ).
tff(declare_p1601,type,
p1601: $i > $o ).
tff(predicate_p1601,axiom,
~ p1601('fmb_$i_1') ).
tff(declare_p1501,type,
p1501: $i > $o ).
tff(predicate_p1501,axiom,
~ p1501('fmb_$i_1') ).
tff(declare_p1401,type,
p1401: $i > $o ).
tff(predicate_p1401,axiom,
~ p1401('fmb_$i_1') ).
tff(declare_p1301,type,
p1301: $i > $o ).
tff(predicate_p1301,axiom,
~ p1301('fmb_$i_1') ).
tff(declare_p1201,type,
p1201: $i > $o ).
tff(predicate_p1201,axiom,
~ p1201('fmb_$i_1') ).
tff(declare_p1101,type,
p1101: $i > $o ).
tff(predicate_p1101,axiom,
~ p1101('fmb_$i_1') ).
tff(declare_p1001,type,
p1001: $i > $o ).
tff(predicate_p1001,axiom,
~ p1001('fmb_$i_1') ).
tff(declare_p901,type,
p901: $i > $o ).
tff(predicate_p901,axiom,
~ p901('fmb_$i_1') ).
tff(declare_p801,type,
p801: $i > $o ).
tff(predicate_p801,axiom,
~ p801('fmb_$i_1') ).
tff(declare_p701,type,
p701: $i > $o ).
tff(predicate_p701,axiom,
~ p701('fmb_$i_1') ).
tff(declare_p601,type,
p601: $i > $o ).
tff(predicate_p601,axiom,
~ p601('fmb_$i_1') ).
tff(declare_p501,type,
p501: $i > $o ).
tff(predicate_p501,axiom,
~ p501('fmb_$i_1') ).
tff(declare_p401,type,
p401: $i > $o ).
tff(predicate_p401,axiom,
~ p401('fmb_$i_1') ).
tff(declare_p301,type,
p301: $i > $o ).
tff(predicate_p301,axiom,
p301('fmb_$i_1') ).
tff(declare_p201,type,
p201: $i > $o ).
tff(predicate_p201,axiom,
~ p201('fmb_$i_1') ).
tff(declare_p101,type,
p101: $i > $o ).
tff(predicate_p101,axiom,
~ p101('fmb_$i_1') ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL667+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.35 % Computer : n012.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 27 16:27:05 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.38 Running first-order model finding
% 0.09/0.38 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 2.55/0.86 % (2567482)Will run a generic schedule for satisfiability detection.
% 2.55/0.86 % (2567487)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=702487693_2999 on theBenchmark for (2999ds/0Mi)
% 2.55/0.86 % (2567488)% WARNING: option uhcvi not known.
% 2.55/0.86 % (2567492)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3911081848:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.55/0.86 % (2567493)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=629430766:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.55/0.86 % (2567489)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=761696989:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.55/0.86 % (2567488)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3708482159:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.55/0.86 % (2567491)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=757189877:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.55/0.86 % (2567490)dis+10_1_sil=32000:sp=arity:random_seed=2892267259:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.55/0.86 % (2567490)Instruction limit reached!
% 2.55/0.86 % (2567490)------------------------------
% 2.55/0.86 % (2567490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.55/0.86 % (2567490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/0.86 % (2567490)CaDiCaL version: 2.1.3
% 2.55/0.86 % (2567490)Termination reason: Instruction limit
% 2.55/0.86 % (2567490)Termination phase: Naming
% 2.55/0.86 % (2567490)Time elapsed: 0.047 s
% 2.55/0.86 % (2567490)Peak memory usage: 14 MB
% 2.55/0.86 % (2567490)Instructions burned: 105 (million)
% 2.55/0.86 % (2567492)Instruction limit reached!
% 2.55/0.86 % (2567492)------------------------------
% 2.55/0.86 % (2567492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.55/0.86 % (2567492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/0.86 % (2567492)CaDiCaL version: 2.1.3
% 2.55/0.86 % (2567492)Termination reason: Instruction limit
% 2.55/0.86 % (2567492)Termination phase: Preprocessing 3
% 2.55/0.86 % (2567492)Time elapsed: 0.059 s
% 2.55/0.86 % (2567492)Peak memory usage: 15 MB
% 2.55/0.86 % (2567492)Instructions burned: 133 (million)
% 2.55/0.86 % (2567491)Instruction limit reached!
% 2.55/0.86 % (2567491)------------------------------
% 2.55/0.86 % (2567491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.55/0.86 % (2567491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/0.86 % (2567491)CaDiCaL version: 2.1.3
% 2.55/0.86 % (2567491)Termination reason: Instruction limit
% 2.55/0.86 % (2567491)Termination phase: Property scanning
% 2.55/0.86 % (2567491)Time elapsed: 0.060 s
% 2.55/0.86 % (2567491)Peak memory usage: 16 MB
% 2.55/0.86 % (2567491)Instructions burned: 117 (million)
% 2.55/0.86 % (2567493)Instruction limit reached!
% 2.55/0.86 % (2567493)------------------------------
% 2.55/0.86 % (2567493)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.55/0.86 % (2567493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/0.86 % (2567493)CaDiCaL version: 2.1.3
% 2.55/0.86 % (2567493)Termination reason: Instruction limit
% 2.55/0.86 % (2567493)Termination phase: Preprocessing 3
% 2.55/0.86 % (2567493)Time elapsed: 0.070 s
% 2.55/0.86 % (2567493)Peak memory usage: 16 MB
% 2.55/0.86 % (2567493)Instructions burned: 159 (million)
% 2.55/0.86 % (2567501)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2357146418:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 2.55/0.86 % (2567502)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=205102059:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 2.55/0.86 % (2567503)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=4057455619:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 2.55/0.86 % (2567505)ott-21_1_sil=16000:fs=off:random_seed=3420391206:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 2.55/0.86 % (2567502)Instruction limit reached!
% 2.55/0.86 % (2567502)------------------------------
% 2.55/0.86 % (2567502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.55/0.86 % (2567502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/0.86 % (2567502)CaDiCaL version: 2.1.3
% 2.55/0.86 % (2567502)Termination reason: Instruction limit
% 2.55/0.86 % (2567502)Termination phase: Preprocessing 3
% 2.55/0.86 % (2567502)Time elapsed: 0.057 s
% 2.55/0.86 % (2567502)Peak memory usage: 15 MB
% 2.55/0.86 % (2567502)Instructions burned: 131 (million)
% 2.55/0.86 % (2567509)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2701915607:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 2.55/0.86 % (2567505)Instruction limit reached!
% 2.55/0.86 % (2567505)------------------------------
% 2.55/0.86 % (2567505)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.55/0.86 % (2567505)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/0.86 % (2567505)CaDiCaL version: 2.1.3
% 2.55/0.86 % (2567505)Termination reason: Instruction limit
% 2.55/0.86 % (2567505)Termination phase: Property scanning
% 2.55/0.86 % (2567505)Time elapsed: 0.082 s
% 2.55/0.86 % (2567505)Peak memory usage: 18 MB
% 2.55/0.86 % (2567505)Instructions burned: 180 (million)
% 2.55/0.86 % (2567511)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=637168839:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 2.55/0.86 % TRYING [1]
% 2.55/0.86 % TRYING [1]
% 2.55/0.86 % (2567509)Instruction limit reached!
% 2.55/0.86 % (2567509)------------------------------
% 2.55/0.86 % (2567509)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.55/0.86 % (2567509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/0.86 % (2567509)CaDiCaL version: 2.1.3
% 2.55/0.86 % (2567509)Termination reason: Instruction limit
% 2.55/0.86 % (2567509)Termination phase: Saturation
% 2.55/0.86 % (2567509)Time elapsed: 0.131 s
% 2.55/0.86 % (2567509)Peak memory usage: 22 MB
% 2.55/0.86 % (2567509)Instructions burned: 478 (million)
% 2.55/0.86 % (2567513)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1719239111:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 2.55/0.86 % (2567501)Instruction limit reached!
% 2.55/0.86 % (2567501)------------------------------
% 2.55/0.86 % (2567501)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.55/0.86 % (2567501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/0.86 % (2567501)CaDiCaL version: 2.1.3
% 2.55/0.86 % (2567501)Termination reason: Instruction limit
% 2.55/0.86 % (2567501)Termination phase: Finite model building SAT solving
% 2.55/0.86 % (2567501)Time elapsed: 0.305 s
% 2.55/0.86 % (2567501)Peak memory usage: 24 MB
% 2.55/0.86 % (2567501)Instructions burned: 715 (million)
% 2.55/0.86 % (2567515)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=808636542:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 2.55/0.86 % TRYING [1]
% 2.55/0.86 % Finite Model Found!
% 2.55/0.86 % SZS status CounterSatisfiable for theBenchmark
% 2.55/0.86 % (2567511) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2567482-2567511"...
% 2.55/0.86 % (2567511)...printing done.
% 2.55/0.86 % SZS output start FiniteModel for theBenchmark
% See solution above
% 2.55/0.86 % (2567511)------------------------------
% 2.55/0.86 % (2567511)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.55/0.86 % (2567511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.55/0.86 % (2567511)CaDiCaL version: 2.1.3
% 2.55/0.86 % (2567511)Termination reason: Satisfiable
% 2.55/0.86 % (2567511)Time elapsed: 0.206 s
% 2.55/0.86 % (2567511)Peak memory usage: 24 MB
% 2.55/0.86 % (2567511)Instructions burned: 470 (million)
% 2.55/0.86 % (2567482)Success in time 0.47 s
% 2.55/0.86 % Vampire exiting
%------------------------------------------------------------------------------