%------------------------------------------------------------------------------
% File : FMB4J---0.1
% Problem : LCL685+1.015 : 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 3.35s 1.65s
% Output : FiniteModel 3.82s
% 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,
( ~ p109("d0")
& ~ p108("d0")
& ~ p107("d0")
& ~ p106("d0")
& ~ p105("d0")
& ~ p104("d0")
& ~ p103("d0")
& ~ p102("d0")
& p101("d0")
& ~ p115("d0")
& ~ p114("d0")
& ~ p113("d0")
& ~ p112("d0")
& ~ p111("d0")
& ~ p110("d0")
& ~ p1215("d0")
& ~ p1214("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")
& ~ p509("d0")
& ~ p508("d0")
& ~ p507("d0")
& ~ p506("d0")
& p505("d0")
& ~ p504("d0")
& ~ p503("d0")
& ~ p502("d0")
& ~ p501("d0")
& ~ p515("d0")
& ~ p514("d0")
& ~ p513("d0")
& ~ p512("d0")
& ~ p511("d0")
& ~ p510("d0")
& ~ p906("d0")
& ~ p905("d0")
& ~ p904("d0")
& ~ p903("d0")
& ~ p902("d0")
& ~ p901("d0")
& p909("d0")
& ~ p908("d0")
& ~ p907("d0")
& ~ p915("d0")
& ~ p914("d0")
& ~ p913("d0")
& ~ p912("d0")
& ~ p911("d0")
& ~ p910("d0")
& ~ p1314("d0")
& ~ p1313("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")
& ~ p409("d0")
& ~ p408("d0")
& ~ p407("d0")
& ~ p406("d0")
& ~ p405("d0")
& p404("d0")
& ~ p403("d0")
& ~ p402("d0")
& ~ p401("d0")
& ~ p415("d0")
& ~ p414("d0")
& ~ p413("d0")
& ~ p412("d0")
& ~ p411("d0")
& ~ p410("d0")
& ~ p807("d0")
& ~ p806("d0")
& ~ p805("d0")
& ~ p804("d0")
& ~ p803("d0")
& ~ p802("d0")
& ~ p801("d0")
& ~ p809("d0")
& p808("d0")
& ~ p815("d0")
& ~ p814("d0")
& ~ p813("d0")
& ~ p812("d0")
& ~ p811("d0")
& ~ p810("d0")
& ~ p1413("d0")
& ~ p1412("d0")
& ~ p1415("d0")
& p1414("d0")
& ~ p1411("d0")
& ~ p1410("d0")
& r1("d0","d0")
& ~ p1409("d0")
& ~ p1406("d0")
& ~ p1405("d0")
& ~ p1408("d0")
& ~ p1407("d0")
& ~ p1402("d0")
& ~ p1401("d0")
& ~ p1404("d0")
& ~ p1403("d0")
& ~ p309("d0")
& ~ p308("d0")
& ~ p307("d0")
& ~ p306("d0")
& ~ p305("d0")
& ~ p304("d0")
& p303("d0")
& ~ p302("d0")
& ~ p301("d0")
& ~ p315("d0")
& ~ p314("d0")
& ~ p313("d0")
& ~ p312("d0")
& ~ p311("d0")
& ~ p310("d0")
& ~ p708("d0")
& p707("d0")
& ~ p706("d0")
& ~ p705("d0")
& ~ p704("d0")
& ~ p703("d0")
& ~ p702("d0")
& ~ p701("d0")
& ~ p709("d0")
& ~ p715("d0")
& ~ p714("d0")
& ~ p713("d0")
& ~ p712("d0")
& ~ p711("d0")
& ~ p710("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")
& p1515("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")
& ~ p209("d0")
& ~ p208("d0")
& ~ p207("d0")
& ~ p206("d0")
& ~ p205("d0")
& ~ p204("d0")
& ~ p203("d0")
& p202("d0")
& ~ p201("d0")
& ~ p215("d0")
& ~ p214("d0")
& ~ p213("d0")
& ~ p212("d0")
& ~ p211("d0")
& ~ p210("d0")
& ~ p609("d0")
& ~ p608("d0")
& ~ p607("d0")
& p606("d0")
& ~ p605("d0")
& ~ p604("d0")
& ~ p603("d0")
& ~ p602("d0")
& ~ p601("d0")
& ~ p615("d0")
& ~ p614("d0")
& ~ p613("d0")
& ~ p612("d0")
& ~ p611("d0")
& ~ p610("d0")
& ~ p1615("d0")
& ~ p1614("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") ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL685+1.015 : 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.37 % Computer : n015.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 : Thu Sep 24 00:22:55 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.41/0.74 Running: java -jar /export/starexec/sandbox2/solver/bin/FMB4J.jar /export/starexec/sandbox2/tmp/tmp.NfuIe0LGFx/theBenchmark.cnf 300
% 2.05/1.35 % domain size: 1
% 3.35/1.63 % model found for domain size 1
% 3.35/1.65 % SZS status CounterSatisfiable for theBenchmark
% 3.35/1.65 % SZS output start FiniteModel for theBenchmark
% See solution above
% 3.82/1.76 % FMB4L exiting
%------------------------------------------------------------------------------