%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL685+1.015 : TPTP v9.3.1. Released v4.0.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 12:00:17 PM UTC 2026
% Result : CounterSatisfiable 1.70s 0.90s
% Output : FiniteModel 3.23s
% 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 : LCL685+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.37 % Computer : n004.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 16:38:22 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.41 Running first-order model finding
% 0.10/0.41 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
% 1.70/0.90 % (3720360)Will run a generic schedule for satisfiability detection.
% 1.70/0.90 % (3720365)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2754099973_2999 on theBenchmark for (2999ds/0Mi)
% 1.70/0.90 % (3720366)% WARNING: option uhcvi not known.
% 1.70/0.90 % (3720367)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=546132083:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.70/0.90 % (3720366)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1552266616:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.70/0.90 % (3720368)dis+10_1_sil=32000:sp=arity:random_seed=4227670749:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.70/0.90 % (3720371)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3366910254:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.70/0.90 % (3720369)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1912279652:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.70/0.90 % (3720370)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1704353350:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.70/0.90 % (3720368)Instruction limit reached!
% 1.70/0.90 % (3720368)------------------------------
% 1.70/0.90 % (3720368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/0.90 % (3720368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/0.90 % (3720368)CaDiCaL version: 2.1.3
% 1.70/0.90 % (3720368)Termination reason: Instruction limit
% 1.70/0.90 % (3720368)Termination phase: Naming
% 1.70/0.90 % (3720368)Time elapsed: 0.052 s
% 1.70/0.90 % (3720368)Peak memory usage: 16 MB
% 1.70/0.90 % (3720368)Instructions burned: 105 (million)
% 1.70/0.90 % (3720369)Instruction limit reached!
% 1.70/0.90 % (3720369)------------------------------
% 1.70/0.90 % (3720369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/0.90 % (3720369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/0.90 % (3720369)CaDiCaL version: 2.1.3
% 1.70/0.90 % (3720369)Termination reason: Instruction limit
% 1.70/0.90 % (3720369)Termination phase: NewCNF
% 1.70/0.90 % (3720369)Time elapsed: 0.062 s
% 1.70/0.90 % (3720369)Peak memory usage: 17 MB
% 1.70/0.90 % (3720369)Instructions burned: 116 (million)
% 1.70/0.90 % (3720370)Instruction limit reached!
% 1.70/0.90 % (3720370)------------------------------
% 1.70/0.90 % (3720370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/0.90 % (3720370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/0.90 % (3720370)CaDiCaL version: 2.1.3
% 1.70/0.90 % (3720370)Termination reason: Instruction limit
% 1.70/0.90 % (3720370)Termination phase: Naming
% 1.70/0.90 % (3720370)Time elapsed: 0.065 s
% 1.70/0.90 % (3720370)Peak memory usage: 16 MB
% 1.70/0.90 % (3720370)Instructions burned: 131 (million)
% 1.70/0.90 % (3720371)Instruction limit reached!
% 1.70/0.90 % (3720371)------------------------------
% 1.70/0.90 % (3720371)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/0.90 % (3720371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/0.90 % (3720371)CaDiCaL version: 2.1.3
% 1.70/0.90 % (3720371)Termination reason: Instruction limit
% 1.70/0.90 % (3720371)Termination phase: Preprocessing 3
% 1.70/0.90 % (3720371)Time elapsed: 0.073 s
% 1.70/0.90 % (3720371)Peak memory usage: 17 MB
% 1.70/0.90 % (3720371)Instructions burned: 160 (million)
% 1.70/0.90 % (3720379)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1691669813:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 1.70/0.90 % (3720380)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1566831454:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.70/0.90 % (3720381)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=3196065410:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.70/0.90 % (3720383)ott-21_1_sil=16000:fs=off:random_seed=811699305:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.70/0.90 % (3720380)Instruction limit reached!
% 1.70/0.90 % (3720380)------------------------------
% 1.70/0.90 % (3720380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/0.90 % (3720380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/0.90 % (3720380)CaDiCaL version: 2.1.3
% 1.70/0.90 % (3720380)Termination reason: Instruction limit
% 1.70/0.90 % (3720380)Termination phase: Naming
% 1.70/0.90 % (3720380)Time elapsed: 0.065 s
% 1.70/0.90 % (3720380)Peak memory usage: 16 MB
% 1.70/0.90 % (3720380)Instructions burned: 133 (million)
% 1.70/0.90 % (3720387)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2710849969:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 1.70/0.90 % (3720383)Instruction limit reached!
% 1.70/0.90 % (3720383)------------------------------
% 1.70/0.90 % (3720383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/0.90 % (3720383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/0.90 % (3720383)CaDiCaL version: 2.1.3
% 1.70/0.90 % (3720383)Termination reason: Instruction limit
% 1.70/0.90 % (3720383)Termination phase: Preprocessing 3
% 1.70/0.90 % (3720383)Time elapsed: 0.080 s
% 1.70/0.90 % (3720383)Peak memory usage: 18 MB
% 1.70/0.90 % (3720383)Instructions burned: 180 (million)
% 1.70/0.90 % (3720389)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1888253047:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 1.70/0.90 % TRYING [1]
% 1.70/0.90 % TRYING [1]
% 1.70/0.90 % (3720379)Instruction limit reached!
% 1.70/0.90 % (3720379)------------------------------
% 1.70/0.90 % (3720379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/0.90 % (3720379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/0.90 % (3720379)CaDiCaL version: 2.1.3
% 1.70/0.90 % (3720379)Termination reason: Instruction limit
% 1.70/0.90 % (3720379)Termination phase: Finite model building SAT solving
% 1.70/0.90 % (3720379)Time elapsed: 0.303 s
% 1.70/0.90 % (3720379)Peak memory usage: 30 MB
% 1.70/0.90 % (3720379)Instructions burned: 716 (million)
% 1.70/0.90 % (3720387)Instruction limit reached!
% 1.70/0.90 % (3720387)------------------------------
% 1.70/0.90 % (3720387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/0.90 % (3720387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/0.90 % (3720387)CaDiCaL version: 2.1.3
% 1.70/0.90 % (3720387)Termination reason: Instruction limit
% 1.70/0.90 % (3720387)Termination phase: Saturation
% 1.70/0.90 % (3720387)Time elapsed: 0.212 s
% 1.70/0.90 % (3720387)Peak memory usage: 25 MB
% 1.70/0.90 % (3720387)Instructions burned: 477 (million)
% 1.70/0.90 % (3720392)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3999939454:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 1.70/0.90 % (3720381)Instruction limit reached!
% 1.70/0.90 % (3720381)------------------------------
% 1.70/0.90 % (3720381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.70/0.90 % (3720381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.70/0.90 % (3720381)CaDiCaL version: 2.1.3
% 1.70/0.90 % (3720381)Termination reason: Instruction limit
% 1.70/0.90 % (3720381)Termination phase: Saturation
% 1.70/0.90 % (3720381)Time elapsed: 0.316 s
% 1.70/0.90 % (3720381)Peak memory usage: 25 MB
% 1.70/0.90 % (3720381)Instructions burned: 686 (million)
% 1.70/0.90 % (3720393)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3607388656:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 1.70/0.90 % Finite Model Found!
% 1.70/0.90 % SZS status CounterSatisfiable for theBenchmark
% 1.70/0.90 % (3720365) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3720360-3720365"...
% 1.70/0.90 % (3720365)...printing done.
% 3.23/0.90 % SZS output start FiniteModel for theBenchmark
% See solution above
% 3.23/0.90 % (3720365)------------------------------
% 3.23/0.90 % (3720365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.23/0.90 % (3720365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.23/0.90 % (3720365)CaDiCaL version: 2.1.3
% 3.23/0.90 % (3720365)Termination reason: Satisfiable
% 3.23/0.90 % (3720365)Time elapsed: 0.413 s
% 3.23/0.90 % (3720365)Peak memory usage: 39 MB
% 3.23/0.90 % (3720365)Instructions burned: 1682 (million)
% 3.23/0.90 % (3720360)Success in time 0.481 s
% 3.23/0.90 % Vampire exiting
%------------------------------------------------------------------------------