%------------------------------------------------------------------------------
% File : FMB4J---0.1
% Problem : SYO581+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n007.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:49:58 PM UTC 2026
% Result : CounterSatisfiable 1.92s 1.06s
% Output : FiniteModel 2.42s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(domain,interpretation-domains,
! [X] :
( X = "d3"
| X = "d2"
| X = "d1"
| X = "d0" ) ).
fof(mappings,interpretation-mappings,
$true ).
fof(predicate_mappings,interpretation-mappings,
( ~ k04_buttercup10389("d1")
& k04_buttercup10389("d0")
& ~ k04_buttercup10389("d3")
& ~ k04_buttercup10389("d2")
& ~ b48_buttercup10489("d1")
& ~ k04_buttercup10385("d1")
& ~ k04_buttercup10382("d2")
& b48_buttercup10489("d0")
& k04_buttercup10385("d0")
& ~ k04_buttercup10382("d3")
& ~ b48_buttercup10489("d3")
& ~ k04_buttercup10385("d3")
& k04_buttercup10382("d0")
& ~ b48_buttercup10489("d2")
& ~ k04_buttercup10385("d2")
& ~ k04_buttercup10382("d1")
& ~ b48_buttercup10487("d3")
& k04_buttercup10391("d0")
& ~ b48_buttercup10487("d2")
& ~ k04_buttercup10391("d1")
& ~ b48_buttercup10487("d1")
& ~ k04_buttercup10391("d2")
& b48_buttercup10487("d0")
& ~ k04_buttercup10391("d3")
& ~ b48_buttercup10483("d3")
& ~ b48_buttercup10483("d2")
& ~ b48_buttercup10483("d1")
& b48_buttercup10483("d0")
& ~ k04_buttercup10397("d2")
& ~ k04_buttercup10397("d3")
& k04_buttercup10397("d0")
& ~ k04_buttercup10397("d1")
& ~ b48_buttercup10479("d2")
& ~ b48_buttercup10478("d1")
& ~ b48_buttercup10479("d3")
& b48_buttercup10478("d0")
& b48_buttercup10479("d0")
& ~ b48_buttercup10478("d3")
& ~ b48_buttercup10479("d1")
& ~ b48_buttercup10478("d2")
& ~ b48_buttercup10474("d1")
& b48_buttercup10474("d0")
& ~ b48_buttercup10474("d3")
& ~ b48_buttercup10474("d2")
& ~ b48_buttercup10471("d2")
& ~ b48_buttercup10471("d3")
& b48_buttercup10471("d0")
& ~ b48_buttercup10471("d1")
& ~ b48_buttercup10029("d3")
& b48_buttercup10029("d2")
& ~ b48_buttercup10029("d1")
& b48_buttercup10029("d0")
& b48_buttercup10022("d0")
& ~ b48_buttercup10022("d1")
& ~ b48_buttercup10022("d2")
& ~ b48_buttercup10022("d3")
& ~ b48_buttercup10021("d3")
& ~ b48_buttercup10021("d2")
& ~ b48_buttercup10021("d1")
& b48_buttercup10021("d0")
& b48_buttercup10019("d0")
& ~ b48_buttercup10019("d1")
& ~ b48_buttercup10019("d2")
& ~ b48_buttercup10019("d3")
& ~ b48_buttercup10496("d1")
& ~ b48_buttercup10013("d2")
& b48_buttercup10496("d0")
& ~ b48_buttercup10013("d3")
& ~ b48_buttercup10496("d3")
& b48_buttercup10013("d0")
& ~ b48_buttercup10496("d2")
& ~ b48_buttercup10013("d1")
& ~ b48_buttercup10493("d2")
& ~ b48_buttercup10493("d3")
& b48_buttercup10493("d0")
& ~ b48_buttercup10493("d1")
& ~ b48_buttercup10490("d3")
& ~ b48_buttercup10490("d2")
& ~ b48_buttercup10490("d1")
& b48_buttercup10490("d0")
& ~ b48_buttercup10046("d2")
& ~ b48_buttercup10046("d3")
& b48_buttercup10046("d0")
& ~ b48_buttercup10046("d1")
& ~ b48_buttercup10034("d1")
& ~ b48_buttercup10035("d2")
& b48_buttercup10034("d0")
& ~ b48_buttercup10035("d3")
& ~ b48_buttercup10034("d3")
& b48_buttercup10035("d0")
& ~ b48_buttercup10034("d2")
& ~ b48_buttercup10035("d1")
& ~ b48_buttercup10031("d2")
& ~ b48_buttercup10031("d3")
& b48_buttercup10031("d0")
& ~ b48_buttercup10031("d1")
& ~ b48_buttercup10068("d2")
& ~ b48_buttercup10068("d3")
& b48_buttercup10068("d0")
& ~ b48_buttercup10068("d1")
& ~ b48_buttercup10065("d3")
& ~ b48_buttercup10065("d2")
& ~ b48_buttercup10065("d1")
& b48_buttercup10065("d0")
& ~ b48_buttercup10058("d3")
& ~ b48_buttercup10058("d2")
& ~ b48_buttercup10058("d1")
& b48_buttercup10058("d0")
& ~ b48_buttercup10054("d3")
& ~ b48_buttercup10052("d1")
& ~ b48_buttercup10054("d2")
& b48_buttercup10052("d0")
& ~ b48_buttercup10054("d1")
& ~ b48_buttercup10052("d3")
& b48_buttercup10054("d0")
& ~ b48_buttercup10052("d2")
& ~ b48_buttercup10050("d3")
& ~ b48_buttercup10050("d2")
& ~ b48_buttercup10050("d1")
& b48_buttercup10050("d0")
& ~ k04_buttercup10303("d3")
& ~ k04_buttercup10303("d2")
& k04_buttercup10303("d1")
& k04_buttercup10303("d0")
& ~ b48_buttercup10405("d1")
& b48_buttercup10405("d0")
& ~ b48_buttercup10405("d3")
& ~ b48_buttercup10405("d2")
& ~ b48_buttercup10402("d2")
& ~ b48_buttercup10402("d3")
& b48_buttercup10402("d0")
& ~ b48_buttercup10402("d1")
& ~ k04_buttercup10316("d1")
& k04_buttercup10316("d0")
& ~ k04_buttercup10316("d3")
& ~ k04_buttercup10316("d2")
& ~ k04_buttercup10312("d1")
& k04_buttercup10312("d0")
& ~ k04_buttercup10312("d3")
& ~ k04_buttercup10312("d2")
& ~ k04_buttercup10329("d3")
& ~ k04_buttercup10329("d2")
& ~ k04_buttercup10329("d1")
& k04_buttercup10329("d0")
& ~ k04_buttercup10325("d3")
& ~ k04_buttercup10325("d2")
& ~ k04_buttercup10325("d1")
& k04_buttercup10325("d0")
& ~ b48_buttercup10427("d1")
& b48_buttercup10427("d0")
& ~ b48_buttercup10427("d3")
& ~ b48_buttercup10427("d2")
& b48_buttercup10422("d0")
& ~ b48_buttercup10422("d1")
& ~ b48_buttercup10422("d2")
& ~ b48_buttercup10422("d3")
& ~ b48_buttercup10421("d3")
& ~ b48_buttercup10421("d2")
& b48_buttercup10421("d1")
& b48_buttercup10421("d0")
& k04_buttercup10337("d0")
& k04_buttercup10337("d1")
& ~ k04_buttercup10337("d2")
& ~ k04_buttercup10337("d3")
& ~ b48_buttercup10417("d2")
& k04_buttercup10333("d0")
& ~ b48_buttercup10417("d3")
& ~ k04_buttercup10333("d1")
& b48_buttercup10417("d0")
& ~ k04_buttercup10333("d2")
& b48_buttercup10417("d1")
& ~ k04_buttercup10333("d3")
& b48_buttercup10411("d0")
& ~ b48_buttercup10411("d1")
& ~ b48_buttercup10411("d2")
& ~ b48_buttercup10411("d3")
& ~ b48_buttercup10410("d3")
& ~ b48_buttercup10410("d2")
& ~ b48_buttercup10410("d1")
& b48_buttercup10410("d0")
& ~ k04_buttercup10347("d3")
& ~ k04_buttercup10347("d2")
& ~ k04_buttercup10347("d1")
& k04_buttercup10347("d0")
& ~ k04_buttercup10342("d2")
& ~ k04_buttercup10342("d3")
& k04_buttercup10342("d0")
& ~ k04_buttercup10342("d1")
& ~ b48_buttercup10446("d2")
& ~ b48_buttercup10446("d3")
& b48_buttercup10446("d0")
& ~ b48_buttercup10446("d1")
& ~ b48_buttercup10443("d3")
& ~ b48_buttercup10442("d2")
& ~ b48_buttercup10441("d1")
& b48_buttercup10440("d0")
& ~ b48_buttercup10443("d2")
& ~ b48_buttercup10442("d3")
& ~ b48_buttercup10440("d1")
& b48_buttercup10441("d0")
& ~ b48_buttercup10443("d1")
& b48_buttercup10442("d0")
& ~ b48_buttercup10441("d3")
& ~ b48_buttercup10440("d2")
& b48_buttercup10443("d0")
& ~ b48_buttercup10442("d1")
& ~ b48_buttercup10440("d3")
& ~ b48_buttercup10441("d2")
& ~ k04_buttercup10356("d1")
& k04_buttercup10356("d0")
& ~ k04_buttercup10356("d3")
& ~ k04_buttercup10356("d2")
& ~ b48_buttercup10434("d1")
& k04_buttercup10351("d0")
& b48_buttercup10434("d0")
& ~ k04_buttercup10351("d1")
& ~ b48_buttercup10434("d3")
& ~ k04_buttercup10351("d2")
& ~ b48_buttercup10434("d2")
& ~ k04_buttercup10351("d3")
& ~ k04_buttercup10369("d3")
& ~ k04_buttercup10369("d2")
& ~ k04_buttercup10369("d1")
& k04_buttercup10369("d0")
& k04_buttercup10364("d2")
& ~ k04_buttercup10364("d3")
& k04_buttercup10364("d0")
& ~ k04_buttercup10364("d1")
& ~ b48_buttercup10469("d3")
& ~ b48_buttercup10467("d1")
& b48_buttercup10466("d0")
& ~ b48_buttercup10469("d2")
& b48_buttercup10467("d0")
& ~ b48_buttercup10466("d1")
& ~ b48_buttercup10469("d1")
& ~ b48_buttercup10467("d3")
& ~ b48_buttercup10466("d2")
& b48_buttercup10469("d0")
& ~ b48_buttercup10467("d2")
& ~ b48_buttercup10466("d3")
& ~ b48_buttercup10465("d3")
& ~ b48_buttercup10465("d2")
& ~ b48_buttercup10465("d1")
& b48_buttercup10465("d0")
& ~ b48_buttercup10460("d2")
& ~ b48_buttercup10460("d3")
& b48_buttercup10460("d0")
& ~ b48_buttercup10460("d1")
& ~ k04_buttercup10376("d3")
& ~ k04_buttercup10376("d2")
& ~ k04_buttercup10376("d1")
& k04_buttercup10376("d0")
& ~ b48_buttercup10458("d3")
& ~ b48_buttercup10456("d1")
& k04_buttercup10373("d0")
& ~ k04_buttercup10371("d2")
& ~ b48_buttercup10458("d2")
& b48_buttercup10456("d0")
& ~ k04_buttercup10373("d1")
& ~ k04_buttercup10371("d3")
& ~ b48_buttercup10458("d1")
& ~ b48_buttercup10456("d3")
& ~ k04_buttercup10373("d2")
& k04_buttercup10371("d0")
& b48_buttercup10458("d0")
& ~ b48_buttercup10456("d2")
& ~ k04_buttercup10373("d3")
& ~ k04_buttercup10371("d1")
& b48_buttercup10451("d0")
& ~ b48_buttercup10454("d3")
& k04_buttercup10380("d0")
& ~ b48_buttercup10451("d1")
& ~ b48_buttercup10454("d2")
& ~ k04_buttercup10380("d1")
& ~ b48_buttercup10451("d2")
& ~ b48_buttercup10454("d1")
& ~ k04_buttercup10380("d2")
& ~ b48_buttercup10451("d3")
& b48_buttercup10454("d0")
& ~ k04_buttercup10380("d3")
& ~ k04_buttercup10408("d1")
& ~ k04_buttercup10406("d3")
& k04_buttercup10408("d0")
& ~ k04_buttercup10406("d2")
& ~ k04_buttercup10408("d3")
& ~ k04_buttercup10406("d1")
& ~ k04_buttercup10408("d2")
& k04_buttercup10406("d0")
& b48_buttercup10507("d0")
& ~ k04_buttercup10404("d1")
& ~ b48_buttercup10507("d1")
& k04_buttercup10404("d0")
& ~ b48_buttercup10507("d2")
& ~ k04_buttercup10404("d3")
& ~ b48_buttercup10507("d3")
& ~ k04_buttercup10404("d2")
& ~ k04_buttercup10400("d1")
& k04_buttercup10400("d0")
& ~ k04_buttercup10400("d3")
& ~ k04_buttercup10400("d2")
& ~ b48_buttercup10502("d3")
& ~ b48_buttercup10502("d2")
& ~ b48_buttercup10502("d1")
& b48_buttercup10502("d0")
& ~ k04_buttercup10419("d1")
& k04_buttercup10419("d0")
& ~ k04_buttercup10419("d3")
& k04_buttercup10419("d2")
& ~ k04_buttercup10415("d1")
& k04_buttercup10415("d0")
& ~ k04_buttercup10415("d3")
& ~ k04_buttercup10415("d2")
& ~ b48_buttercup10085("d1")
& ~ b48_buttercup10086("d2")
& b48_buttercup10085("d0")
& ~ b48_buttercup10086("d3")
& ~ b48_buttercup10085("d3")
& b48_buttercup10086("d0")
& ~ b48_buttercup10085("d2")
& ~ b48_buttercup10086("d1")
& ~ b48_buttercup10082("d2")
& ~ b48_buttercup10082("d3")
& b48_buttercup10082("d0")
& ~ b48_buttercup10082("d1")
& ~ b48_buttercup10076("d3")
& ~ b48_buttercup10075("d2")
& ~ b48_buttercup10076("d2")
& ~ b48_buttercup10075("d3")
& ~ b48_buttercup10076("d1")
& b48_buttercup10075("d0")
& b48_buttercup10076("d0")
& ~ b48_buttercup10075("d1")
& ~ b48_buttercup10072("d3")
& ~ b48_buttercup10070("d1")
& ~ b48_buttercup10072("d2")
& b48_buttercup10070("d0")
& ~ b48_buttercup10072("d1")
& ~ b48_buttercup10070("d3")
& b48_buttercup10072("d0")
& ~ b48_buttercup10070("d2")
& ~ b48_buttercup10092("d1")
& b48_buttercup10092("d0")
& ~ b48_buttercup10092("d3")
& ~ b48_buttercup10092("d2")
& b48_buttercup10367("d0")
& ~ b48_buttercup10367("d1")
& ~ b48_buttercup10367("d2")
& ~ b48_buttercup10367("d3")
& ~ b48_buttercup10362("d3")
& ~ b48_buttercup10362("d2")
& ~ b48_buttercup10362("d1")
& b48_buttercup10362("d0")
& ~ b48_buttercup10353("d1")
& b48_buttercup10352("d0")
& ~ k04_buttercup10282("d1")
& b48_buttercup10353("d0")
& ~ b48_buttercup10352("d1")
& k04_buttercup10282("d0")
& ~ b48_buttercup10353("d3")
& ~ b48_buttercup10352("d2")
& ~ k04_buttercup10282("d3")
& ~ b48_buttercup10353("d2")
& ~ b48_buttercup10352("d3")
& ~ k04_buttercup10282("d2")
& ~ b48_buttercup10386("d1")
& ~ k04_buttercup10293("d1")
& b48_buttercup10386("d0")
& k04_buttercup10293("d0")
& ~ b48_buttercup10386("d3")
& ~ k04_buttercup10293("d3")
& ~ b48_buttercup10386("d2")
& ~ k04_buttercup10293("d2")
& b48_buttercup10381("d0")
& ~ b48_buttercup10383("d2")
& ~ b48_buttercup10381("d1")
& ~ b48_buttercup10383("d3")
& ~ b48_buttercup10381("d2")
& b48_buttercup10383("d0")
& ~ b48_buttercup10381("d3")
& ~ b48_buttercup10383("d1")
& ~ k04_buttercup10298("d2")
& ~ k04_buttercup10298("d3")
& k04_buttercup10298("d0")
& ~ k04_buttercup10298("d1")
& b48_buttercup10378("d0")
& k04_buttercup10296("d0")
& ~ b48_buttercup10378("d1")
& ~ k04_buttercup10296("d1")
& ~ b48_buttercup10378("d2")
& ~ k04_buttercup10296("d2")
& ~ b48_buttercup10378("d3")
& ~ k04_buttercup10296("d3")
& ~ b48_buttercup10377("d3")
& b48_buttercup10374("d0")
& ~ b48_buttercup10377("d2")
& ~ b48_buttercup10374("d1")
& ~ b48_buttercup10377("d1")
& ~ b48_buttercup10374("d2")
& b48_buttercup10377("d0")
& ~ b48_buttercup10374("d3")
& b48_buttercup10370("d0")
& ~ b48_buttercup10370("d1")
& ~ b48_buttercup10370("d2")
& ~ b48_buttercup10370("d3")
& ~ b48_buttercup10398("d2")
& ~ b48_buttercup10398("d3")
& b48_buttercup10398("d0")
& ~ b48_buttercup10398("d1")
& ~ b48_buttercup10394("d2")
& ~ b48_buttercup10394("d3")
& b48_buttercup10394("d0")
& ~ b48_buttercup10394("d1")
& b48_buttercup10309("d0")
& ~ k04_buttercup10206("d1")
& ~ k04_buttercup10204("d3")
& ~ b48_buttercup10309("d1")
& k04_buttercup10206("d0")
& ~ k04_buttercup10204("d2")
& ~ b48_buttercup10309("d2")
& ~ k04_buttercup10206("d3")
& ~ k04_buttercup10204("d1")
& ~ b48_buttercup10309("d3")
& ~ k04_buttercup10206("d2")
& k04_buttercup10204("d0")
& ~ b48_buttercup10308("d3")
& ~ b48_buttercup10307("d2")
& ~ k04_buttercup10200("d3")
& ~ b48_buttercup10305("d0")
& ~ b48_buttercup10308("d2")
& ~ b48_buttercup10307("d3")
& ~ k04_buttercup10200("d2")
& b48_buttercup10305("d1")
& ~ b48_buttercup10308("d1")
& b48_buttercup10307("d0")
& ~ k04_buttercup10200("d1")
& ~ b48_buttercup10305("d2")
& b48_buttercup10308("d0")
& ~ b48_buttercup10307("d1")
& k04_buttercup10200("d0")
& ~ b48_buttercup10305("d3")
& ~ b48_buttercup10300("d3")
& ~ b48_buttercup10300("d2")
& b48_buttercup10300("d1")
& b48_buttercup10300("d0")
& ~ k04_buttercup10219("d3")
& ~ k04_buttercup10219("d2")
& ~ k04_buttercup10219("d1")
& k04_buttercup10219("d0")
& ~ k04_buttercup10213("d1")
& k04_buttercup10213("d0")
& ~ k04_buttercup10213("d3")
& ~ k04_buttercup10213("d2")
& ~ k04_buttercup10225("d2")
& ~ k04_buttercup10225("d3")
& k04_buttercup10225("d0")
& ~ k04_buttercup10225("d1")
& k04_buttercup10221("d2")
& ~ k04_buttercup10221("d3")
& k04_buttercup10221("d0")
& ~ k04_buttercup10221("d1")
& ~ b48_buttercup10326("d3")
& ~ b48_buttercup10326("d2")
& ~ b48_buttercup10326("d1")
& b48_buttercup10326("d0")
& ~ b48_buttercup10322("d3")
& ~ b48_buttercup10320("d1")
& ~ b48_buttercup10322("d2")
& b48_buttercup10320("d0")
& ~ b48_buttercup10322("d1")
& ~ b48_buttercup10320("d3")
& b48_buttercup10322("d0")
& ~ b48_buttercup10320("d2")
& k04_buttercup10238("d0")
& ~ k04_buttercup10236("d2")
& ~ k04_buttercup10238("d1")
& ~ k04_buttercup10236("d3")
& ~ k04_buttercup10238("d2")
& k04_buttercup10236("d0")
& ~ k04_buttercup10238("d3")
& ~ k04_buttercup10236("d1")
& ~ b48_buttercup10318("d2")
& k04_buttercup10234("d0")
& ~ b48_buttercup10318("d3")
& ~ k04_buttercup10234("d1")
& b48_buttercup10318("d0")
& ~ k04_buttercup10234("d2")
& ~ b48_buttercup10318("d1")
& ~ k04_buttercup10234("d3")
& ~ b48_buttercup10313("d1")
& b48_buttercup10313("d0")
& ~ b48_buttercup10313("d3")
& ~ b48_buttercup10313("d2")
& ~ k04_buttercup10244("d3")
& ~ k04_buttercup10244("d2")
& ~ k04_buttercup10244("d1")
& k04_buttercup10244("d0")
& ~ b48_buttercup10348("d3")
& ~ b48_buttercup10348("d2")
& ~ b48_buttercup10348("d1")
& b48_buttercup10348("d0")
& ~ b48_buttercup10344("d3")
& ~ b48_buttercup10343("d2")
& ~ b48_buttercup10344("d2")
& ~ b48_buttercup10343("d3")
& ~ b48_buttercup10344("d1")
& b48_buttercup10343("d0")
& b48_buttercup10344("d0")
& ~ b48_buttercup10343("d1")
& b48_buttercup10334("d0")
& k04_buttercup10252("d0")
& ~ b48_buttercup10334("d1")
& ~ k04_buttercup10252("d1")
& ~ b48_buttercup10334("d2")
& ~ k04_buttercup10252("d2")
& ~ b48_buttercup10334("d3")
& ~ k04_buttercup10252("d3")
& ~ b48_buttercup10332("d2")
& ~ b48_buttercup10332("d3")
& b48_buttercup10332("d0")
& ~ b48_buttercup10332("d1")
& ~ k04_buttercup10147("d1")
& k04_buttercup10147("d0")
& ~ k04_buttercup10147("d3")
& ~ k04_buttercup10147("d2")
& ~ b48_buttercup10248("d2")
& k04_buttercup10142("d0")
& ~ b48_buttercup10248("d3")
& ~ k04_buttercup10142("d1")
& b48_buttercup10248("d0")
& ~ k04_buttercup10142("d2")
& ~ b48_buttercup10248("d1")
& ~ k04_buttercup10142("d3")
& ~ b48_buttercup10240("d2")
& ~ b48_buttercup10240("d3")
& b48_buttercup10240("d0")
& ~ b48_buttercup10240("d1")
& k04_buttercup10153("d0")
& ~ k04_buttercup10153("d1")
& ~ k04_buttercup10153("d2")
& ~ k04_buttercup10153("d3")
& b48_buttercup10231("d0")
& ~ b48_buttercup10231("d1")
& ~ b48_buttercup10231("d2")
& ~ b48_buttercup10231("d3")
& ~ b48_buttercup10269("d1")
& k04_buttercup10164("d0")
& b48_buttercup10269("d0")
& ~ k04_buttercup10164("d1")
& ~ b48_buttercup10269("d3")
& ~ k04_buttercup10164("d2")
& ~ b48_buttercup10269("d2")
& ~ k04_buttercup10164("d3")
& ~ k04_buttercup10172("d1")
& k04_buttercup10172("d0")
& ~ k04_buttercup10172("d3")
& ~ k04_buttercup10172("d2")
& ~ k04_buttercup10181("d3")
& ~ k04_buttercup10181("d2")
& ~ k04_buttercup10181("d1")
& k04_buttercup10181("d0")
& ~ k04_buttercup10184("d2")
& ~ k04_buttercup10184("d3")
& k04_buttercup10184("d0")
& ~ k04_buttercup10184("d1")
& ~ b48_buttercup10289("d3")
& ~ b48_buttercup10289("d2")
& ~ b48_buttercup10289("d1")
& b48_buttercup10289("d0")
& ~ k04_buttercup10190("d1")
& k04_buttercup10190("d0")
& ~ k04_buttercup10190("d3")
& ~ k04_buttercup10190("d2")
& ~ b48_buttercup10299("d2")
& ~ b48_buttercup10299("d3")
& b48_buttercup10299("d0")
& ~ b48_buttercup10299("d1")
& ~ b48_buttercup10294("d1")
& b48_buttercup10294("d0")
& ~ b48_buttercup10294("d3")
& ~ b48_buttercup10294("d2")
& ~ b48_buttercup10291("d2")
& ~ b48_buttercup10291("d3")
& b48_buttercup10291("d0")
& ~ b48_buttercup10291("d1")
& ~ k04_buttercup10547("d1")
& ~ k04_buttercup10544("d2")
& k04_buttercup10546("d0")
& k04_buttercup10547("d0")
& ~ k04_buttercup10544("d3")
& ~ k04_buttercup10546("d1")
& ~ k04_buttercup10547("d3")
& ~ k04_buttercup10546("d2")
& k04_buttercup10544("d0")
& ~ k04_buttercup10547("d2")
& ~ k04_buttercup10546("d3")
& ~ k04_buttercup10544("d1")
& b48_buttercup10642("d0")
& ~ b48_buttercup10642("d1")
& ~ b48_buttercup10642("d2")
& ~ b48_buttercup10642("d3")
& ~ b48_buttercup10640("d2")
& ~ b48_buttercup10640("d3")
& b48_buttercup10640("d0")
& ~ b48_buttercup10640("d1")
& ~ k04_buttercup10559("d2")
& ~ k04_buttercup10559("d3")
& k04_buttercup10559("d0")
& ~ k04_buttercup10559("d1")
& ~ k04_buttercup10555("d2")
& ~ k04_buttercup10555("d3")
& k04_buttercup10555("d0")
& ~ k04_buttercup10555("d1")
& ~ b48_buttercup10638("d3")
& ~ b48_buttercup10636("d1")
& ~ k04_buttercup10551("d2")
& ~ b48_buttercup10638("d2")
& b48_buttercup10636("d0")
& ~ k04_buttercup10551("d3")
& ~ b48_buttercup10638("d1")
& ~ b48_buttercup10636("d3")
& k04_buttercup10551("d0")
& b48_buttercup10638("d0")
& ~ b48_buttercup10636("d2")
& ~ k04_buttercup10551("d1")
& ~ b48_buttercup10632("d1")
& b48_buttercup10632("d0")
& ~ b48_buttercup10632("d3")
& ~ b48_buttercup10632("d2")
& ~ k04_buttercup10567("d3")
& ~ k04_buttercup10567("d2")
& ~ k04_buttercup10567("d1")
& k04_buttercup10567("d0")
& ~ k04_buttercup10578("d3")
& ~ k04_buttercup10578("d2")
& ~ k04_buttercup10578("d1")
& k04_buttercup10578("d0")
& k04_buttercup10586("d0")
& b48_buttercup10208("d2")
& k04_buttercup10100("d2")
& ~ k04_buttercup10586("d1")
& ~ b48_buttercup10208("d3")
& ~ k04_buttercup10100("d3")
& ~ k04_buttercup10586("d2")
& b48_buttercup10208("d0")
& k04_buttercup10100("d0")
& ~ k04_buttercup10586("d3")
& ~ b48_buttercup10208("d1")
& ~ k04_buttercup10100("d1")
& ~ k04_buttercup10581("d3")
& ~ k04_buttercup10581("d2")
& ~ k04_buttercup10581("d1")
& k04_buttercup10581("d0")
& k04_buttercup10117("d0")
& ~ k04_buttercup10599("d2")
& ~ k04_buttercup10117("d1")
& ~ k04_buttercup10599("d3")
& ~ k04_buttercup10117("d2")
& k04_buttercup10599("d0")
& ~ k04_buttercup10117("d3")
& ~ k04_buttercup10599("d1")
& k04_buttercup10593("d0")
& ~ k04_buttercup10593("d1")
& ~ k04_buttercup10593("d2")
& ~ k04_buttercup10593("d3")
& ~ b48_buttercup10229("d1")
& ~ k04_buttercup10125("d1")
& b48_buttercup10228("d0")
& b48_buttercup10229("d0")
& k04_buttercup10125("d0")
& ~ b48_buttercup10228("d1")
& ~ b48_buttercup10229("d3")
& ~ k04_buttercup10125("d3")
& ~ b48_buttercup10228("d2")
& ~ b48_buttercup10229("d2")
& ~ k04_buttercup10125("d2")
& ~ b48_buttercup10228("d3")
& ~ b48_buttercup10227("d3")
& ~ b48_buttercup10227("d2")
& ~ b48_buttercup10227("d1")
& b48_buttercup10227("d0")
& b48_buttercup10220("d0")
& ~ b48_buttercup10222("d2")
& ~ b48_buttercup10220("d1")
& ~ b48_buttercup10222("d3")
& ~ b48_buttercup10220("d2")
& b48_buttercup10222("d0")
& ~ b48_buttercup10220("d3")
& ~ b48_buttercup10222("d1")
& k04_buttercup10139("d0")
& k04_buttercup10139("d1")
& ~ k04_buttercup10139("d2")
& ~ k04_buttercup10139("d3")
& b48_buttercup10217("d0")
& k04_buttercup10135("d0")
& ~ b48_buttercup10217("d1")
& ~ k04_buttercup10135("d1")
& ~ b48_buttercup10217("d2")
& ~ k04_buttercup10135("d2")
& ~ b48_buttercup10217("d3")
& ~ k04_buttercup10135("d3")
& ~ k04_buttercup10132("d1")
& ~ b48_buttercup10214("d1")
& k04_buttercup10132("d0")
& b48_buttercup10214("d0")
& ~ k04_buttercup10132("d3")
& ~ b48_buttercup10214("d3")
& ~ k04_buttercup10132("d2")
& b48_buttercup10214("d2")
& ~ b48_buttercup10210("d1")
& b48_buttercup10210("d0")
& ~ b48_buttercup10210("d3")
& ~ b48_buttercup10210("d2")
& ~ k04_buttercup10602("d1")
& k04_buttercup10602("d0")
& ~ k04_buttercup10602("d3")
& ~ k04_buttercup10602("d2")
& ~ k04_buttercup10608("d3")
& k04_buttercup10608("d2")
& ~ k04_buttercup10608("d1")
& k04_buttercup10608("d0")
& ~ k04_buttercup10611("d3")
& ~ k04_buttercup10611("d2")
& ~ k04_buttercup10611("d1")
& k04_buttercup10611("d0")
& ~ k04_buttercup10619("d3")
& k04_buttercup10619("d2")
& k04_buttercup10619("d1")
& k04_buttercup10619("d0")
& ~ k04_buttercup10628("d1")
& ~ k04_buttercup10626("d3")
& k04_buttercup10628("d0")
& ~ k04_buttercup10626("d2")
& ~ k04_buttercup10628("d3")
& ~ k04_buttercup10626("d1")
& ~ k04_buttercup10628("d2")
& k04_buttercup10626("d0")
& ~ k04_buttercup10622("d3")
& ~ k04_buttercup10622("d2")
& k04_buttercup10622("d1")
& k04_buttercup10622("d0")
& k04_buttercup10620("d1")
& k04_buttercup10620("d0")
& ~ k04_buttercup10620("d3")
& k04_buttercup10620("d2")
& ~ k04_buttercup10639("d1")
& ~ k04_buttercup10637("d3")
& k04_buttercup10639("d0")
& ~ k04_buttercup10637("d2")
& ~ k04_buttercup10639("d3")
& ~ k04_buttercup10637("d1")
& ~ k04_buttercup10639("d2")
& k04_buttercup10637("d0")
& ~ k04_buttercup10635("d1")
& k04_buttercup10635("d0")
& ~ k04_buttercup10635("d3")
& ~ k04_buttercup10635("d2")
& ~ k04_buttercup10631("d1")
& k04_buttercup10631("d0")
& ~ k04_buttercup10631("d3")
& ~ k04_buttercup10631("d2")
& ~ k04_buttercup10643("d2")
& ~ k04_buttercup10643("d3")
& k04_buttercup10643("d0")
& ~ k04_buttercup10643("d1")
& k04_buttercup10641("d0")
& ~ k04_buttercup10641("d1")
& ~ k04_buttercup10641("d2")
& ~ k04_buttercup10641("d3")
& ~ k04_buttercup10028("d3")
& ~ k04_buttercup10028("d2")
& ~ k04_buttercup10028("d1")
& k04_buttercup10028("d0")
& ~ k04_buttercup10026("d1")
& k04_buttercup10026("d0")
& ~ k04_buttercup10026("d3")
& ~ k04_buttercup10026("d2")
& b48_buttercup10121("d0")
& ~ b48_buttercup10121("d1")
& ~ b48_buttercup10121("d2")
& ~ b48_buttercup10121("d3")
& ~ b48_buttercup10120("d3")
& ~ b48_buttercup10120("d2")
& ~ b48_buttercup10120("d1")
& b48_buttercup10120("d0")
& ~ k04_buttercup10039("d3")
& ~ k04_buttercup10039("d2")
& ~ k04_buttercup10039("d1")
& k04_buttercup10039("d0")
& ~ b48_buttercup10119("d1")
& b48_buttercup10119("d0")
& ~ b48_buttercup10119("d3")
& ~ b48_buttercup10119("d2")
& ~ b48_buttercup10115("d1")
& ~ k04_buttercup10033("d1")
& b48_buttercup10115("d0")
& k04_buttercup10033("d0")
& ~ b48_buttercup10115("d3")
& ~ k04_buttercup10033("d3")
& ~ b48_buttercup10115("d2")
& ~ k04_buttercup10033("d2")
& ~ b48_buttercup10596("d2")
& ~ b48_buttercup10111("d1")
& b48_buttercup10110("d0")
& ~ b48_buttercup10596("d3")
& b48_buttercup10111("d0")
& ~ b48_buttercup10110("d1")
& b48_buttercup10596("d0")
& ~ b48_buttercup10111("d3")
& ~ b48_buttercup10110("d2")
& ~ b48_buttercup10596("d1")
& ~ b48_buttercup10111("d2")
& ~ b48_buttercup10110("d3")
& ~ k04_buttercup10049("d2")
& ~ k04_buttercup10049("d3")
& k04_buttercup10049("d0")
& ~ k04_buttercup10049("d1")
& ~ k04_buttercup10048("d1")
& k04_buttercup10048("d0")
& ~ k04_buttercup10048("d3")
& ~ k04_buttercup10048("d2")
& b48_buttercup10143("d0")
& ~ k04_buttercup10051("d1")
& ~ b48_buttercup10143("d1")
& k04_buttercup10051("d0")
& ~ b48_buttercup10143("d2")
& ~ k04_buttercup10051("d3")
& ~ b48_buttercup10143("d3")
& ~ k04_buttercup10051("d2")
& ~ k04_buttercup10057("d3")
& ~ k04_buttercup10057("d2")
& ~ k04_buttercup10057("d1")
& k04_buttercup10057("d0")
& ~ k04_buttercup10053("d3")
& k04_buttercup10053("d2")
& ~ k04_buttercup10053("d1")
& k04_buttercup10053("d0")
& ~ b48_buttercup10134("d2")
& ~ b48_buttercup10133("d1")
& k04_buttercup10061("d0")
& ~ b48_buttercup10134("d3")
& b48_buttercup10133("d0")
& ~ k04_buttercup10061("d1")
& b48_buttercup10134("d0")
& ~ b48_buttercup10133("d3")
& ~ k04_buttercup10061("d2")
& ~ b48_buttercup10134("d1")
& ~ b48_buttercup10133("d2")
& ~ k04_buttercup10061("d3")
& ~ b48_buttercup10130("d2")
& ~ b48_buttercup10130("d3")
& b48_buttercup10130("d0")
& ~ b48_buttercup10130("d1")
& ~ k04_buttercup10067("d2")
& ~ k04_buttercup10067("d3")
& k04_buttercup10067("d0")
& ~ k04_buttercup10067("d1")
& b48_buttercup10169("d0")
& ~ k04_buttercup10064("d3")
& ~ b48_buttercup10169("d1")
& ~ k04_buttercup10064("d2")
& ~ b48_buttercup10169("d2")
& ~ k04_buttercup10064("d1")
& ~ b48_buttercup10169("d3")
& k04_buttercup10064("d0")
& ~ b48_buttercup10167("d2")
& ~ b48_buttercup10166("d1")
& ~ b48_buttercup10167("d3")
& b48_buttercup10166("d0")
& b48_buttercup10167("d0")
& ~ b48_buttercup10166("d3")
& ~ b48_buttercup10167("d1")
& ~ b48_buttercup10166("d2")
& b48_buttercup10161("d0")
& ~ b48_buttercup10161("d1")
& ~ b48_buttercup10161("d2")
& ~ b48_buttercup10161("d3")
& ~ b48_buttercup10160("d3")
& ~ b48_buttercup10160("d2")
& ~ b48_buttercup10160("d1")
& b48_buttercup10160("d0")
& ~ k04_buttercup10079("d3")
& ~ k04_buttercup10079("d2")
& ~ k04_buttercup10079("d1")
& k04_buttercup10079("d0")
& ~ b48_buttercup10159("d1")
& b48_buttercup10158("d0")
& ~ k04_buttercup10074("d2")
& b48_buttercup10159("d0")
& ~ b48_buttercup10158("d1")
& ~ k04_buttercup10074("d3")
& ~ b48_buttercup10159("d3")
& ~ b48_buttercup10158("d2")
& k04_buttercup10074("d0")
& ~ b48_buttercup10159("d2")
& ~ b48_buttercup10158("d3")
& ~ k04_buttercup10074("d1")
& ~ b48_buttercup10156("d2")
& b48_buttercup10154("d0")
& ~ k04_buttercup10084("d1")
& ~ b48_buttercup10156("d3")
& ~ b48_buttercup10154("d1")
& k04_buttercup10084("d0")
& b48_buttercup10156("d0")
& ~ b48_buttercup10154("d2")
& ~ k04_buttercup10084("d3")
& ~ b48_buttercup10156("d1")
& ~ b48_buttercup10154("d3")
& ~ k04_buttercup10084("d2")
& b48_buttercup10150("d0")
& ~ b48_buttercup10150("d1")
& ~ b48_buttercup10150("d2")
& ~ b48_buttercup10150("d3")
& ~ k04_buttercup10089("d2")
& ~ k04_buttercup10089("d3")
& k04_buttercup10089("d0")
& ~ k04_buttercup10089("d1")
& k04_buttercup10095("d1")
& k04_buttercup10095("d0")
& ~ k04_buttercup10095("d3")
& ~ k04_buttercup10095("d2")
& ~ b48_buttercup10186("d3")
& ~ b48_buttercup10186("d2")
& ~ b48_buttercup10186("d1")
& b48_buttercup10186("d0")
& ~ b48_buttercup10180("d1")
& b48_buttercup10180("d0")
& ~ b48_buttercup10180("d3")
& ~ b48_buttercup10180("d2")
& ~ k04_buttercup10097("d3")
& ~ k04_buttercup10096("d2")
& ~ k04_buttercup10097("d2")
& ~ k04_buttercup10096("d3")
& ~ k04_buttercup10097("d1")
& k04_buttercup10096("d0")
& k04_buttercup10097("d0")
& ~ k04_buttercup10096("d1")
& ~ b48_buttercup10179("d3")
& b48_buttercup10176("d0")
& ~ b48_buttercup10179("d2")
& ~ b48_buttercup10176("d1")
& ~ b48_buttercup10179("d1")
& ~ b48_buttercup10176("d2")
& b48_buttercup10179("d0")
& ~ b48_buttercup10176("d3")
& ~ b48_buttercup10174("d2")
& ~ b48_buttercup10173("d1")
& ~ b48_buttercup10174("d3")
& b48_buttercup10173("d0")
& b48_buttercup10174("d0")
& ~ b48_buttercup10173("d3")
& ~ b48_buttercup10174("d1")
& ~ b48_buttercup10173("d2")
& ~ b48_buttercup10170("d2")
& ~ b48_buttercup10170("d3")
& b48_buttercup10170("d0")
& ~ b48_buttercup10170("d1")
& ~ k04_buttercup10424("d3")
& k04_buttercup10425("d0")
& ~ k04_buttercup10424("d2")
& ~ k04_buttercup10425("d1")
& ~ k04_buttercup10425("d2")
& ~ k04_buttercup10424("d1")
& ~ k04_buttercup10425("d3")
& k04_buttercup10424("d0")
& ~ b48_buttercup10526("d1")
& b48_buttercup10526("d0")
& ~ b48_buttercup10526("d3")
& ~ b48_buttercup10526("d2")
& b48_buttercup10521("d0")
& ~ b48_buttercup10521("d1")
& ~ b48_buttercup10521("d2")
& ~ b48_buttercup10521("d3")
& ~ b48_buttercup10520("d3")
& ~ b48_buttercup10520("d2")
& ~ b48_buttercup10520("d1")
& b48_buttercup10520("d0")
& ~ b48_buttercup10519("d1")
& b48_buttercup10518("d0")
& ~ k04_buttercup10437("d1")
& b48_buttercup10519("d0")
& ~ b48_buttercup10518("d1")
& k04_buttercup10437("d0")
& ~ b48_buttercup10519("d3")
& ~ b48_buttercup10518("d2")
& ~ k04_buttercup10437("d3")
& ~ b48_buttercup10519("d2")
& ~ b48_buttercup10518("d3")
& ~ k04_buttercup10437("d2")
& ~ b48_buttercup10515("d1")
& ~ k04_buttercup10430("d2")
& b48_buttercup10515("d0")
& ~ k04_buttercup10430("d3")
& ~ b48_buttercup10515("d3")
& k04_buttercup10430("d0")
& ~ b48_buttercup10515("d2")
& ~ k04_buttercup10430("d1")
& k04_buttercup10449("d2")
& ~ k04_buttercup10449("d3")
& k04_buttercup10449("d0")
& ~ k04_buttercup10449("d1")
& ~ k04_buttercup10445("d2")
& ~ k04_buttercup10445("d3")
& k04_buttercup10445("d0")
& ~ k04_buttercup10445("d1")
& ~ b48_buttercup10549("d2")
& ~ b48_buttercup10548("d1")
& ~ b48_buttercup10549("d3")
& b48_buttercup10548("d0")
& b48_buttercup10549("d0")
& ~ b48_buttercup10548("d3")
& ~ b48_buttercup10549("d1")
& ~ b48_buttercup10548("d2")
& ~ b48_buttercup10545("d2")
& ~ b48_buttercup10545("d3")
& b48_buttercup10545("d0")
& ~ b48_buttercup10545("d1")
& ~ b48_buttercup10542("d3")
& ~ b48_buttercup10542("d2")
& ~ b48_buttercup10542("d1")
& b48_buttercup10542("d0")
& ~ k04_buttercup10453("d3")
& ~ k04_buttercup10453("d2")
& ~ k04_buttercup10453("d1")
& k04_buttercup10453("d0")
& ~ b48_buttercup10531("d3")
& ~ b48_buttercup10531("d2")
& ~ b48_buttercup10531("d1")
& b48_buttercup10531("d0")
& ~ k04_buttercup10464("d3")
& k04_buttercup10464("d2")
& ~ k04_buttercup10464("d1")
& k04_buttercup10464("d0")
& ~ k04_buttercup10462("d1")
& k04_buttercup10462("d0")
& ~ k04_buttercup10462("d3")
& ~ k04_buttercup10462("d2")
& ~ b48_buttercup10562("d1")
& b48_buttercup10561("d0")
& ~ b48_buttercup10563("d2")
& b48_buttercup10562("d0")
& ~ b48_buttercup10561("d1")
& ~ b48_buttercup10563("d3")
& ~ b48_buttercup10562("d3")
& ~ b48_buttercup10561("d2")
& b48_buttercup10563("d0")
& ~ b48_buttercup10562("d2")
& ~ b48_buttercup10561("d3")
& ~ b48_buttercup10563("d1")
& ~ k04_buttercup10477("d1")
& k04_buttercup10477("d0")
& ~ k04_buttercup10477("d3")
& ~ k04_buttercup10477("d2")
& ~ k04_buttercup10473("d1")
& ~ k04_buttercup10470("d2")
& k04_buttercup10473("d0")
& ~ k04_buttercup10470("d3")
& ~ k04_buttercup10473("d3")
& k04_buttercup10470("d0")
& ~ k04_buttercup10473("d2")
& ~ k04_buttercup10470("d1")
& ~ b48_buttercup10552("d2")
& ~ b48_buttercup10552("d3")
& b48_buttercup10552("d0")
& ~ b48_buttercup10552("d1")
& ~ k04_buttercup10486("d3")
& ~ b48_buttercup10109("d2")
& ~ b48_buttercup10108("d1")
& b48_buttercup10107("d0")
& ~ k04_buttercup10486("d2")
& ~ b48_buttercup10109("d3")
& b48_buttercup10108("d0")
& b48_buttercup10107("d1")
& ~ k04_buttercup10486("d1")
& b48_buttercup10109("d0")
& ~ b48_buttercup10108("d3")
& b48_buttercup10107("d2")
& k04_buttercup10486("d0")
& ~ b48_buttercup10109("d1")
& ~ b48_buttercup10108("d2")
& ~ b48_buttercup10107("d3")
& ~ b48_buttercup10589("d2")
& ~ k04_buttercup10482("d3")
& ~ b48_buttercup10104("d1")
& ~ b48_buttercup10589("d3")
& ~ k04_buttercup10482("d2")
& b48_buttercup10104("d0")
& b48_buttercup10589("d0")
& ~ k04_buttercup10482("d1")
& ~ b48_buttercup10104("d3")
& ~ b48_buttercup10589("d1")
& k04_buttercup10482("d0")
& ~ b48_buttercup10104("d2")
& ~ b48_buttercup10102("d3")
& ~ b48_buttercup10102("d2")
& ~ b48_buttercup10102("d1")
& b48_buttercup10102("d0")
& ~ b48_buttercup10582("d3")
& ~ b48_buttercup10582("d2")
& ~ b48_buttercup10582("d1")
& b48_buttercup10582("d0")
& ~ k04_buttercup10016("d2")
& ~ k04_buttercup10016("d3")
& k04_buttercup10016("d0")
& ~ k04_buttercup10016("d1")
& ~ k04_buttercup10499("d1")
& k04_buttercup10012("d2")
& k04_buttercup10499("d0")
& ~ k04_buttercup10012("d3")
& ~ k04_buttercup10499("d3")
& k04_buttercup10012("d0")
& ~ k04_buttercup10499("d2")
& k04_buttercup10012("d1")
& ~ b48_buttercup10579("d3")
& ~ k04_buttercup10495("d1")
& ~ k04_buttercup10492("d2")
& ~ b48_buttercup10579("d2")
& k04_buttercup10495("d0")
& ~ k04_buttercup10492("d3")
& ~ b48_buttercup10579("d1")
& ~ k04_buttercup10495("d3")
& k04_buttercup10492("d0")
& b48_buttercup10579("d0")
& ~ k04_buttercup10495("d2")
& ~ k04_buttercup10492("d1")
& ~ b48_buttercup10575("d3")
& b48_buttercup10572("d0")
& ~ b48_buttercup10574("d2")
& ~ b48_buttercup10575("d2")
& ~ b48_buttercup10572("d1")
& ~ b48_buttercup10574("d3")
& ~ b48_buttercup10575("d1")
& ~ b48_buttercup10572("d2")
& b48_buttercup10574("d0")
& b48_buttercup10575("d0")
& ~ b48_buttercup10572("d3")
& ~ b48_buttercup10574("d1")
& ~ b48_buttercup10570("d2")
& ~ b48_buttercup10570("d3")
& b48_buttercup10570("d0")
& ~ b48_buttercup10570("d1")
& ~ k04_buttercup10504("d2")
& k04_buttercup10506("d0")
& ~ k04_buttercup10504("d3")
& ~ k04_buttercup10506("d1")
& ~ k04_buttercup10506("d2")
& k04_buttercup10504("d0")
& ~ k04_buttercup10506("d3")
& ~ k04_buttercup10504("d1")
& ~ b48_buttercup10609("d3")
& ~ b48_buttercup10609("d2")
& ~ b48_buttercup10609("d1")
& b48_buttercup10609("d0")
& ~ b48_buttercup10605("d3")
& ~ b48_buttercup10604("d2")
& ~ b48_buttercup10605("d2")
& ~ b48_buttercup10604("d3")
& ~ b48_buttercup10605("d1")
& b48_buttercup10604("d0")
& b48_buttercup10605("d0")
& ~ b48_buttercup10604("d1")
& ~ k04_buttercup10516("d3")
& k04_buttercup10517("d0")
& ~ k04_buttercup10516("d2")
& k04_buttercup10517("d1")
& ~ k04_buttercup10517("d2")
& k04_buttercup10516("d1")
& ~ k04_buttercup10517("d3")
& k04_buttercup10516("d0")
& ~ k04_buttercup10510("d1")
& k04_buttercup10510("d0")
& ~ k04_buttercup10510("d3")
& ~ k04_buttercup10510("d2")
& ~ k04_buttercup10529("d1")
& k04_buttercup10529("d0")
& ~ k04_buttercup10529("d3")
& ~ k04_buttercup10529("d2")
& ~ b48_buttercup10629("d1")
& k04_buttercup10524("d0")
& b48_buttercup10629("d0")
& ~ k04_buttercup10524("d1")
& ~ b48_buttercup10629("d3")
& ~ k04_buttercup10524("d2")
& ~ b48_buttercup10629("d2")
& ~ k04_buttercup10524("d3")
& b48_buttercup10624("d0")
& ~ b48_buttercup10624("d1")
& ~ b48_buttercup10624("d2")
& ~ b48_buttercup10624("d3")
& k04_buttercup10535("d0")
& ~ k04_buttercup10535("d1")
& ~ k04_buttercup10535("d2")
& ~ k04_buttercup10535("d3")
& ~ b48_buttercup10616("d3")
& ~ b48_buttercup10616("d2")
& ~ b48_buttercup10616("d1")
& b48_buttercup10616("d0")
& ~ b48_buttercup10199("d1")
& b48_buttercup10199("d0")
& ~ b48_buttercup10199("d3")
& ~ b48_buttercup10199("d2")
& ~ b48_buttercup10195("d1")
& b48_buttercup10195("d0")
& ~ b48_buttercup10195("d3")
& ~ b48_buttercup10195("d2")
& ~ b48_buttercup10193("d3")
& ~ b48_buttercup10191("d1")
& ~ b48_buttercup10193("d2")
& b48_buttercup10191("d0")
& ~ b48_buttercup10193("d1")
& ~ b48_buttercup10191("d3")
& b48_buttercup10193("d0")
& ~ b48_buttercup10191("d2") ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO581+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.04 % Command : run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n007.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 03:04:53 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_fmb4j /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.41 Running: java -jar /export/starexec/sandbox2/solver/bin/FMB4J.jar /export/starexec/sandbox2/tmp/tmp.HyngenSdYj/theBenchmark.cnf 300
% 0.62/0.76 % domain size: 1
% 1.07/0.88 % domain size: 2
% 1.41/0.91 % domain size: 3
% 1.41/0.96 % domain size: 4
% 1.92/1.05 % model found for domain size 4
% 1.92/1.06 % SZS status CounterSatisfiable for theBenchmark
% 1.92/1.07 % SZS output start FiniteModel for theBenchmark
% See solution above
% 2.74/1.24 % FMB4L exiting
%------------------------------------------------------------------------------