%------------------------------------------------------------------------------
% File : FMB4J---0.1
% Problem : SYN909-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.15s 0.90s
% Output : FiniteModel 1.15s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(domain,interpretation-domains,
! [X] :
( X = "d1"
| X = "d0" ) ).
fof(mappings,interpretation-mappings,
( 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"
& skf98("d1") = "d1"
& skf97("d0") = "d1"
& skf98("d0") = "d1"
& skf97("d1") = "d1"
& skf99("d0") = "d1"
& skf99("d1") = "d1"
& skf61("d0") = "d0"
& skf60("d1") = "d0"
& skf61("d1") = "d0"
& skf60("d0") = "d0"
& skf63("d0") = "d0"
& skf62("d1") = "d0"
& skf63("d1") = "d0"
& 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") = "d0"
& skf71("d1") = "d1"
& skf71("d0") = "d0"
& skf74("d1") = "d1"
& skf74("d0") = "d0"
& skf73("d1") = "d1"
& skf73("d0") = "d0"
& skf76("d1") = "d1"
& skf76("d0") = "d1"
& skf75("d1") = "d1"
& skf75("d0") = "d0"
& skf78("d1") = "d1"
& skf77("d0") = "d1"
& skf78("d0") = "d1"
& skf77("d1") = "d1"
& skf79("d0") = "d1"
& skf79("d1") = "d1"
& skf51("d0") = "d1"
& skf52("d0") = "d1"
& skf52("d1") = "d0"
& skf51("d1") = "d1"
& 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"
& skc61 = "d0"
& skf101("d0") = "d1"
& skf101("d1") = "d1"
& skf100("d1") = "d1"
& skf100("d0") = "d1" ) ).
fof(predicate_mappings,interpretation-mappings,
( ssPv24("d1")
& ~ ssPv24("d0")
& ssSkP809("d0")
& ssSkP809("d1")
& ssPv22("d1")
& ~ ssPv23("d0")
& ~ ssPv22("d0")
& ssPv23("d1")
& ~ ssPv21("d0")
& ssPv21("d1")
& ssSkP813("d1")
& ~ ssSkP814("d0")
& ~ ssSkP813("d0")
& ssSkP814("d1")
& ~ ssSkP812("d0")
& ssSkP811("d1")
& ssSkP812("d1")
& ~ ssSkP811("d0")
& ~ ssSkP818("d0")
& ssSkP817("d1")
& ssSkP818("d1")
& ~ ssSkP817("d0")
& ~ ssSkP816("d0")
& ssSkP815("d1")
& ssSkP816("d1")
& ~ ssSkP815("d0")
& ssSkP819("d1")
& ~ ssSkP819("d0")
& ssSkP820("d1")
& ~ ssSkP821("d0")
& ~ ssSkP820("d0")
& ssSkP821("d1")
& ssSkP901("d1")
& ssSkP902("d0")
& ssSkP901("d0")
& ssSkP902("d1")
& ssSkP900("d0")
& ssSkP900("d1")
& ssSkP905("d1")
& ssSkP906("d0")
& ssSkP905("d0")
& ssSkP906("d1")
& ssSkP903("d1")
& ssSkP904("d0")
& ssSkP903("d0")
& ssSkP904("d1")
& ssSkP909("d1")
& ssSkP909("d0")
& ssSkP907("d1")
& ssSkP908("d0")
& ssSkP907("d0")
& ssSkP908("d1")
& ssSkP810("d1","d1")
& ssSkP810("d0","d0")
& ssSkP810("d1","d0")
& ssSkP810("d0","d1")
& ~ ssSkP912("d1")
& ssPv15("d1")
& ~ ssPv16("d0")
& ssSkP913("d0")
& ssSkP912("d0")
& ~ ssPv15("d0")
& ssPv16("d1")
& ~ ssSkP913("d1")
& ssSkP910("d1")
& ssSkP911("d0")
& ~ ssPv14("d0")
& ssPv13("d1")
& ssSkP911("d1")
& ssSkP910("d0")
& ssPv14("d1")
& ~ ssPv13("d0")
& ~ ssSkP847("d0")
& ssSkP846("d1")
& ssSkP847("d1")
& ~ ssSkP846("d0")
& ssSkP844("d1")
& ssSkP845("d0")
& ~ ssSkP844("d0")
& ssSkP845("d1")
& ssSkP848("d1")
& ssSkP849("d0")
& ~ ssSkP848("d0")
& ssSkP849("d1")
& ssSkP823("d1","d1")
& ssSkP823("d0","d0")
& ssSkP823("d0","d1")
& ssSkP823("d1","d0")
& ssSkP850("d0")
& ssSkP850("d1")
& ssSkP853("d1")
& ssSkP854("d0")
& ssSkP853("d0")
& ssSkP854("d1")
& ssSkP851("d1")
& ssSkP852("d0")
& ssSkP851("d0")
& ssSkP852("d1")
& ssSkP857("d1")
& ssSkP858("d0")
& ssSkP857("d0")
& ssSkP858("d1")
& ssSkP855("d1")
& ssSkP856("d0")
& ssSkP855("d0")
& ssSkP856("d1")
& ssSkP859("d1")
& ssSkP859("d0")
& ssSkP860("d1")
& ssSkP861("d0")
& ssSkP860("d0")
& ssSkP861("d1")
& ssSkP865("d0")
& ssSkP864("d1")
& ssSkP865("d1")
& ssSkP864("d0")
& ssSkP863("d0")
& ssSkP862("d1")
& ssSkP863("d1")
& ssSkP862("d0")
& ~ ssSkP825("d0")
& ssSkP824("d1")
& ssSkP825("d1")
& ~ ssSkP824("d0")
& ssSkP822("d1")
& ~ ssSkP822("d0")
& ~ ssSkP829("d0")
& ssSkP828("d1")
& ssSkP829("d1")
& ~ ssSkP828("d0")
& ssSkP826("d1")
& ~ ssSkP827("d0")
& ~ ssSkP826("d0")
& ssSkP827("d1")
& ~ ssSkC30
& ~ ssSkP832("d0")
& ssSkP831("d1")
& ssSkP832("d1")
& ~ ssSkP831("d0")
& ~ ssSkP830("d0")
& ssSkP830("d1")
& ssSkP835("d1")
& ~ ssSkP836("d0")
& ~ ssSkP835("d0")
& ssSkP836("d1")
& ~ ssSkP834("d0")
& ssSkP833("d1")
& ssSkP834("d1")
& ~ ssSkP833("d0")
& ssSkP839("d1")
& ~ ssSkP839("d0")
& ~ ssSkP838("d0")
& ssSkP837("d1")
& ssSkP838("d1")
& ~ ssSkP837("d0")
& ~ ssSkP843("d0")
& ssSkP842("d1")
& ssSkP843("d1")
& ~ ssSkP842("d0")
& ~ ssSkP841("d0")
& ssSkP840("d1")
& ssSkP841("d1")
& ~ ssSkP840("d0")
& ssSkP889("d0")
& ssSkP888("d1")
& ssSkP889("d1")
& ssSkP888("d0")
& ~ ssPv8("d0")
& ssPv8("d1")
& ssPv7("d1")
& ~ ssPv6("d0")
& ~ ssPv7("d0")
& ssPv6("d1")
& ssSkP890("d0")
& ssSkP890("d1")
& ssPv5("d1")
& ssSkP893("d1")
& ssSkP894("d0")
& ~ ssPv5("d0")
& ssSkP893("d0")
& ssSkP894("d1")
& ssSkP891("d1")
& ssSkP892("d0")
& ssSkP891("d0")
& ssSkP892("d1")
& ssSkP897("d1")
& ssSkP898("d0")
& ssSkP897("d0")
& ssSkP898("d1")
& ssSkP895("d1")
& ssSkP896("d0")
& ssSkP895("d0")
& ssSkP896("d1")
& ssSkP899("d1")
& ssSkP899("d0")
& ssSkP869("d0")
& ssSkP868("d1")
& ssSkP869("d1")
& ssSkP868("d0")
& ssSkP867("d0")
& ssSkP866("d1")
& ssSkP867("d1")
& ssSkP866("d0")
& ssSkP871("d1")
& ssSkP872("d0")
& ssSkP871("d0")
& ssSkP872("d1")
& ssSkP870("d0")
& ssSkP870("d1")
& ssSkP875("d1")
& ssSkP876("d0")
& ssSkP875("d0")
& ssSkP876("d1")
& ssSkP873("d1")
& ssSkP874("d0")
& ssSkP873("d0")
& ssSkP874("d1")
& ssSkP879("d1")
& ssSkP879("d0")
& ssSkP877("d1")
& ssSkP878("d0")
& ssSkP877("d0")
& ssSkP878("d1")
& ssSkP883("d0")
& ssSkP882("d1")
& ssSkP883("d1")
& ssSkP882("d0")
& ssSkP881("d0")
& ssSkP880("d1")
& ssSkP881("d1")
& ssSkP880("d0")
& ssSkP887("d0")
& ssSkP886("d1")
& ssSkP887("d1")
& ssSkP886("d0")
& ssSkP885("d0")
& ssSkP884("d1")
& ssSkP885("d1")
& ssSkP884("d0")
& ssRr("d1","d1")
& ~ ssRr("d0","d0")
& ssRr("d0","d1")
& ssRr("d1","d0") ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN909-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n011.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 02:32:43 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.44 Running: java -jar /export/starexec/sandbox2/solver/bin/FMB4J.jar /export/starexec/sandbox2/tmp/tmp.OnAzJHq7H6/theBenchmark.cnf 300
% 0.55/0.76 % domain size: 1
% 0.86/0.85 % domain size: 2
% 0.86/0.88 % model found for domain size 2
% 1.15/0.90 % SZS status CounterSatisfiable for theBenchmark
% 1.15/0.90 % SZS output start FiniteModel for theBenchmark
% See solution above
% 1.15/0.98 % FMB4L exiting
%------------------------------------------------------------------------------