%------------------------------------------------------------------------------
% File : FMB4J---0.1
% Problem : SYN907-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n006.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 03:38:38 PM UTC 2026
% Result : Satisfiable 1.03s 1.05s
% Output : FiniteModel 1.03s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(domain,interpretation-domains,
! [X] :
( X = "d1"
| X = "d0" ) ).
fof(mappings,interpretation-mappings,
( skc41 = "d0"
& skf81("d1") = "d1"
& skf80("d0") = "d1"
& skf81("d0") = "d1"
& skf80("d1") = "d1"
& skf83("d1") = "d1"
& skf82("d0") = "d1"
& skf83("d0") = "d1"
& skf82("d1") = "d1"
& skf85("d1") = "d1"
& skf84("d0") = "d1"
& skf85("d0") = "d1"
& skf84("d1") = "d1"
& skf87("d1") = "d1"
& skf86("d0") = "d1"
& skf87("d0") = "d1"
& skf86("d1") = "d1"
& skf89("d1") = "d1"
& skf88("d0") = "d1"
& skf89("d0") = "d1"
& skf88("d1") = "d1"
& skf90("d1") = "d1"
& skf90("d0") = "d1"
& skf92("d1") = "d1"
& skf91("d0") = "d1"
& skf92("d0") = "d1"
& skf91("d1") = "d1"
& skf94("d1") = "d1"
& skf93("d0") = "d1"
& skf94("d0") = "d1"
& skf93("d1") = "d1"
& skf96("d1") = "d1"
& skf95("d0") = "d1"
& skf96("d0") = "d1"
& skf95("d1") = "d1"
& skf97("d0") = "d1"
& skf97("d1") = "d1"
& skf60("d1") = "d0"
& skf61("d1") = "d1"
& skf61("d0") = "d0"
& skf60("d0") = "d0"
& skf63("d1") = "d1"
& skf63("d0") = "d0"
& skf62("d1") = "d1"
& skf62("d0") = "d0"
& skf65("d1") = "d1"
& skf65("d0") = "d0"
& skf64("d1") = "d1"
& skf64("d0") = "d0"
& skf67("d1") = "d1"
& skf67("d0") = "d0"
& skf66("d1") = "d1"
& skf66("d0") = "d0"
& skf69("d1") = "d1"
& skf69("d0") = "d0"
& skf68("d1") = "d1"
& skf68("d0") = "d0"
& skf70("d1") = "d1"
& skf70("d0") = "d0"
& skf72("d1") = "d1"
& skf72("d0") = "d1"
& skf71("d1") = "d1"
& skf71("d0") = "d0"
& skf74("d1") = "d1"
& skf73("d0") = "d1"
& skf74("d0") = "d1"
& skf73("d1") = "d1"
& skf76("d1") = "d1"
& skf75("d0") = "d1"
& skf76("d0") = "d1"
& skf75("d1") = "d1"
& skf78("d1") = "d1"
& skf77("d0") = "d1"
& skf78("d0") = "d1"
& skf77("d1") = "d1"
& skf79("d0") = "d1"
& skf79("d1") = "d1"
& skf49("d1") = "d1"
& skf49("d0") = "d1"
& skf50("d0") = "d1"
& skf50("d1") = "d0"
& skf52("d0") = "d0"
& skf51("d1") = "d0"
& skf52("d1") = "d0"
& skf51("d0") = "d0"
& skf54("d0") = "d0"
& skf53("d1") = "d0"
& skf54("d1") = "d0"
& skf53("d0") = "d0"
& skf56("d0") = "d0"
& skf55("d1") = "d0"
& skf56("d1") = "d0"
& skf55("d0") = "d0"
& skf58("d0") = "d0"
& skf57("d1") = "d0"
& skf58("d1") = "d0"
& skf57("d0") = "d0"
& skf59("d1") = "d0"
& skf59("d0") = "d0" ) ).
fof(predicate_mappings,interpretation-mappings,
( ssPv24("d1")
& ~ ssPv24("d0")
& ssPv22("d1")
& ~ ssPv23("d0")
& ~ ssPv22("d0")
& ssPv23("d1")
& ~ ssPv21("d0")
& ssPv21("d1")
& ssPv15("d1")
& ~ ssPv16("d0")
& ~ ssPv15("d0")
& ssPv16("d1")
& ~ ssPv14("d0")
& ssPv14("d1")
& ~ ssSkP605("d0")
& ssSkP604("d1")
& ssSkP605("d1")
& ~ ssSkP604("d0")
& ~ ssSkP603("d0")
& ssSkP602("d1")
& ssSkP603("d1")
& ~ ssSkP602("d0")
& ssSkP608("d1")
& ssSkP609("d0")
& ~ ssSkP608("d0")
& ssSkP609("d1")
& ~ ssSkP607("d0")
& ssSkP606("d1")
& ssSkP607("d1")
& ~ ssSkP606("d0")
& ~ ssSkP612("d0")
& ssSkP611("d1")
& ssSkP612("d1")
& ~ ssSkP611("d0")
& ~ ssSkP610("d0")
& ssSkP610("d1")
& ssSkP615("d1")
& ssSkP616("d0")
& ssSkP615("d0")
& ssSkP616("d1")
& ssSkP613("d1")
& ssSkP614("d0")
& ~ ssSkP613("d0")
& ssSkP614("d1")
& ssSkP619("d1")
& ssSkP619("d0")
& ssSkP617("d1")
& ssSkP618("d0")
& ssSkP617("d0")
& ssSkP618("d1")
& ssSkP622("d1")
& ssSkP623("d0")
& ssSkP622("d0")
& ssSkP623("d1")
& ssSkP620("d1")
& ssSkP621("d0")
& ssSkP620("d0")
& ssSkP621("d1")
& ssSkP600("d1")
& ~ ssSkP601("d0")
& ~ ssSkP600("d0")
& ssSkP601("d1")
& ssSkP649("d0")
& ssSkP648("d1")
& ssSkP649("d1")
& ssSkP648("d0")
& ssSkP647("d0")
& ssSkP646("d1")
& ssSkP647("d1")
& ssSkP646("d0")
& ~ ssPv8("d0")
& ssPv8("d1")
& ssPv7("d1")
& ~ ssPv6("d0")
& ~ ssPv7("d0")
& ssPv6("d1")
& ssPv5("d1")
& ssSkP651("d1")
& ssSkP652("d0")
& ~ ssPv5("d0")
& ssSkP651("d0")
& ssSkP652("d1")
& ssSkP650("d0")
& ssSkP650("d1")
& ssSkP655("d1")
& ssSkP656("d0")
& ssSkP655("d0")
& ssSkP656("d1")
& ssSkP653("d1")
& ssSkP654("d0")
& ssSkP653("d0")
& ssSkP654("d1")
& ssSkP659("d1")
& ssSkP659("d0")
& ssSkP657("d1")
& ssSkP658("d0")
& ssSkP657("d0")
& ssSkP658("d1")
& ssSkP663("d0")
& ssSkP662("d1")
& ssSkP663("d1")
& ssSkP662("d0")
& ssSkP661("d0")
& ssSkP660("d1")
& ssSkP661("d1")
& ssSkP660("d0")
& ssSkP667("d0")
& ssSkP666("d1")
& ssSkP667("d1")
& ssSkP666("d0")
& ssSkP665("d0")
& ssSkP664("d1")
& ssSkP665("d1")
& ssSkP664("d0")
& ssSkP627("d0")
& ssSkP626("d1")
& ssSkP627("d1")
& ssSkP626("d0")
& ssSkP624("d1")
& ssSkP625("d0")
& ssSkP624("d0")
& ssSkP625("d1")
& ssSkP629("d0")
& ssSkP628("d1")
& ssSkP629("d1")
& ssSkP628("d0")
& ssSkP630("d0")
& ssSkP630("d1")
& ssSkP633("d1")
& ssSkP634("d0")
& ssSkP633("d0")
& ssSkP634("d1")
& ssSkP631("d1")
& ssSkP632("d0")
& ssSkP631("d0")
& ssSkP632("d1")
& ssSkP637("d1")
& ssSkP638("d0")
& ssSkP637("d0")
& ssSkP638("d1")
& ssSkP635("d1")
& ssSkP636("d0")
& ssSkP635("d0")
& ssSkP636("d1")
& ssSkP639("d1")
& ssSkP639("d0")
& ssSkP641("d0")
& ssSkP640("d1")
& ssSkP641("d1")
& ssSkP640("d0")
& ssSkP645("d0")
& ssSkP644("d1")
& ssSkP645("d1")
& ssSkP644("d0")
& ssSkP643("d0")
& ssSkP642("d1")
& ssSkP643("d1")
& ssSkP642("d0")
& ~ ssSkP579("d0")
& ssSkP579("d1")
& ssSkP577("d0")
& ssSkP577("d1")
& ssSkP581("d1")
& ~ ssSkP582("d0")
& ~ ssSkP581("d0")
& ssSkP582("d1")
& ~ ssSkP580("d0")
& ssSkP580("d1")
& ssSkP585("d1")
& ~ ssSkP586("d0")
& ~ ssSkP585("d0")
& ssSkP586("d1")
& ~ ssSkP584("d0")
& ssSkP583("d1")
& ssSkP584("d1")
& ~ ssSkP583("d0")
& ssSkP589("d1")
& ~ ssSkP589("d0")
& ~ ssSkP588("d0")
& ssSkP587("d1")
& ssSkP588("d1")
& ~ ssSkP587("d0")
& ssSkP669("d0")
& ssSkP668("d1")
& ssSkP669("d1")
& ssSkP668("d0")
& ssSkP578("d1","d0")
& ssSkP578("d0","d1")
& ssSkP578("d1","d1")
& ssSkP578("d0","d0")
& ssSkP670("d0")
& ssSkP670("d1")
& ssSkP674("d0")
& ssSkP673("d1")
& ssSkP674("d1")
& ssSkP673("d0")
& ssSkP671("d1")
& ssSkP672("d0")
& ssSkP671("d0")
& ssSkP672("d1")
& ~ ssSkP677("d1")
& ssSkP677("d0")
& ssSkP676("d0")
& ssSkP675("d1")
& ~ ssSkP676("d1")
& ssSkP675("d0")
& ssSkP590("d0","d1")
& ssSkP590("d1","d0")
& ssSkP590("d1","d1")
& ssSkP590("d0","d0")
& ~ ssSkC20
& ~ ssSkP593("d0")
& ssSkP592("d1")
& ssSkP593("d1")
& ~ ssSkP592("d0")
& ~ ssSkP591("d0")
& ssSkP591("d1")
& ssSkP596("d1")
& ~ ssSkP597("d0")
& ~ ssSkP596("d0")
& ssSkP597("d1")
& ~ ssSkP595("d0")
& ssSkP594("d1")
& ssSkP595("d1")
& ~ ssSkP594("d0")
& ssSkP598("d1")
& ~ ssSkP599("d0")
& ~ ssSkP598("d0")
& ssSkP599("d1")
& ssRr("d1","d1")
& ~ ssRr("d0","d0")
& ssRr("d0","d1")
& ssRr("d1","d0") ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN907-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.52 % Computer : n006.cluster.edu
% 0.10/0.52 % Model : x86_64 x86_64
% 0.10/0.52 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.52 % Memory : 8046.5625MB
% 0.10/0.52 % OS : Linux 6.8.0-71-generic
% 0.10/0.52 % CPULimit : 300
% 0.10/0.52 % WCLimit : 300
% 0.10/0.52 % DateTime : Fri Sep 25 02:32:31 UTC 2026
% 0.10/0.53 % CPUTime :
% 0.10/0.53 Running run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.15/0.59 Running: java -jar /export/starexec/sandbox/solver/bin/FMB4J.jar /export/starexec/sandbox/tmp/tmp.x6JD46ZG8L/theBenchmark.cnf 300
% 0.15/0.91 % domain size: 1
% 0.15/1.00 % domain size: 2
% 1.03/1.04 % model found for domain size 2
% 1.03/1.05 % SZS status CounterSatisfiable for theBenchmark
% 1.03/1.06 % SZS output start FiniteModel for theBenchmark
% See solution above
% 1.33/1.14 % FMB4L exiting
%------------------------------------------------------------------------------