%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL667+1.020 : 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 : n011.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 13.78s 2.77s
% Output : FiniteModel 13.78s
% 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_p2120,type,
p2120: $i > $o ).
tff(predicate_p2120,axiom,
~ p2120('fmb_$i_1') ).
tff(declare_p2020,type,
p2020: $i > $o ).
tff(predicate_p2020,axiom,
~ p2020('fmb_$i_1') ).
tff(declare_p1920,type,
p1920: $i > $o ).
tff(predicate_p1920,axiom,
~ p1920('fmb_$i_1') ).
tff(declare_p1820,type,
p1820: $i > $o ).
tff(predicate_p1820,axiom,
~ p1820('fmb_$i_1') ).
tff(declare_p1720,type,
p1720: $i > $o ).
tff(predicate_p1720,axiom,
~ p1720('fmb_$i_1') ).
tff(declare_p1620,type,
p1620: $i > $o ).
tff(predicate_p1620,axiom,
~ p1620('fmb_$i_1') ).
tff(declare_p1520,type,
p1520: $i > $o ).
tff(predicate_p1520,axiom,
~ p1520('fmb_$i_1') ).
tff(declare_p1420,type,
p1420: $i > $o ).
tff(predicate_p1420,axiom,
~ p1420('fmb_$i_1') ).
tff(declare_p1320,type,
p1320: $i > $o ).
tff(predicate_p1320,axiom,
~ p1320('fmb_$i_1') ).
tff(declare_p1220,type,
p1220: $i > $o ).
tff(predicate_p1220,axiom,
~ p1220('fmb_$i_1') ).
tff(declare_p1120,type,
p1120: $i > $o ).
tff(predicate_p1120,axiom,
~ p1120('fmb_$i_1') ).
tff(declare_p1020,type,
p1020: $i > $o ).
tff(predicate_p1020,axiom,
~ p1020('fmb_$i_1') ).
tff(declare_p920,type,
p920: $i > $o ).
tff(predicate_p920,axiom,
~ p920('fmb_$i_1') ).
tff(declare_p820,type,
p820: $i > $o ).
tff(predicate_p820,axiom,
~ p820('fmb_$i_1') ).
tff(declare_p720,type,
p720: $i > $o ).
tff(predicate_p720,axiom,
~ p720('fmb_$i_1') ).
tff(declare_p620,type,
p620: $i > $o ).
tff(predicate_p620,axiom,
~ p620('fmb_$i_1') ).
tff(declare_p520,type,
p520: $i > $o ).
tff(predicate_p520,axiom,
~ p520('fmb_$i_1') ).
tff(declare_p420,type,
p420: $i > $o ).
tff(predicate_p420,axiom,
~ p420('fmb_$i_1') ).
tff(declare_p320,type,
p320: $i > $o ).
tff(predicate_p320,axiom,
~ p320('fmb_$i_1') ).
tff(declare_p220,type,
p220: $i > $o ).
tff(predicate_p220,axiom,
p220('fmb_$i_1') ).
tff(declare_p120,type,
p120: $i > $o ).
tff(predicate_p120,axiom,
~ p120('fmb_$i_1') ).
tff(declare_p2119,type,
p2119: $i > $o ).
tff(predicate_p2119,axiom,
~ p2119('fmb_$i_1') ).
tff(declare_p2019,type,
p2019: $i > $o ).
tff(predicate_p2019,axiom,
~ p2019('fmb_$i_1') ).
tff(declare_p1919,type,
p1919: $i > $o ).
tff(predicate_p1919,axiom,
~ p1919('fmb_$i_1') ).
tff(declare_p1819,type,
p1819: $i > $o ).
tff(predicate_p1819,axiom,
~ p1819('fmb_$i_1') ).
tff(declare_p1719,type,
p1719: $i > $o ).
tff(predicate_p1719,axiom,
~ p1719('fmb_$i_1') ).
tff(declare_p1619,type,
p1619: $i > $o ).
tff(predicate_p1619,axiom,
~ p1619('fmb_$i_1') ).
tff(declare_p1519,type,
p1519: $i > $o ).
tff(predicate_p1519,axiom,
~ p1519('fmb_$i_1') ).
tff(declare_p1419,type,
p1419: $i > $o ).
tff(predicate_p1419,axiom,
~ p1419('fmb_$i_1') ).
tff(declare_p1319,type,
p1319: $i > $o ).
tff(predicate_p1319,axiom,
~ p1319('fmb_$i_1') ).
tff(declare_p1219,type,
p1219: $i > $o ).
tff(predicate_p1219,axiom,
~ p1219('fmb_$i_1') ).
tff(declare_p1119,type,
p1119: $i > $o ).
tff(predicate_p1119,axiom,
~ p1119('fmb_$i_1') ).
tff(declare_p1019,type,
p1019: $i > $o ).
tff(predicate_p1019,axiom,
~ p1019('fmb_$i_1') ).
tff(declare_p919,type,
p919: $i > $o ).
tff(predicate_p919,axiom,
~ p919('fmb_$i_1') ).
tff(declare_p819,type,
p819: $i > $o ).
tff(predicate_p819,axiom,
p819('fmb_$i_1') ).
tff(declare_p719,type,
p719: $i > $o ).
tff(predicate_p719,axiom,
~ p719('fmb_$i_1') ).
tff(declare_p619,type,
p619: $i > $o ).
tff(predicate_p619,axiom,
~ p619('fmb_$i_1') ).
tff(declare_p519,type,
p519: $i > $o ).
tff(predicate_p519,axiom,
~ p519('fmb_$i_1') ).
tff(declare_p419,type,
p419: $i > $o ).
tff(predicate_p419,axiom,
~ p419('fmb_$i_1') ).
tff(declare_p319,type,
p319: $i > $o ).
tff(predicate_p319,axiom,
~ p319('fmb_$i_1') ).
tff(declare_p219,type,
p219: $i > $o ).
tff(predicate_p219,axiom,
~ p219('fmb_$i_1') ).
tff(declare_p119,type,
p119: $i > $o ).
tff(predicate_p119,axiom,
~ p119('fmb_$i_1') ).
tff(declare_p2118,type,
p2118: $i > $o ).
tff(predicate_p2118,axiom,
~ p2118('fmb_$i_1') ).
tff(declare_p2018,type,
p2018: $i > $o ).
tff(predicate_p2018,axiom,
~ p2018('fmb_$i_1') ).
tff(declare_p1918,type,
p1918: $i > $o ).
tff(predicate_p1918,axiom,
~ p1918('fmb_$i_1') ).
tff(declare_p1818,type,
p1818: $i > $o ).
tff(predicate_p1818,axiom,
~ p1818('fmb_$i_1') ).
tff(declare_p1718,type,
p1718: $i > $o ).
tff(predicate_p1718,axiom,
~ p1718('fmb_$i_1') ).
tff(declare_p1618,type,
p1618: $i > $o ).
tff(predicate_p1618,axiom,
~ p1618('fmb_$i_1') ).
tff(declare_p1518,type,
p1518: $i > $o ).
tff(predicate_p1518,axiom,
~ p1518('fmb_$i_1') ).
tff(declare_p1418,type,
p1418: $i > $o ).
tff(predicate_p1418,axiom,
~ p1418('fmb_$i_1') ).
tff(declare_p1318,type,
p1318: $i > $o ).
tff(predicate_p1318,axiom,
~ p1318('fmb_$i_1') ).
tff(declare_p1218,type,
p1218: $i > $o ).
tff(predicate_p1218,axiom,
~ p1218('fmb_$i_1') ).
tff(declare_p1118,type,
p1118: $i > $o ).
tff(predicate_p1118,axiom,
~ p1118('fmb_$i_1') ).
tff(declare_p1018,type,
p1018: $i > $o ).
tff(predicate_p1018,axiom,
~ p1018('fmb_$i_1') ).
tff(declare_p918,type,
p918: $i > $o ).
tff(predicate_p918,axiom,
~ p918('fmb_$i_1') ).
tff(declare_p818,type,
p818: $i > $o ).
tff(predicate_p818,axiom,
~ p818('fmb_$i_1') ).
tff(declare_p718,type,
p718: $i > $o ).
tff(predicate_p718,axiom,
~ p718('fmb_$i_1') ).
tff(declare_p618,type,
p618: $i > $o ).
tff(predicate_p618,axiom,
p618('fmb_$i_1') ).
tff(declare_p518,type,
p518: $i > $o ).
tff(predicate_p518,axiom,
~ p518('fmb_$i_1') ).
tff(declare_p418,type,
p418: $i > $o ).
tff(predicate_p418,axiom,
~ p418('fmb_$i_1') ).
tff(declare_p318,type,
p318: $i > $o ).
tff(predicate_p318,axiom,
~ p318('fmb_$i_1') ).
tff(declare_p218,type,
p218: $i > $o ).
tff(predicate_p218,axiom,
~ p218('fmb_$i_1') ).
tff(declare_p118,type,
p118: $i > $o ).
tff(predicate_p118,axiom,
~ p118('fmb_$i_1') ).
tff(declare_p2117,type,
p2117: $i > $o ).
tff(predicate_p2117,axiom,
~ p2117('fmb_$i_1') ).
tff(declare_p2017,type,
p2017: $i > $o ).
tff(predicate_p2017,axiom,
~ p2017('fmb_$i_1') ).
tff(declare_p1917,type,
p1917: $i > $o ).
tff(predicate_p1917,axiom,
~ p1917('fmb_$i_1') ).
tff(declare_p1817,type,
p1817: $i > $o ).
tff(predicate_p1817,axiom,
p1817('fmb_$i_1') ).
tff(declare_p1717,type,
p1717: $i > $o ).
tff(predicate_p1717,axiom,
~ p1717('fmb_$i_1') ).
tff(declare_p1617,type,
p1617: $i > $o ).
tff(predicate_p1617,axiom,
~ p1617('fmb_$i_1') ).
tff(declare_p1517,type,
p1517: $i > $o ).
tff(predicate_p1517,axiom,
~ p1517('fmb_$i_1') ).
tff(declare_p1417,type,
p1417: $i > $o ).
tff(predicate_p1417,axiom,
~ p1417('fmb_$i_1') ).
tff(declare_p1317,type,
p1317: $i > $o ).
tff(predicate_p1317,axiom,
~ p1317('fmb_$i_1') ).
tff(declare_p1217,type,
p1217: $i > $o ).
tff(predicate_p1217,axiom,
~ p1217('fmb_$i_1') ).
tff(declare_p1117,type,
p1117: $i > $o ).
tff(predicate_p1117,axiom,
~ p1117('fmb_$i_1') ).
tff(declare_p1017,type,
p1017: $i > $o ).
tff(predicate_p1017,axiom,
~ p1017('fmb_$i_1') ).
tff(declare_p917,type,
p917: $i > $o ).
tff(predicate_p917,axiom,
~ p917('fmb_$i_1') ).
tff(declare_p817,type,
p817: $i > $o ).
tff(predicate_p817,axiom,
~ p817('fmb_$i_1') ).
tff(declare_p717,type,
p717: $i > $o ).
tff(predicate_p717,axiom,
~ p717('fmb_$i_1') ).
tff(declare_p617,type,
p617: $i > $o ).
tff(predicate_p617,axiom,
~ p617('fmb_$i_1') ).
tff(declare_p517,type,
p517: $i > $o ).
tff(predicate_p517,axiom,
~ p517('fmb_$i_1') ).
tff(declare_p417,type,
p417: $i > $o ).
tff(predicate_p417,axiom,
~ p417('fmb_$i_1') ).
tff(declare_p317,type,
p317: $i > $o ).
tff(predicate_p317,axiom,
~ p317('fmb_$i_1') ).
tff(declare_p217,type,
p217: $i > $o ).
tff(predicate_p217,axiom,
~ p217('fmb_$i_1') ).
tff(declare_p117,type,
p117: $i > $o ).
tff(predicate_p117,axiom,
~ p117('fmb_$i_1') ).
tff(declare_p2116,type,
p2116: $i > $o ).
tff(predicate_p2116,axiom,
~ p2116('fmb_$i_1') ).
tff(declare_p2016,type,
p2016: $i > $o ).
tff(predicate_p2016,axiom,
~ p2016('fmb_$i_1') ).
tff(declare_p1916,type,
p1916: $i > $o ).
tff(predicate_p1916,axiom,
~ p1916('fmb_$i_1') ).
tff(declare_p1816,type,
p1816: $i > $o ).
tff(predicate_p1816,axiom,
~ p1816('fmb_$i_1') ).
tff(declare_p1716,type,
p1716: $i > $o ).
tff(predicate_p1716,axiom,
~ p1716('fmb_$i_1') ).
tff(declare_p1616,type,
p1616: $i > $o ).
tff(predicate_p1616,axiom,
~ p1616('fmb_$i_1') ).
tff(declare_p1516,type,
p1516: $i > $o ).
tff(predicate_p1516,axiom,
~ p1516('fmb_$i_1') ).
tff(declare_p1416,type,
p1416: $i > $o ).
tff(predicate_p1416,axiom,
~ p1416('fmb_$i_1') ).
tff(declare_p1316,type,
p1316: $i > $o ).
tff(predicate_p1316,axiom,
~ p1316('fmb_$i_1') ).
tff(declare_p1216,type,
p1216: $i > $o ).
tff(predicate_p1216,axiom,
~ p1216('fmb_$i_1') ).
tff(declare_p1116,type,
p1116: $i > $o ).
tff(predicate_p1116,axiom,
~ p1116('fmb_$i_1') ).
tff(declare_p1016,type,
p1016: $i > $o ).
tff(predicate_p1016,axiom,
~ p1016('fmb_$i_1') ).
tff(declare_p916,type,
p916: $i > $o ).
tff(predicate_p916,axiom,
~ p916('fmb_$i_1') ).
tff(declare_p816,type,
p816: $i > $o ).
tff(predicate_p816,axiom,
~ p816('fmb_$i_1') ).
tff(declare_p716,type,
p716: $i > $o ).
tff(predicate_p716,axiom,
~ p716('fmb_$i_1') ).
tff(declare_p616,type,
p616: $i > $o ).
tff(predicate_p616,axiom,
~ p616('fmb_$i_1') ).
tff(declare_p516,type,
p516: $i > $o ).
tff(predicate_p516,axiom,
p516('fmb_$i_1') ).
tff(declare_p416,type,
p416: $i > $o ).
tff(predicate_p416,axiom,
~ p416('fmb_$i_1') ).
tff(declare_p316,type,
p316: $i > $o ).
tff(predicate_p316,axiom,
~ p316('fmb_$i_1') ).
tff(declare_p216,type,
p216: $i > $o ).
tff(predicate_p216,axiom,
~ p216('fmb_$i_1') ).
tff(declare_p116,type,
p116: $i > $o ).
tff(predicate_p116,axiom,
~ p116('fmb_$i_1') ).
tff(declare_p2115,type,
p2115: $i > $o ).
tff(predicate_p2115,axiom,
~ p2115('fmb_$i_1') ).
tff(declare_p2015,type,
p2015: $i > $o ).
tff(predicate_p2015,axiom,
~ p2015('fmb_$i_1') ).
tff(declare_p1915,type,
p1915: $i > $o ).
tff(predicate_p1915,axiom,
~ p1915('fmb_$i_1') ).
tff(declare_p1815,type,
p1815: $i > $o ).
tff(predicate_p1815,axiom,
~ p1815('fmb_$i_1') ).
tff(declare_p1715,type,
p1715: $i > $o ).
tff(predicate_p1715,axiom,
~ p1715('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_p2114,type,
p2114: $i > $o ).
tff(predicate_p2114,axiom,
~ p2114('fmb_$i_1') ).
tff(declare_p2014,type,
p2014: $i > $o ).
tff(predicate_p2014,axiom,
~ p2014('fmb_$i_1') ).
tff(declare_p1914,type,
p1914: $i > $o ).
tff(predicate_p1914,axiom,
~ p1914('fmb_$i_1') ).
tff(declare_p1814,type,
p1814: $i > $o ).
tff(predicate_p1814,axiom,
~ p1814('fmb_$i_1') ).
tff(declare_p1714,type,
p1714: $i > $o ).
tff(predicate_p1714,axiom,
~ p1714('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_p2113,type,
p2113: $i > $o ).
tff(predicate_p2113,axiom,
p2113('fmb_$i_1') ).
tff(declare_p2013,type,
p2013: $i > $o ).
tff(predicate_p2013,axiom,
~ p2013('fmb_$i_1') ).
tff(declare_p1913,type,
p1913: $i > $o ).
tff(predicate_p1913,axiom,
~ p1913('fmb_$i_1') ).
tff(declare_p1813,type,
p1813: $i > $o ).
tff(predicate_p1813,axiom,
~ p1813('fmb_$i_1') ).
tff(declare_p1713,type,
p1713: $i > $o ).
tff(predicate_p1713,axiom,
~ p1713('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_p2112,type,
p2112: $i > $o ).
tff(predicate_p2112,axiom,
~ p2112('fmb_$i_1') ).
tff(declare_p2012,type,
p2012: $i > $o ).
tff(predicate_p2012,axiom,
~ p2012('fmb_$i_1') ).
tff(declare_p1912,type,
p1912: $i > $o ).
tff(predicate_p1912,axiom,
p1912('fmb_$i_1') ).
tff(declare_p1812,type,
p1812: $i > $o ).
tff(predicate_p1812,axiom,
~ p1812('fmb_$i_1') ).
tff(declare_p1712,type,
p1712: $i > $o ).
tff(predicate_p1712,axiom,
~ p1712('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_p2111,type,
p2111: $i > $o ).
tff(predicate_p2111,axiom,
~ p2111('fmb_$i_1') ).
tff(declare_p2011,type,
p2011: $i > $o ).
tff(predicate_p2011,axiom,
p2011('fmb_$i_1') ).
tff(declare_p1911,type,
p1911: $i > $o ).
tff(predicate_p1911,axiom,
~ p1911('fmb_$i_1') ).
tff(declare_p1811,type,
p1811: $i > $o ).
tff(predicate_p1811,axiom,
~ p1811('fmb_$i_1') ).
tff(declare_p1711,type,
p1711: $i > $o ).
tff(predicate_p1711,axiom,
~ p1711('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_p2110,type,
p2110: $i > $o ).
tff(predicate_p2110,axiom,
~ p2110('fmb_$i_1') ).
tff(declare_p2010,type,
p2010: $i > $o ).
tff(predicate_p2010,axiom,
~ p2010('fmb_$i_1') ).
tff(declare_p1910,type,
p1910: $i > $o ).
tff(predicate_p1910,axiom,
~ p1910('fmb_$i_1') ).
tff(declare_p1810,type,
p1810: $i > $o ).
tff(predicate_p1810,axiom,
~ p1810('fmb_$i_1') ).
tff(declare_p1710,type,
p1710: $i > $o ).
tff(predicate_p1710,axiom,
~ p1710('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_p2109,type,
p2109: $i > $o ).
tff(predicate_p2109,axiom,
~ p2109('fmb_$i_1') ).
tff(declare_p2009,type,
p2009: $i > $o ).
tff(predicate_p2009,axiom,
~ p2009('fmb_$i_1') ).
tff(declare_p1909,type,
p1909: $i > $o ).
tff(predicate_p1909,axiom,
~ p1909('fmb_$i_1') ).
tff(declare_p1809,type,
p1809: $i > $o ).
tff(predicate_p1809,axiom,
~ p1809('fmb_$i_1') ).
tff(declare_p1709,type,
p1709: $i > $o ).
tff(predicate_p1709,axiom,
~ p1709('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_p2108,type,
p2108: $i > $o ).
tff(predicate_p2108,axiom,
~ p2108('fmb_$i_1') ).
tff(declare_p2008,type,
p2008: $i > $o ).
tff(predicate_p2008,axiom,
~ p2008('fmb_$i_1') ).
tff(declare_p1908,type,
p1908: $i > $o ).
tff(predicate_p1908,axiom,
~ p1908('fmb_$i_1') ).
tff(declare_p1808,type,
p1808: $i > $o ).
tff(predicate_p1808,axiom,
~ p1808('fmb_$i_1') ).
tff(declare_p1708,type,
p1708: $i > $o ).
tff(predicate_p1708,axiom,
p1708('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_p2107,type,
p2107: $i > $o ).
tff(predicate_p2107,axiom,
~ p2107('fmb_$i_1') ).
tff(declare_p2007,type,
p2007: $i > $o ).
tff(predicate_p2007,axiom,
~ p2007('fmb_$i_1') ).
tff(declare_p1907,type,
p1907: $i > $o ).
tff(predicate_p1907,axiom,
~ p1907('fmb_$i_1') ).
tff(declare_p1807,type,
p1807: $i > $o ).
tff(predicate_p1807,axiom,
~ p1807('fmb_$i_1') ).
tff(declare_p1707,type,
p1707: $i > $o ).
tff(predicate_p1707,axiom,
~ p1707('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_p2106,type,
p2106: $i > $o ).
tff(predicate_p2106,axiom,
~ p2106('fmb_$i_1') ).
tff(declare_p2006,type,
p2006: $i > $o ).
tff(predicate_p2006,axiom,
~ p2006('fmb_$i_1') ).
tff(declare_p1906,type,
p1906: $i > $o ).
tff(predicate_p1906,axiom,
~ p1906('fmb_$i_1') ).
tff(declare_p1806,type,
p1806: $i > $o ).
tff(predicate_p1806,axiom,
~ p1806('fmb_$i_1') ).
tff(declare_p1706,type,
p1706: $i > $o ).
tff(predicate_p1706,axiom,
~ p1706('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_p2105,type,
p2105: $i > $o ).
tff(predicate_p2105,axiom,
~ p2105('fmb_$i_1') ).
tff(declare_p2005,type,
p2005: $i > $o ).
tff(predicate_p2005,axiom,
~ p2005('fmb_$i_1') ).
tff(declare_p1905,type,
p1905: $i > $o ).
tff(predicate_p1905,axiom,
~ p1905('fmb_$i_1') ).
tff(declare_p1805,type,
p1805: $i > $o ).
tff(predicate_p1805,axiom,
~ p1805('fmb_$i_1') ).
tff(declare_p1705,type,
p1705: $i > $o ).
tff(predicate_p1705,axiom,
~ p1705('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_p2104,type,
p2104: $i > $o ).
tff(predicate_p2104,axiom,
~ p2104('fmb_$i_1') ).
tff(declare_p2004,type,
p2004: $i > $o ).
tff(predicate_p2004,axiom,
~ p2004('fmb_$i_1') ).
tff(declare_p1904,type,
p1904: $i > $o ).
tff(predicate_p1904,axiom,
~ p1904('fmb_$i_1') ).
tff(declare_p1804,type,
p1804: $i > $o ).
tff(predicate_p1804,axiom,
~ p1804('fmb_$i_1') ).
tff(declare_p1704,type,
p1704: $i > $o ).
tff(predicate_p1704,axiom,
~ p1704('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_p2103,type,
p2103: $i > $o ).
tff(predicate_p2103,axiom,
~ p2103('fmb_$i_1') ).
tff(declare_p2003,type,
p2003: $i > $o ).
tff(predicate_p2003,axiom,
~ p2003('fmb_$i_1') ).
tff(declare_p1903,type,
p1903: $i > $o ).
tff(predicate_p1903,axiom,
~ p1903('fmb_$i_1') ).
tff(declare_p1803,type,
p1803: $i > $o ).
tff(predicate_p1803,axiom,
~ p1803('fmb_$i_1') ).
tff(declare_p1703,type,
p1703: $i > $o ).
tff(predicate_p1703,axiom,
~ p1703('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_p2102,type,
p2102: $i > $o ).
tff(predicate_p2102,axiom,
~ p2102('fmb_$i_1') ).
tff(declare_p2002,type,
p2002: $i > $o ).
tff(predicate_p2002,axiom,
~ p2002('fmb_$i_1') ).
tff(declare_p1902,type,
p1902: $i > $o ).
tff(predicate_p1902,axiom,
~ p1902('fmb_$i_1') ).
tff(declare_p1802,type,
p1802: $i > $o ).
tff(predicate_p1802,axiom,
~ p1802('fmb_$i_1') ).
tff(declare_p1702,type,
p1702: $i > $o ).
tff(predicate_p1702,axiom,
~ p1702('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_p2101,type,
p2101: $i > $o ).
tff(predicate_p2101,axiom,
~ p2101('fmb_$i_1') ).
tff(declare_p2001,type,
p2001: $i > $o ).
tff(predicate_p2001,axiom,
~ p2001('fmb_$i_1') ).
tff(declare_p1901,type,
p1901: $i > $o ).
tff(predicate_p1901,axiom,
~ p1901('fmb_$i_1') ).
tff(declare_p1801,type,
p1801: $i > $o ).
tff(predicate_p1801,axiom,
~ p1801('fmb_$i_1') ).
tff(declare_p1701,type,
p1701: $i > $o ).
tff(predicate_p1701,axiom,
~ p1701('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.03 % Problem : LCL667+1.020 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.18/0.42 % Computer : n011.cluster.edu
% 0.18/0.42 % Model : x86_64 x86_64
% 0.18/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.42 % Memory : 8046.5625MB
% 0.18/0.42 % OS : Linux 6.8.0-71-generic
% 0.18/0.42 % CPULimit : 300
% 0.18/0.42 % WCLimit : 300
% 0.18/0.42 % DateTime : Sun Sep 27 16:27:45 UTC 2026
% 0.18/0.42 % CPUTime :
% 0.18/0.42 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.25/0.47 Running first-order model finding
% 0.25/0.47 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
% 13.78/2.77 % (2600439)Will run a generic schedule for satisfiability detection.
% 13.78/2.77 % (2600446)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=331677435:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 13.78/2.77 % (2600444)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=597805218_2999 on theBenchmark for (2999ds/0Mi)
% 13.78/2.77 % (2600445)% WARNING: option uhcvi not known.
% 13.78/2.77 % (2600448)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2499140201:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 13.78/2.77 % (2600447)dis+10_1_sil=32000:sp=arity:random_seed=779397914:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 13.78/2.77 % (2600445)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=400844117:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 13.78/2.77 % (2600449)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3226489784:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 13.78/2.77 % (2600450)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=647046886:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 13.78/2.77 % (2600447)Instruction limit reached!
% 13.78/2.77 % (2600447)------------------------------
% 13.78/2.77 % (2600447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.78/2.77 % (2600447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.78/2.77 % (2600447)CaDiCaL version: 2.1.3
% 13.78/2.77 % (2600447)Termination reason: Instruction limit
% 13.78/2.77 % (2600447)Termination phase: Unused predicate definition removal
% 13.78/2.77 % (2600447)Time elapsed: 0.083 s
% 13.78/2.77 % (2600447)Peak memory usage: 14 MB
% 13.78/2.77 % (2600447)Instructions burned: 103 (million)
% 13.78/2.77 % (2600448)Instruction limit reached!
% 13.78/2.77 % (2600448)------------------------------
% 13.78/2.77 % (2600448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.78/2.77 % (2600448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.78/2.77 % (2600448)CaDiCaL version: 2.1.3
% 13.78/2.77 % (2600448)Termination reason: Instruction limit
% 13.78/2.77 % (2600448)Termination phase: Unused predicate definition removal
% 13.78/2.77 % (2600448)Time elapsed: 0.095 s
% 13.78/2.77 % (2600448)Peak memory usage: 15 MB
% 13.78/2.77 % (2600448)Instructions burned: 117 (million)
% 13.78/2.77 % (2600449)Instruction limit reached!
% 13.78/2.77 % (2600449)------------------------------
% 13.78/2.77 % (2600449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.78/2.77 % (2600449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.78/2.77 % (2600449)CaDiCaL version: 2.1.3
% 13.78/2.77 % (2600449)Termination reason: Instruction limit
% 13.78/2.77 % (2600449)Termination phase: Unused predicate definition removal
% 13.78/2.77 % (2600449)Time elapsed: 0.105 s
% 13.78/2.77 % (2600449)Peak memory usage: 15 MB
% 13.78/2.77 % (2600449)Instructions burned: 132 (million)
% 13.78/2.77 % (2600458)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=694279915:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 13.78/2.77 % (2600459)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2998882003:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 13.78/2.77 % (2600450)Instruction limit reached!
% 13.78/2.77 % (2600450)------------------------------
% 13.78/2.77 % (2600450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.78/2.77 % (2600450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.78/2.77 % (2600450)CaDiCaL version: 2.1.3
% 13.78/2.77 % (2600450)Termination reason: Instruction limit
% 13.78/2.77 % (2600450)Termination phase: Naming
% 13.78/2.77 % (2600450)Time elapsed: 0.134 s
% 13.78/2.77 % (2600450)Peak memory usage: 17 MB
% 13.78/2.77 % (2600450)Instructions burned: 159 (million)
% 13.78/2.77 % (2600460)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=3669097075:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 13.78/2.77 % (2600463)ott-21_1_sil=16000:fs=off:random_seed=2612265645:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 13.78/2.77 % (2600459)Instruction limit reached!
% 13.78/2.77 % (2600459)------------------------------
% 13.78/2.77 % (2600459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.78/2.77 % (2600459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.78/2.77 % (2600459)CaDiCaL version: 2.1.3
% 13.78/2.77 % (2600459)Termination reason: Instruction limit
% 13.78/2.77 % (2600459)Termination phase: Unused predicate definition removal
% 13.78/2.77 % (2600459)Time elapsed: 0.106 s
% 13.78/2.77 % (2600459)Peak memory usage: 15 MB
% 13.78/2.77 % (2600459)Instructions burned: 133 (million)
% 13.78/2.77 % (2600466)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1414051883:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 13.78/2.77 % (2600463)Instruction limit reached!
% 13.78/2.77 % (2600463)------------------------------
% 13.78/2.77 % (2600463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.78/2.77 % (2600463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.78/2.77 % (2600463)CaDiCaL version: 2.1.3
% 13.78/2.77 % (2600463)Termination reason: Instruction limit
% 13.78/2.77 % (2600463)Termination phase: Naming
% 13.78/2.77 % (2600463)Time elapsed: 0.154 s
% 13.78/2.77 % (2600463)Peak memory usage: 18 MB
% 13.78/2.77 % (2600463)Instructions burned: 180 (million)
% 13.78/2.77 % (2600469)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1950181369:fmbsr=1.3:i=865:ins=25_2995 on theBenchmark for (2995ds/865Mi)
% 13.78/2.77 % (2600458)Instruction limit reached!
% 13.78/2.77 % (2600458)------------------------------
% 13.78/2.77 % (2600458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.78/2.77 % (2600458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.78/2.77 % (2600458)CaDiCaL version: 2.1.3
% 13.78/2.77 % (2600458)Termination reason: Instruction limit
% 13.78/2.77 % (2600458)Termination phase: Finite model building preprocessing
% 13.78/2.77 % (2600458)Time elapsed: 0.498 s
% 13.78/2.77 % (2600458)Peak memory usage: 34 MB
% 13.78/2.77 % (2600458)Instructions burned: 715 (million)
% 13.78/2.77 % (2600466)Instruction limit reached!
% 13.78/2.77 % (2600466)------------------------------
% 13.78/2.77 % (2600466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.78/2.77 % (2600466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.78/2.77 % (2600466)CaDiCaL version: 2.1.3
% 13.78/2.77 % (2600466)Termination reason: Instruction limit
% 13.78/2.77 % (2600466)Termination phase: Preprocessing 3
% 13.78/2.77 % (2600466)Time elapsed: 0.347 s
% 13.78/2.77 % (2600466)Peak memory usage: 23 MB
% 13.78/2.77 % (2600466)Instructions burned: 477 (million)
% 13.78/2.77 % (2600472)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1738213310:i=1179_2992 on theBenchmark for (2992ds/1179Mi)
% 13.78/2.77 % (2600473)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=47708292:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 13.78/2.77 % (2600460)Instruction limit reached!
% 13.78/2.77 % (2600460)------------------------------
% 13.78/2.77 % (2600460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.78/2.77 % (2600460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.78/2.77 % (2600460)CaDiCaL version: 2.1.3
% 13.78/2.77 % (2600460)Termination reason: Instruction limit
% 13.78/2.77 % (2600460)Termination phase: Saturation
% 13.78/2.77 % (2600460)Time elapsed: 0.608 s
% 13.78/2.77 % (2600460)Peak memory usage: 32 MB
% 13.78/2.77 % (2600460)Instructions burned: 684 (million)
% 13.78/2.77 % (2600476)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=246591876:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 13.78/2.77 % (2600469)Instruction limit reached!
% 13.78/2.77 % (2600469)------------------------------
% 13.78/2.77 % (2600469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.78/2.77 % (2600469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.78/2.77 % (2600469)CaDiCaL version: 2.1.3
% 13.78/2.77 % (2600469)Termination reason: Instruction limit
% 13.78/2.77 % (2600469)Termination phase: Finite model building preprocessing
% 13.78/2.77 % (2600469)Time elapsed: 0.676 s
% 13.78/2.77 % (2600469)Peak memory usage: 35 MB
% 13.78/2.77 % (2600469)Instructions burned: 865 (million)
% 13.78/2.77 % (2600478)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2079193758:i=879:kws=inv_precedence:fsr=off_2988 on theBenchmark for (2988ds/879Mi)
% 13.78/2.77 % (2600473)Instruction limit reached!
% 13.78/2.77 % (2600473)------------------------------
% 13.78/2.77 % (2600473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.78/2.77 % (2600473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.78/2.77 % (2600473)CaDiCaL version: 2.1.3
% 13.78/2.77 % (2600473)Termination reason: Instruction limit
% 13.78/2.77 % (2600473)Termination phase: Finite model building preprocessing
% 13.78/2.77 % (2600473)Time elapsed: 0.651 s
% 13.78/2.77 % (2600473)Peak memory usage: 34 MB
% 13.78/2.77 % (2600473)Instructions burned: 889 (million)
% 13.78/2.77 % TRYING [1]
% 13.78/2.77 % (2600480)fmb+10_1_sil=64000:random_seed=691283196:i=22061:nm=2:gsp=on_2985 on theBenchmark for (2985ds/22061Mi)
% 13.78/2.77 % (2600476)Instruction limit reached!
% 13.78/2.77 % (2600476)------------------------------
% 13.78/2.77 % (2600476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.78/2.77 % (2600476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.78/2.77 % (2600476)CaDiCaL version: 2.1.3
% 13.78/2.77 % (2600476)Termination reason: Instruction limit
% 13.78/2.77 % (2600476)Termination phase: Saturation
% 13.78/2.77 % (2600476)Time elapsed: 0.617 s
% 13.78/2.77 % (2600476)Peak memory usage: 34 MB
% 13.78/2.77 % (2600476)Instructions burned: 693 (million)
% 13.78/2.77 % (2600482)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=98755697:i=9515:nm=5_2984 on theBenchmark for (2984ds/9515Mi)
% 13.78/2.77 % (2600472)Instruction limit reached!
% 13.78/2.77 % (2600472)------------------------------
% 13.78/2.77 % (2600472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.78/2.77 % (2600472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.78/2.77 % (2600472)CaDiCaL version: 2.1.3
% 13.78/2.77 % (2600472)Termination reason: Instruction limit
% 13.78/2.77 % (2600472)Termination phase: Saturation
% 13.78/2.77 % (2600472)Time elapsed: 0.917 s
% 13.78/2.77 % (2600472)Peak memory usage: 46 MB
% 13.78/2.77 % (2600472)Instructions burned: 1179 (million)
% 13.78/2.77 % (2600484)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4017119528:fmbsr=1.7:i=920_2983 on theBenchmark for (2983ds/920Mi)
% 13.78/2.77 % (2600478)Instruction limit reached!
% 13.78/2.77 % (2600478)------------------------------
% 13.78/2.77 % (2600478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.78/2.77 % (2600478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.78/2.77 % (2600478)CaDiCaL version: 2.1.3
% 13.78/2.77 % (2600478)Termination reason: Instruction limit
% 13.78/2.77 % (2600478)Termination phase: Saturation
% 13.78/2.77 % (2600478)Time elapsed: 0.684 s
% 13.78/2.77 % (2600478)Peak memory usage: 35 MB
% 13.78/2.77 % (2600478)Instructions burned: 879 (million)
% 13.78/2.77 % (2600486)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1660436520:i=5131_2980 on theBenchmark for (2980ds/5131Mi)
% 13.78/2.77 % Finite Model Found!
% 13.78/2.77 % SZS status CounterSatisfiable for theBenchmark
% 13.78/2.77 % (2600444) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2600439-2600444"...
% 13.78/2.77 % (2600444)...printing done.
% 13.78/2.77 % SZS output start FiniteModel for theBenchmark
% See solution above
% 13.78/2.78 % (2600444)------------------------------
% 13.78/2.78 % (2600444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.78/2.78 % (2600444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.78/2.78 % (2600444)CaDiCaL version: 2.1.3
% 13.78/2.78 % (2600444)Termination reason: Satisfiable
% 13.78/2.78 % (2600444)Time elapsed: 2.127 s
% 13.78/2.78 % (2600444)Peak memory usage: 51 MB
% 13.78/2.78 % (2600444)Instructions burned: 2780 (million)
% 13.78/2.78 % (2600439)Success in time 2.282 s
% 13.78/2.78 % Vampire exiting
%------------------------------------------------------------------------------