%------------------------------------------------------------------------------
% File : FMB4J---0.1
% Problem : LCL685+1.020 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:04:50 PM UTC 2026
% Result : CounterSatisfiable 5.75s 2.69s
% Output : FiniteModel 6.21s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(domain,interpretation-domains,
! [X] : X = "d0" ).
fof(mappings,interpretation-mappings,
$true ).
fof(predicate_mappings,interpretation-mappings,
( ~ p520("d0")
& ~ p509("d0")
& ~ p508("d0")
& ~ p507("d0")
& ~ p506("d0")
& p505("d0")
& ~ p504("d0")
& ~ p503("d0")
& ~ p502("d0")
& ~ p501("d0")
& ~ p519("d0")
& ~ p518("d0")
& ~ p517("d0")
& ~ p516("d0")
& ~ p515("d0")
& ~ p514("d0")
& ~ p513("d0")
& ~ p512("d0")
& ~ p511("d0")
& ~ p510("d0")
& ~ p420("d0")
& ~ p409("d0")
& ~ p408("d0")
& ~ p407("d0")
& ~ p406("d0")
& ~ p405("d0")
& p404("d0")
& ~ p403("d0")
& ~ p402("d0")
& ~ p401("d0")
& ~ p419("d0")
& ~ p418("d0")
& ~ p417("d0")
& ~ p416("d0")
& ~ p415("d0")
& ~ p414("d0")
& ~ p413("d0")
& ~ p412("d0")
& ~ p411("d0")
& ~ p410("d0")
& ~ p720("d0")
& ~ p708("d0")
& p707("d0")
& ~ p706("d0")
& ~ p705("d0")
& ~ p704("d0")
& ~ p703("d0")
& ~ p702("d0")
& ~ p701("d0")
& ~ p709("d0")
& ~ p719("d0")
& ~ p718("d0")
& ~ p717("d0")
& ~ p716("d0")
& ~ p715("d0")
& ~ p714("d0")
& ~ p713("d0")
& ~ p712("d0")
& ~ p711("d0")
& ~ p710("d0")
& ~ p2007("d0")
& ~ p2006("d0")
& ~ p2009("d0")
& ~ p2008("d0")
& ~ p2003("d0")
& ~ p2002("d0")
& ~ p2005("d0")
& ~ p2004("d0")
& ~ p2001("d0")
& p2020("d0")
& ~ p2018("d0")
& ~ p2017("d0")
& ~ p2019("d0")
& ~ p2014("d0")
& ~ p2013("d0")
& ~ p2016("d0")
& ~ p2015("d0")
& ~ p2010("d0")
& ~ p2012("d0")
& ~ p2011("d0")
& ~ p609("d0")
& ~ p608("d0")
& ~ p607("d0")
& p606("d0")
& ~ p605("d0")
& ~ p604("d0")
& ~ p603("d0")
& ~ p602("d0")
& ~ p601("d0")
& ~ p619("d0")
& ~ p618("d0")
& ~ p617("d0")
& ~ p616("d0")
& ~ p615("d0")
& ~ p614("d0")
& ~ p613("d0")
& ~ p612("d0")
& ~ p611("d0")
& ~ p610("d0")
& ~ p620("d0")
& ~ p109("d0")
& ~ p108("d0")
& ~ p107("d0")
& ~ p106("d0")
& ~ p105("d0")
& ~ p104("d0")
& ~ p103("d0")
& ~ p102("d0")
& p101("d0")
& ~ p119("d0")
& ~ p118("d0")
& ~ p117("d0")
& ~ p116("d0")
& ~ p115("d0")
& ~ p114("d0")
& ~ p113("d0")
& ~ p112("d0")
& ~ p111("d0")
& ~ p110("d0")
& ~ p120("d0")
& ~ p1718("d0")
& ~ p1717("d0")
& ~ p1719("d0")
& ~ p1714("d0")
& ~ p1713("d0")
& p1716("d0")
& ~ p1715("d0")
& ~ p1710("d0")
& ~ p1712("d0")
& ~ p1711("d0")
& ~ p1707("d0")
& ~ p1706("d0")
& ~ p1709("d0")
& ~ p1708("d0")
& ~ p1703("d0")
& ~ p1702("d0")
& ~ p1705("d0")
& ~ p1704("d0")
& ~ p1701("d0")
& ~ p1720("d0")
& ~ p1820("d0")
& p1817("d0")
& ~ p1816("d0")
& ~ p1819("d0")
& ~ p1818("d0")
& ~ p1813("d0")
& ~ p1812("d0")
& ~ p1815("d0")
& ~ p1814("d0")
& ~ p1811("d0")
& ~ p1810("d0")
& ~ p1809("d0")
& ~ p1806("d0")
& ~ p1805("d0")
& ~ p1808("d0")
& ~ p1807("d0")
& ~ p1802("d0")
& ~ p1801("d0")
& ~ p1804("d0")
& ~ p1803("d0")
& ~ p320("d0")
& ~ p309("d0")
& ~ p308("d0")
& ~ p307("d0")
& ~ p306("d0")
& ~ p305("d0")
& ~ p304("d0")
& p303("d0")
& ~ p302("d0")
& ~ p301("d0")
& ~ p319("d0")
& ~ p318("d0")
& ~ p317("d0")
& ~ p316("d0")
& ~ p315("d0")
& ~ p314("d0")
& ~ p313("d0")
& ~ p312("d0")
& ~ p311("d0")
& ~ p310("d0")
& ~ p1916("d0")
& ~ p1915("d0")
& ~ p1918("d0")
& ~ p1917("d0")
& ~ p1912("d0")
& ~ p1911("d0")
& ~ p1914("d0")
& ~ p1913("d0")
& ~ p1910("d0")
& ~ p1909("d0")
& ~ p1908("d0")
& ~ p1905("d0")
& ~ p1904("d0")
& ~ p1907("d0")
& ~ p1906("d0")
& ~ p1901("d0")
& ~ p1903("d0")
& ~ p1902("d0")
& ~ p1920("d0")
& p1919("d0")
& ~ p209("d0")
& ~ p208("d0")
& ~ p207("d0")
& ~ p206("d0")
& ~ p205("d0")
& ~ p204("d0")
& ~ p203("d0")
& p202("d0")
& ~ p201("d0")
& ~ p219("d0")
& ~ p218("d0")
& ~ p217("d0")
& ~ p216("d0")
& ~ p215("d0")
& ~ p214("d0")
& ~ p213("d0")
& ~ p212("d0")
& ~ p211("d0")
& ~ p210("d0")
& ~ p220("d0")
& ~ p1219("d0")
& ~ p1218("d0")
& ~ p1215("d0")
& ~ p1214("d0")
& ~ p1217("d0")
& ~ p1216("d0")
& ~ p1211("d0")
& ~ p1210("d0")
& ~ p1213("d0")
& p1212("d0")
& ~ p1208("d0")
& ~ p1207("d0")
& ~ p1209("d0")
& ~ p1204("d0")
& ~ p1203("d0")
& ~ p1206("d0")
& ~ p1205("d0")
& ~ p1202("d0")
& ~ p1201("d0")
& ~ p1220("d0")
& ~ p1318("d0")
& ~ p1317("d0")
& ~ p1319("d0")
& ~ p1314("d0")
& p1313("d0")
& ~ p1316("d0")
& ~ p1315("d0")
& ~ p1310("d0")
& ~ p1312("d0")
& ~ p1311("d0")
& ~ p1307("d0")
& ~ p1306("d0")
& ~ p1309("d0")
& ~ p1308("d0")
& ~ p1303("d0")
& ~ p1302("d0")
& ~ p1305("d0")
& ~ p1304("d0")
& ~ p1301("d0")
& ~ p1320("d0")
& ~ p1519("d0")
& ~ p1516("d0")
& ~ p1515("d0")
& ~ p1518("d0")
& ~ p1517("d0")
& ~ p1512("d0")
& ~ p1511("d0")
& p1514("d0")
& ~ p1513("d0")
& ~ p1510("d0")
& ~ p1509("d0")
& ~ p1508("d0")
& ~ p1505("d0")
& ~ p1504("d0")
& ~ p1507("d0")
& ~ p1506("d0")
& ~ p1501("d0")
& ~ p1503("d0")
& ~ p1502("d0")
& ~ p1520("d0")
& ~ p1619("d0")
& ~ p1618("d0")
& p1615("d0")
& ~ p1614("d0")
& ~ p1617("d0")
& ~ p1616("d0")
& ~ p1611("d0")
& ~ p1610("d0")
& ~ p1613("d0")
& ~ p1612("d0")
& ~ p1608("d0")
& ~ p1607("d0")
& ~ p1609("d0")
& ~ p1604("d0")
& ~ p1603("d0")
& ~ p1606("d0")
& ~ p1605("d0")
& ~ p1602("d0")
& ~ p1601("d0")
& ~ p1620("d0")
& ~ p2120("d0")
& ~ p2117("d0")
& ~ p2116("d0")
& ~ p2119("d0")
& p2118("d0")
& ~ p2113("d0")
& ~ p2112("d0")
& ~ p2115("d0")
& ~ p2114("d0")
& ~ p2111("d0")
& ~ p2110("d0")
& ~ p2109("d0")
& ~ p2106("d0")
& ~ p2105("d0")
& ~ p2108("d0")
& ~ p2107("d0")
& ~ p2102("d0")
& ~ p2101("d0")
& ~ p2104("d0")
& ~ p2103("d0")
& ~ p920("d0")
& ~ p906("d0")
& ~ p905("d0")
& ~ p904("d0")
& ~ p903("d0")
& ~ p902("d0")
& ~ p901("d0")
& p909("d0")
& ~ p908("d0")
& ~ p907("d0")
& ~ p917("d0")
& ~ p916("d0")
& ~ p915("d0")
& ~ p914("d0")
& ~ p913("d0")
& ~ p912("d0")
& ~ p911("d0")
& ~ p910("d0")
& ~ p919("d0")
& ~ p918("d0")
& ~ p820("d0")
& ~ p807("d0")
& ~ p806("d0")
& ~ p805("d0")
& ~ p804("d0")
& ~ p803("d0")
& ~ p802("d0")
& ~ p801("d0")
& ~ p809("d0")
& p808("d0")
& ~ p818("d0")
& ~ p817("d0")
& ~ p816("d0")
& ~ p815("d0")
& ~ p814("d0")
& ~ p813("d0")
& ~ p812("d0")
& ~ p811("d0")
& ~ p810("d0")
& ~ p819("d0")
& r1("d0","d0")
& ~ p1020("d0")
& ~ p1017("d0")
& ~ p1016("d0")
& ~ p1019("d0")
& ~ p1018("d0")
& ~ p1013("d0")
& ~ p1012("d0")
& ~ p1015("d0")
& ~ p1014("d0")
& ~ p1011("d0")
& p1010("d0")
& ~ p1009("d0")
& ~ p1006("d0")
& ~ p1005("d0")
& ~ p1008("d0")
& ~ p1007("d0")
& ~ p1002("d0")
& ~ p1001("d0")
& ~ p1004("d0")
& ~ p1003("d0")
& ~ p1119("d0")
& ~ p1116("d0")
& ~ p1115("d0")
& ~ p1118("d0")
& ~ p1117("d0")
& ~ p1112("d0")
& p1111("d0")
& ~ p1114("d0")
& ~ p1113("d0")
& ~ p1110("d0")
& ~ p1109("d0")
& ~ p1108("d0")
& ~ p1105("d0")
& ~ p1104("d0")
& ~ p1107("d0")
& ~ p1106("d0")
& ~ p1101("d0")
& ~ p1103("d0")
& ~ p1102("d0")
& ~ p1120("d0") ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL685+1.020 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.38 % Computer : n015.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Thu Sep 24 00:23:10 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 1.04/1.36 Running: java -jar /export/starexec/sandbox2/solver/bin/FMB4J.jar /export/starexec/sandbox2/tmp/tmp.5M22VacwmY/theBenchmark.cnf 300
% 4.02/2.28 % domain size: 1
% 5.75/2.68 % model found for domain size 1
% 5.75/2.69 % SZS status CounterSatisfiable for theBenchmark
% 5.75/2.69 % SZS output start FiniteModel for theBenchmark
% See solution above
% 6.66/2.84 % FMB4L exiting
%------------------------------------------------------------------------------