%------------------------------------------------------------------------------
% File : FMB4J---0.1
% Problem : SYN904-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 : n002.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.26s 0.92s
% Output : FiniteModel 1.26s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(domain,interpretation-domains,
! [X] :
( X = "d1"
| X = "d0" ) ).
fof(mappings,interpretation-mappings,
( skc21 = "d0"
& skf81("d1") = "d1"
& skf81("d0") = "d0"
& skf80("d1") = "d1"
& skf80("d0") = "d0"
& skf83("d1") = "d1"
& skf83("d0") = "d0"
& skf82("d1") = "d1"
& skf82("d0") = "d0"
& skf85("d1") = "d1"
& skf85("d0") = "d1"
& skf84("d1") = "d1"
& skf84("d0") = "d0"
& 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("d0") = "d1"
& skf61("d1") = "d0"
& skf60("d1") = "d1"
& skf63("d0") = "d0"
& skf62("d1") = "d0"
& skf63("d1") = "d0"
& skf62("d0") = "d0"
& skf65("d0") = "d0"
& skf64("d1") = "d0"
& skf65("d1") = "d0"
& skf64("d0") = "d0"
& skf67("d0") = "d0"
& skf66("d1") = "d0"
& skf67("d1") = "d0"
& skf66("d0") = "d0"
& skf69("d0") = "d0"
& skf68("d1") = "d0"
& skf69("d1") = "d0"
& skf68("d0") = "d0"
& skf70("d0") = "d0"
& skf70("d1") = "d0"
& skf72("d0") = "d0"
& skf71("d1") = "d0"
& skf72("d1") = "d0"
& skf71("d0") = "d0"
& skf74("d1") = "d1"
& skf74("d0") = "d0"
& skf73("d1") = "d1"
& skf73("d0") = "d0"
& skf76("d1") = "d1"
& skf76("d0") = "d0"
& skf75("d1") = "d1"
& skf75("d0") = "d0"
& skf78("d1") = "d1"
& skf78("d0") = "d0"
& skf77("d1") = "d1"
& skf77("d0") = "d0"
& skf79("d1") = "d1"
& skf79("d0") = "d0"
& skf104("d1") = "d1"
& skf103("d0") = "d1"
& skf104("d0") = "d1"
& skf103("d1") = "d1"
& skf102("d1") = "d1"
& skf101("d0") = "d1"
& skf102("d0") = "d1"
& skf101("d1") = "d1"
& skf100("d1") = "d1"
& skf100("d0") = "d1"
& skf109("d0") = "d1"
& skf109("d1") = "d1"
& skf108("d1") = "d1"
& skf107("d0") = "d1"
& skf108("d0") = "d1"
& skf107("d1") = "d1"
& skf106("d1") = "d1"
& skf105("d0") = "d1"
& skf106("d0") = "d1"
& skf105("d1") = "d1"
& 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" ) ).
fof(predicate_mappings,interpretation-mappings,
( ssPv26("d1")
& ~ ssPv27("d0")
& ~ ssPv26("d0")
& ssPv27("d1")
& ~ ssPv25("d0")
& ssPv25("d1")
& ssPv28("d1")
& ~ ssPv29("d0")
& ~ ssPv28("d0")
& ssPv29("d1")
& ~ ssPv30("d0")
& ssPv30("d1")
& ssPv31("d1")
& ~ ssPv31("d0")
& ssPv15("d1")
& ~ ssPv15("d0")
& ssPv13("d1")
& ~ ssPv14("d0")
& ~ ssPv13("d0")
& ssPv14("d1")
& ~ ssPv12("d0")
& ssPv12("d1")
& ~ ssPv10("d0")
& ssPv10("d1")
& ssSkP406("d0")
& ssSkP407("d1")
& ssSkP406("d1")
& ssSkP407("d0")
& ssSkP404("d0")
& ssSkP405("d1")
& ssSkP404("d1")
& ssSkP405("d0")
& ssSkP408("d0")
& ssSkP409("d1")
& ssSkP408("d1")
& ssSkP409("d0")
& ssSkP410("d1")
& ssSkP410("d0")
& ssSkP413("d0")
& ssSkP414("d1")
& ssSkP413("d1")
& ssSkP414("d0")
& ssSkP411("d0")
& ssSkP412("d1")
& ssSkP411("d1")
& ssSkP412("d0")
& ssSkP417("d0")
& ssSkP418("d1")
& ssSkP417("d1")
& ssSkP418("d0")
& ssSkP415("d0")
& ssSkP416("d1")
& ssSkP415("d1")
& ssSkP416("d0")
& ssSkP419("d0")
& ssSkP419("d1")
& ssSkP421("d1")
& ssSkP420("d0")
& ssSkP421("d0")
& ssSkP420("d1")
& ssSkP425("d1")
& ssSkP424("d0")
& ssSkP425("d0")
& ssSkP424("d1")
& ssSkP423("d1")
& ssSkP422("d0")
& ssSkP423("d0")
& ssSkP422("d1")
& ssSkP402("d0")
& ssSkP403("d1")
& ssSkP402("d1")
& ssSkP403("d0")
& ssSkP400("d0")
& ssSkP401("d1")
& ssSkP400("d1")
& ssSkP401("d0")
& ssSkP449("d1")
& ssSkP448("d0")
& ssSkP449("d0")
& ssSkP448("d1")
& ssSkP450("d1")
& ssSkP450("d0")
& ssSkP453("d0")
& ssSkP454("d1")
& ssSkP453("d1")
& ssSkP454("d0")
& ssSkP451("d0")
& ssSkP452("d1")
& ssSkP451("d1")
& ssSkP452("d0")
& ssSkP457("d0")
& ssSkP458("d1")
& ssSkP457("d1")
& ssSkP458("d0")
& ssSkP455("d0")
& ssSkP456("d1")
& ssSkP455("d1")
& ssSkP456("d0")
& ssSkP459("d0")
& ssSkP459("d1")
& ssSkP461("d1")
& ssSkP460("d0")
& ssSkP461("d0")
& ssSkP460("d1")
& ssSkP465("d1")
& ssSkP464("d0")
& ssSkP465("d0")
& ssSkP464("d1")
& ssSkP463("d1")
& ssSkP462("d0")
& ssSkP463("d0")
& ssSkP462("d1")
& ssSkP469("d1")
& ssSkP468("d0")
& ssSkP469("d0")
& ssSkP468("d1")
& ssSkP467("d1")
& ssSkP466("d0")
& ssSkP467("d0")
& ssSkP466("d1")
& ssSkP429("d1")
& ssSkP428("d0")
& ssSkP429("d0")
& ssSkP428("d1")
& ssSkP427("d1")
& ssSkP426("d0")
& ssSkP427("d0")
& ssSkP426("d1")
& ssSkP431("d0")
& ssSkP432("d1")
& ssSkP431("d1")
& ssSkP432("d0")
& ssSkP430("d1")
& ssSkP430("d0")
& ssSkP435("d0")
& ssSkP436("d1")
& ssSkP435("d1")
& ssSkP436("d0")
& ssSkP433("d0")
& ssSkP434("d1")
& ssSkP433("d1")
& ssSkP434("d0")
& ssSkP439("d0")
& ssSkP439("d1")
& ssSkP437("d0")
& ssSkP438("d1")
& ssSkP437("d1")
& ssSkP438("d0")
& ssSkP443("d1")
& ssSkP442("d0")
& ssSkP443("d0")
& ssSkP442("d1")
& ssSkP441("d1")
& ssSkP440("d0")
& ssSkP441("d0")
& ssSkP440("d1")
& ssSkP447("d1")
& ssSkP446("d0")
& ssSkP447("d0")
& ssSkP446("d1")
& ssSkP445("d1")
& ssSkP444("d0")
& ssSkP445("d0")
& ssSkP444("d1")
& ssSkP358("d1","d1")
& ssSkP358("d0","d0")
& ssSkP358("d1","d0")
& ssSkP358("d0","d1")
& ssSkP373("d1")
& ~ ssSkP372("d0")
& ~ ssSkP373("d0")
& ssSkP372("d1")
& ~ ssSkP370("d0")
& ssSkP370("d1")
& ~ ssSkC10
& ssSkP377("d1")
& ~ ssSkP376("d0")
& ~ ssSkP377("d0")
& ssSkP376("d1")
& ~ ssSkP374("d0")
& ssSkP375("d1")
& ssSkP374("d1")
& ~ ssSkP375("d0")
& ~ ssSkP378("d0")
& ssSkP379("d1")
& ssSkP378("d1")
& ~ ssSkP379("d0")
& ssSkP380("d1")
& ~ ssSkP380("d0")
& ~ ssSkP383("d0")
& ssSkP384("d1")
& ssSkP383("d1")
& ~ ssSkP384("d0")
& ssSkP382("d1")
& ~ ssSkP381("d0")
& ~ ssSkP382("d0")
& ssSkP381("d1")
& ssSkP388("d1")
& ~ ssSkP387("d0")
& ~ ssSkP388("d0")
& ssSkP387("d1")
& ssSkP386("d1")
& ~ ssSkP385("d0")
& ~ ssSkP386("d0")
& ssSkP385("d1")
& ~ ssSkP389("d0")
& ssSkP389("d1")
& ssSkP471("d0")
& ssSkP472("d1")
& ssSkP471("d1")
& ssSkP472("d0")
& ssSkP470("d1")
& ssSkP470("d0")
& ssSkP476("d1")
& ssSkP475("d0")
& ssSkP476("d0")
& ssSkP475("d1")
& ssSkP371("d0","d1")
& ssSkP371("d1","d0")
& ssSkP473("d0")
& ssSkP474("d1")
& ssSkP371("d1","d1")
& ssSkP371("d0","d0")
& ssSkP473("d1")
& ssSkP474("d0")
& ssSkP359("d1")
& ssSkP479("d0")
& ~ ssSkP359("d0")
& ~ ssSkP479("d1")
& ~ ssSkP478("d1")
& ssSkP477("d0")
& ssSkP357("d1")
& ssSkP478("d0")
& ssSkP477("d1")
& ssSkP357("d0")
& ~ ssSkP361("d0")
& ssSkP362("d1")
& ssSkP361("d1")
& ~ ssSkP362("d0")
& ssSkP360("d1")
& ~ ssSkP360("d0")
& ssSkP366("d1")
& ~ ssSkP365("d0")
& ~ ssSkP366("d0")
& ssSkP365("d1")
& ssSkP364("d1")
& ~ ssSkP363("d0")
& ~ ssSkP364("d0")
& ssSkP363("d1")
& ~ ssSkP369("d0")
& ssSkP369("d1")
& ssSkP368("d1")
& ~ ssSkP367("d0")
& ~ ssSkP368("d0")
& ssSkP367("d1")
& ssSkP391("d1")
& ~ ssSkP390("d0")
& ~ ssSkP391("d0")
& ssSkP390("d1")
& ssSkP395("d1")
& ~ ssSkP394("d0")
& ~ ssSkP395("d0")
& ssSkP394("d1")
& ~ ssSkP392("d0")
& ssSkP393("d1")
& ssSkP392("d1")
& ssSkP393("d0")
& ssSkP398("d0")
& ssSkP399("d1")
& ssSkP398("d1")
& ssSkP399("d0")
& ~ ssSkP396("d0")
& ssSkP397("d1")
& ssSkP396("d1")
& ssSkP397("d0")
& ssRr("d1","d1")
& ~ ssRr("d0","d0")
& ssRr("d0","d1")
& ssRr("d1","d0") ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN904-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.03 % Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n002.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Fri Sep 25 02:34:50 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.43 Running: java -jar /export/starexec/sandbox/solver/bin/FMB4J.jar /export/starexec/sandbox/tmp/tmp.k7Njv4V6gr/theBenchmark.cnf 300
% 0.57/0.75 % domain size: 1
% 0.93/0.85 % domain size: 2
% 1.26/0.90 % model found for domain size 2
% 1.26/0.92 % SZS status CounterSatisfiable for theBenchmark
% 1.26/0.92 % SZS output start FiniteModel for theBenchmark
% See solution above
% 1.26/1.01 % FMB4L exiting
%------------------------------------------------------------------------------