%------------------------------------------------------------------------------
% File : FMB4J---0.1
% Problem : SYN905-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 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 : Fri Sep 25 03:38:38 PM UTC 2026
% Result : Satisfiable 1.31s 0.98s
% Output : FiniteModel 2.02s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(domain,interpretation-domains,
! [X] :
( X = "d1"
| X = "d0" ) ).
fof(mappings,interpretation-mappings,
( skc21 = "d0"
& skf80("d0") = "d1"
& skf81("d0") = "d1"
& skf81("d1") = "d0"
& skf80("d1") = "d1"
& skf83("d0") = "d0"
& skf82("d1") = "d0"
& skf83("d1") = "d0"
& skf82("d0") = "d0"
& skf85("d0") = "d0"
& skf84("d1") = "d0"
& skf85("d1") = "d0"
& skf84("d0") = "d0"
& skf87("d0") = "d0"
& skf86("d1") = "d0"
& skf87("d1") = "d0"
& skf86("d0") = "d0"
& skf89("d0") = "d0"
& skf88("d1") = "d0"
& skf89("d1") = "d0"
& skf88("d0") = "d0"
& skf90("d0") = "d0"
& skf90("d1") = "d0"
& skf92("d0") = "d0"
& skf91("d1") = "d0"
& skf92("d1") = "d0"
& skf91("d0") = "d0"
& skf93("d1") = "d0"
& skf94("d1") = "d1"
& skf94("d0") = "d0"
& skf93("d0") = "d0"
& skf96("d1") = "d1"
& skf96("d0") = "d0"
& skf95("d1") = "d1"
& skf95("d0") = "d0"
& skf98("d1") = "d1"
& skf98("d0") = "d0"
& skf97("d1") = "d1"
& skf97("d0") = "d0"
& skf99("d1") = "d1"
& skf99("d0") = "d0"
& skf104("d1") = "d1"
& skf104("d0") = "d0"
& skf103("d1") = "d1"
& skf103("d0") = "d0"
& skf102("d1") = "d1"
& skf102("d0") = "d0"
& skf101("d1") = "d1"
& skf101("d0") = "d0"
& skf100("d1") = "d1"
& skf100("d0") = "d0"
& skf109("d0") = "d1"
& skf109("d1") = "d1"
& skf108("d1") = "d1"
& skf107("d0") = "d1"
& skf108("d0") = "d1"
& skf107("d1") = "d1"
& skf106("d1") = "d1"
& skf106("d0") = "d0"
& skf105("d1") = "d1"
& skf105("d0") = "d0"
& skf115("d1") = "d1"
& skf114("d0") = "d1"
& skf115("d0") = "d1"
& skf114("d1") = "d1"
& skf113("d1") = "d1"
& skf112("d0") = "d1"
& skf113("d0") = "d1"
& skf112("d1") = "d1"
& skf111("d1") = "d1"
& skf110("d0") = "d1"
& skf111("d0") = "d1"
& skf110("d1") = "d1"
& skf119("d1") = "d1"
& skf118("d0") = "d1"
& skf119("d0") = "d1"
& skf118("d1") = "d1"
& skf117("d1") = "d1"
& skf116("d0") = "d1"
& skf117("d0") = "d1"
& skf116("d1") = "d1"
& skf126("d1") = "d1"
& skf125("d0") = "d1"
& skf126("d0") = "d1"
& skf125("d1") = "d1"
& skf124("d1") = "d1"
& skf123("d0") = "d1"
& skf124("d0") = "d1"
& skf123("d1") = "d1"
& skf122("d1") = "d1"
& skf121("d0") = "d1"
& skf122("d0") = "d1"
& skf121("d1") = "d1"
& skf120("d1") = "d1"
& skf120("d0") = "d1"
& skf129("d0") = "d1"
& skf129("d1") = "d1"
& skf128("d1") = "d1"
& skf127("d0") = "d1"
& skf128("d0") = "d1"
& skf127("d1") = "d1"
& skf140("d1") = "d1"
& skf140("d0") = "d1"
& skf137("d1") = "d1"
& skf136("d0") = "d1"
& skf137("d0") = "d1"
& skf136("d1") = "d1"
& skf135("d1") = "d1"
& skf134("d0") = "d1"
& skf135("d0") = "d1"
& skf134("d1") = "d1"
& skf133("d1") = "d1"
& skf132("d0") = "d1"
& skf133("d0") = "d1"
& skf132("d1") = "d1"
& skf131("d1") = "d1"
& skf130("d0") = "d1"
& skf131("d0") = "d1"
& skf130("d1") = "d1"
& skf139("d1") = "d1"
& skf138("d0") = "d1"
& skf139("d0") = "d1"
& skf138("d1") = "d1"
& skf151("d1") = "d1"
& skf150("d0") = "d1"
& skf151("d0") = "d1"
& skf150("d1") = "d1"
& skf148("d1") = "d1"
& skf147("d0") = "d1"
& skf148("d0") = "d1"
& skf147("d1") = "d1"
& skf146("d1") = "d1"
& skf145("d0") = "d1"
& skf146("d0") = "d1"
& skf145("d1") = "d1"
& skf144("d1") = "d1"
& skf143("d0") = "d1"
& skf144("d0") = "d1"
& skf143("d1") = "d1"
& skf142("d1") = "d1"
& skf141("d0") = "d1"
& skf142("d0") = "d1"
& skf141("d1") = "d1"
& skf149("d0") = "d1"
& skf149("d1") = "d1"
& skf159("d1") = "d1"
& skf158("d0") = "d1"
& skf159("d0") = "d1"
& skf158("d1") = "d1"
& skf157("d1") = "d1"
& skf156("d0") = "d1"
& skf157("d0") = "d1"
& skf156("d1") = "d1"
& skf155("d1") = "d1"
& skf154("d0") = "d1"
& skf155("d0") = "d1"
& skf154("d1") = "d1"
& skf153("d1") = "d1"
& skf152("d0") = "d1"
& skf153("d0") = "d1"
& skf152("d1") = "d1" ) ).
fof(predicate_mappings,interpretation-mappings,
( ssPv48("d1")
& ~ ssPv48("d0")
& ssPv46("d1")
& ~ ssPv47("d0")
& ~ ssPv46("d0")
& ssPv47("d1")
& ~ ssPv41("d0")
& ssPv41("d1")
& ~ ssPv25("d0")
& ssPv25("d1")
& ssPv28("d1")
& ~ ssPv29("d0")
& ~ ssPv28("d0")
& ssPv29("d1")
& ~ ssPv30("d0")
& ssPv30("d1")
& ~ ssPv16("d0")
& ssPv16("d1")
& ~ ssPv14("d0")
& ssPv14("d1")
& ~ ssPv12("d0")
& ssPv11("d1")
& ssPv12("d1")
& ~ ssPv11("d0")
& ~ ssSkP527("d0")
& ssSkP528("d1")
& ssSkP527("d1")
& ~ ssSkP528("d0")
& ~ ssSkP525("d0")
& ssSkP526("d1")
& ssSkP525("d1")
& ~ ssSkP526("d0")
& ssPv9("d1")
& ~ ssPv9("d0")
& ~ ssSkP529("d0")
& ssSkP529("d1")
& ~ ssSkP530("d0")
& ssSkP530("d1")
& ~ ssSkP534("d0")
& ssSkP535("d1")
& ssSkP534("d1")
& ~ ssSkP535("d0")
& ssSkP533("d1")
& ~ ssSkP532("d0")
& ~ ssSkP533("d0")
& ssSkP532("d1")
& ssSkP539("d1")
& ~ ssSkP538("d0")
& ~ ssSkP539("d0")
& ssSkP538("d1")
& ~ ssSkP536("d0")
& ssSkP537("d1")
& ssSkP536("d1")
& ~ ssSkP537("d0")
& ~ ssSkP541("d0")
& ssSkP542("d1")
& ssSkP541("d1")
& ~ ssSkP542("d0")
& ssSkP540("d1")
& ~ ssSkP540("d0")
& ssSkP546("d1")
& ~ ssSkP545("d0")
& ~ ssSkP546("d0")
& ssSkP545("d1")
& ~ ssSkP543("d0")
& ssSkP544("d1")
& ssSkP543("d1")
& ~ ssSkP544("d0")
& ssSkP516("d0")
& ssSkP516("d1")
& ssSkP519("d1")
& ~ ssSkP518("d0")
& ~ ssSkP519("d0")
& ssSkP518("d1")
& ssSkP520("d1")
& ~ ssSkP520("d0")
& ~ ssSkP523("d0")
& ssSkP524("d1")
& ssSkP523("d1")
& ~ ssSkP524("d0")
& ~ ssSkP521("d0")
& ssSkP522("d1")
& ssSkP521("d1")
& ~ ssSkP522("d0")
& ssSkP668("d1")
& ssSkP669("d0")
& ssSkP668("d0")
& ssSkP669("d1")
& ssSkP670("d0")
& ssSkP670("d1")
& ssSkP674("d0")
& ssSkP673("d1")
& ssSkP674("d1")
& ssSkP673("d0")
& ssSkP672("d0")
& ssSkP671("d1")
& ssSkP672("d1")
& ssSkP671("d0")
& ~ ssSkP677("d1")
& ssSkP678("d0")
& ssSkP677("d0")
& ~ ssSkP678("d1")
& ssSkP675("d1")
& ssSkP676("d0")
& ssSkP676("d1")
& ssSkP675("d0")
& ssRr("d1","d1")
& ~ ssRr("d0","d0")
& ssRr("d0","d1")
& ssRr("d1","d0")
& ssSkP604("d1")
& ssSkP605("d0")
& ssSkP604("d0")
& ssSkP605("d1")
& ssSkP602("d1")
& ssSkP603("d0")
& ssSkP602("d0")
& ssSkP603("d1")
& ssSkP608("d1")
& ssSkP609("d0")
& ssSkP608("d0")
& ssSkP609("d1")
& ssSkP606("d1")
& ssSkP607("d0")
& ssSkP606("d0")
& ssSkP607("d1")
& ssSkP612("d0")
& ssSkP611("d1")
& ssSkP612("d1")
& ssSkP611("d0")
& ssSkP610("d0")
& ssSkP610("d1")
& ssSkP616("d0")
& ssSkP615("d1")
& ssSkP616("d1")
& ssSkP615("d0")
& ssSkP614("d0")
& ssSkP613("d1")
& ssSkP614("d1")
& ssSkP613("d0")
& ssSkP619("d1")
& ssSkP619("d0")
& ssSkP618("d0")
& ssSkP617("d1")
& ssSkP618("d1")
& ssSkP617("d0")
& ssSkP622("d1")
& ssSkP623("d0")
& ssSkP622("d0")
& ssSkP623("d1")
& ssSkP620("d1")
& ssSkP621("d0")
& ssSkP620("d0")
& ssSkP621("d1")
& ssSkP600("d1")
& ssSkP601("d0")
& ssSkP600("d0")
& ssSkP601("d1")
& ssSkP648("d1")
& ssSkP649("d0")
& ssSkP648("d0")
& ssSkP649("d1")
& ssSkP646("d1")
& ssSkP647("d0")
& ssSkP646("d0")
& ssSkP647("d1")
& ssSkP652("d0")
& ssSkP651("d1")
& ssSkP652("d1")
& ssSkP651("d0")
& ssSkP650("d0")
& ssSkP650("d1")
& ssSkP656("d0")
& ssSkP655("d1")
& ssSkP656("d1")
& ssSkP655("d0")
& ssSkP654("d0")
& ssSkP653("d1")
& ssSkP654("d1")
& ssSkP653("d0")
& ssSkP659("d1")
& ssSkP659("d0")
& ssSkP658("d0")
& ssSkP657("d1")
& ssSkP658("d1")
& ssSkP657("d0")
& ssSkP517("d1","d0")
& ssSkP517("d0","d1")
& ssSkP517("d1","d1")
& ssSkP517("d0","d0")
& ssSkP662("d1")
& ssSkP663("d0")
& ssSkP662("d0")
& ssSkP663("d1")
& ssSkP660("d1")
& ssSkP661("d0")
& ssSkP660("d0")
& ssSkP661("d1")
& ssSkP666("d1")
& ssSkP667("d0")
& ssSkP666("d0")
& ssSkP667("d1")
& ssSkP664("d1")
& ssSkP665("d0")
& ssSkP664("d0")
& ssSkP665("d1")
& ssSkP626("d1")
& ssSkP627("d0")
& ssSkP626("d0")
& ssSkP627("d1")
& ssSkP624("d1")
& ssSkP625("d0")
& ssSkP624("d0")
& ssSkP625("d1")
& ssSkP628("d1")
& ssSkP629("d0")
& ssSkP628("d0")
& ssSkP629("d1")
& ssSkP531("d0","d1")
& ssSkP531("d1","d0")
& ssSkP531("d1","d1")
& ssSkP531("d0","d0")
& ssSkP630("d0")
& ssSkP630("d1")
& ssSkP634("d0")
& ssSkP633("d1")
& ssSkP634("d1")
& ssSkP633("d0")
& ssSkP632("d0")
& ssSkP631("d1")
& ssSkP632("d1")
& ssSkP631("d0")
& ssSkP638("d0")
& ssSkP637("d1")
& ssSkP638("d1")
& ssSkP637("d0")
& ssSkP636("d0")
& ssSkP635("d1")
& ssSkP636("d1")
& ssSkP635("d0")
& ssSkP639("d1")
& ssSkP639("d0")
& ssSkP640("d1")
& ssSkP641("d0")
& ssSkP640("d0")
& ssSkP641("d1")
& ssSkP644("d1")
& ssSkP645("d0")
& ssSkP644("d0")
& ssSkP645("d1")
& ssSkP642("d1")
& ssSkP643("d0")
& ssSkP642("d0")
& ssSkP643("d1")
& ssSkP569("d1")
& ssSkP569("d0")
& ssSkP570("d1")
& ssSkP571("d0")
& ssSkP570("d0")
& ssSkP571("d1")
& ssSkP574("d1")
& ssSkP575("d0")
& ssSkP574("d0")
& ssSkP575("d1")
& ssSkP572("d1")
& ssSkP573("d0")
& ssSkP572("d0")
& ssSkP573("d1")
& ssSkP578("d1")
& ssSkP579("d0")
& ssSkP578("d0")
& ssSkP579("d1")
& ssSkP576("d1")
& ssSkP577("d0")
& ssSkP576("d0")
& ssSkP577("d1")
& ssSkP582("d0")
& ssSkP581("d1")
& ssSkP582("d1")
& ssSkP581("d0")
& ssSkP580("d0")
& ssSkP580("d1")
& ssSkP586("d0")
& ssSkP585("d1")
& ssSkP586("d1")
& ssSkP585("d0")
& ssSkP584("d0")
& ssSkP583("d1")
& ssSkP584("d1")
& ssSkP583("d0")
& ssSkP589("d1")
& ssSkP589("d0")
& ssSkP588("d0")
& ssSkP587("d1")
& ssSkP588("d1")
& ssSkP587("d0")
& ssSkP549("d1")
& ~ ssSkP549("d0")
& ~ ssSkP548("d0")
& ssSkP547("d1")
& ssSkP548("d1")
& ~ ssSkP547("d0")
& ~ ssSkP553("d0")
& ssSkP552("d1")
& ssSkP553("d1")
& ~ ssSkP552("d0")
& ~ ssSkP551("d0")
& ssSkP550("d1")
& ssSkP551("d1")
& ~ ssSkP550("d0")
& ~ ssSkP557("d0")
& ssSkP556("d1")
& ssSkP557("d1")
& ssSkP556("d0")
& ~ ssSkP555("d0")
& ssSkP554("d1")
& ssSkP555("d1")
& ~ ssSkP554("d0")
& ssSkP558("d1")
& ssSkP559("d0")
& ~ ssSkP558("d0")
& ssSkP559("d1")
& ssSkP560("d0")
& ssSkP560("d1")
& ssSkP563("d1")
& ssSkP564("d0")
& ssSkP563("d0")
& ssSkP564("d1")
& ssSkP561("d1")
& ssSkP562("d0")
& ssSkP561("d0")
& ssSkP562("d1")
& ssSkP567("d1")
& ssSkP568("d0")
& ssSkP567("d0")
& ssSkP568("d1")
& ssSkP565("d1")
& ssSkP566("d0")
& ssSkP565("d0")
& ssSkP566("d1")
& ~ ssSkC10
& ssSkP592("d1")
& ssSkP593("d0")
& ssSkP592("d0")
& ssSkP593("d1")
& ssSkP590("d1")
& ssSkP591("d0")
& ssSkP590("d0")
& ssSkP591("d1")
& ssSkP596("d1")
& ssSkP597("d0")
& ssSkP596("d0")
& ssSkP597("d1")
& ssSkP594("d1")
& ssSkP595("d0")
& ssSkP594("d0")
& ssSkP595("d1")
& ssSkP598("d1")
& ssSkP599("d0")
& ssSkP598("d0")
& ssSkP599("d1") ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN905-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.03 % Command : run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.36 % Computer : n011.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Fri Sep 25 02:32:13 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.13/0.46 Running: java -jar /export/starexec/sandbox2/solver/bin/FMB4J.jar /export/starexec/sandbox2/tmp/tmp.SdAS0SkRrN/theBenchmark.cnf 300
% 0.83/0.83 % domain size: 1
% 1.31/0.92 % domain size: 2
% 1.31/0.97 % model found for domain size 2
% 1.31/0.98 % SZS status CounterSatisfiable for theBenchmark
% 1.31/0.98 % SZS output start FiniteModel for theBenchmark
% See solution above
% 2.02/1.11 % FMB4L exiting
%------------------------------------------------------------------------------