%------------------------------------------------------------------------------
% File : FMB4J---0.1
% Problem : SYN903-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 : n008.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:37 PM UTC 2026
% Result : Satisfiable 1.13s 0.93s
% Output : FiniteModel 1.13s
% 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"
& 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"
& skf61("d1") = "d1"
& skf61("d0") = "d0"
& skf60("d1") = "d1"
& skf60("d0") = "d0"
& skf63("d1") = "d1"
& skf63("d0") = "d1"
& skf62("d1") = "d1"
& skf62("d0") = "d0"
& skf65("d1") = "d1"
& skf64("d0") = "d1"
& skf65("d0") = "d1"
& skf64("d1") = "d1"
& skf67("d1") = "d1"
& skf66("d0") = "d1"
& skf67("d0") = "d1"
& skf66("d1") = "d1"
& skf69("d1") = "d1"
& skf68("d0") = "d1"
& skf69("d0") = "d1"
& skf68("d1") = "d1"
& skf70("d1") = "d1"
& skf70("d0") = "d1"
& skf72("d1") = "d1"
& skf71("d0") = "d1"
& skf72("d0") = "d1"
& skf71("d1") = "d1"
& 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"
& skf44("d0") = "d1"
& skf45("d0") = "d1"
& skf45("d1") = "d0"
& skf44("d1") = "d1"
& skf47("d0") = "d0"
& skf46("d1") = "d0"
& skf47("d1") = "d0"
& skf46("d0") = "d0"
& skf49("d0") = "d0"
& skf48("d1") = "d0"
& skf49("d1") = "d0"
& skf48("d0") = "d0"
& skf50("d0") = "d0"
& skf50("d1") = "d0"
& skf52("d0") = "d0"
& skf51("d1") = "d0"
& skf52("d1") = "d0"
& skf51("d0") = "d0"
& skf53("d1") = "d0"
& skf54("d1") = "d1"
& skf54("d0") = "d0"
& skf53("d0") = "d0"
& skf56("d1") = "d1"
& skf56("d0") = "d0"
& skf55("d1") = "d1"
& skf55("d0") = "d0"
& skf58("d1") = "d1"
& skf58("d0") = "d0"
& skf57("d1") = "d1"
& skf57("d0") = "d0"
& skf59("d1") = "d1"
& skf59("d0") = "d0" ) ).
fof(predicate_mappings,interpretation-mappings,
( ssPv22("d1")
& ~ ssPv23("d0")
& ~ ssPv22("d0")
& ssPv23("d1")
& ~ ssPv21("d0")
& ssPv21("d1")
& ssPv15("d1")
& ~ ssPv16("d0")
& ~ ssPv15("d0")
& ssPv16("d1")
& ssPv13("d1")
& ~ ssPv13("d0")
& ~ ssPv6("d0")
& ssPv7("d1")
& ssPv6("d1")
& ~ ssPv7("d0")
& ssPv5("d1")
& ~ ssPv5("d0")
& ssSkP300("d1")
& ~ ssSkP300("d0")
& ~ ssSkP303("d0")
& ssSkP304("d1")
& ssSkP303("d1")
& ssSkP304("d0")
& ssSkP302("d1")
& ~ ssSkP301("d0")
& ~ ssSkP302("d0")
& ssSkP301("d1")
& ssSkP329("d0")
& ssSkP329("d1")
& ssSkP328("d1")
& ssSkP327("d0")
& ssSkP328("d0")
& ssSkP327("d1")
& ssSkP332("d0")
& ssSkP333("d1")
& ssSkP332("d1")
& ssSkP333("d0")
& ssSkP330("d0")
& ssSkP331("d1")
& ssSkP330("d1")
& ssSkP331("d0")
& ssSkP336("d0")
& ssSkP337("d1")
& ssSkP336("d1")
& ssSkP337("d0")
& ssSkP334("d0")
& ssSkP335("d1")
& ssSkP334("d1")
& ssSkP335("d0")
& ssSkP338("d0")
& ssSkP339("d1")
& ssSkP338("d1")
& ssSkP339("d0")
& ssSkP340("d1")
& ssSkP340("d0")
& ssSkP344("d1")
& ssSkP343("d0")
& ssSkP344("d0")
& ssSkP343("d1")
& ssSkP342("d1")
& ssSkP341("d0")
& ssSkP342("d0")
& ssSkP341("d1")
& ssSkP348("d1")
& ssSkP347("d0")
& ssSkP348("d0")
& ssSkP347("d1")
& ssSkP346("d1")
& ssSkP345("d0")
& ssSkP346("d0")
& ssSkP345("d1")
& ssSkP308("d1")
& ~ ssSkP307("d0")
& ~ ssSkP308("d0")
& ssSkP307("d1")
& ssSkP306("d1")
& ~ ssSkP305("d0")
& ~ ssSkP306("d0")
& ssSkP305("d1")
& ~ ssSkP309("d0")
& ssSkP309("d1")
& ~ ssSkP310("d0")
& ssSkP311("d1")
& ssSkP310("d1")
& ssSkP311("d0")
& ssSkP314("d0")
& ssSkP315("d1")
& ssSkP314("d1")
& ssSkP315("d0")
& ssSkP312("d0")
& ssSkP313("d1")
& ssSkP312("d1")
& ssSkP313("d0")
& ssSkP318("d0")
& ssSkP319("d1")
& ssSkP318("d1")
& ssSkP319("d0")
& ssSkP316("d0")
& ssSkP317("d1")
& ssSkP316("d1")
& ssSkP317("d0")
& ssSkP322("d1")
& ssSkP321("d0")
& ssSkP322("d0")
& ssSkP321("d1")
& ssSkP320("d1")
& ssSkP320("d0")
& ssSkP326("d1")
& ssSkP325("d0")
& ssSkP326("d0")
& ssSkP325("d1")
& ssSkP324("d1")
& ssSkP323("d0")
& ssSkP324("d0")
& ssSkP323("d1")
& ssSkP370("d0")
& ~ ssSkP370("d1")
& ~ ssSkC10
& ssSkP349("d0")
& ssSkP349("d1")
& ssSkP350("d0")
& ssSkP351("d1")
& ssSkP350("d1")
& ssSkP351("d0")
& ssSkP354("d0")
& ssSkP355("d1")
& ssSkP354("d1")
& ssSkP355("d0")
& ssSkP352("d0")
& ssSkP353("d1")
& ssSkP352("d1")
& ssSkP353("d0")
& ssSkP358("d0")
& ssSkP359("d1")
& ssSkP358("d1")
& ssSkP359("d0")
& ssSkP356("d0")
& ssSkP357("d1")
& ssSkP356("d1")
& ssSkP357("d0")
& ssSkP362("d1")
& ssSkP361("d0")
& ssSkP362("d0")
& ssSkP361("d1")
& 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")
& ssSkP367("d1")
& ssSkP368("d0")
& ssSkP292("d1")
& ~ ssSkP292("d0")
& ssSkP290("d1")
& ~ ssSkP290("d0")
& ssSkP296("d1")
& ~ ssSkP295("d0")
& ~ ssSkP296("d0")
& ssSkP295("d1")
& ~ ssSkP293("d0")
& ssSkP294("d1")
& ssSkP293("d1")
& ~ ssSkP294("d0")
& ~ ssSkP299("d0")
& ssSkP299("d1")
& ~ ssSkP297("d0")
& ssSkP298("d1")
& ssSkP297("d1")
& ~ ssSkP298("d0")
& ssSkP281("d1","d0")
& ssSkP281("d0","d1")
& ssSkP281("d1","d1")
& ssSkP281("d0","d0")
& ssSkP291("d1","d1")
& ssSkP291("d0","d0")
& ssSkP291("d0","d1")
& ssSkP291("d1","d0")
& ssSkP280("d0")
& ssSkP280("d1")
& ssSkP285("d1")
& ~ ssSkP284("d0")
& ~ ssSkP285("d0")
& ssSkP284("d1")
& ssSkP283("d1")
& ~ ssSkP282("d0")
& ~ ssSkP283("d0")
& ssSkP282("d1")
& ~ ssSkP288("d0")
& ssSkP289("d1")
& ssSkP288("d1")
& ~ ssSkP289("d0")
& ~ ssSkP286("d0")
& ssSkP287("d1")
& ssSkP286("d1")
& ~ ssSkP287("d0")
& ssRr("d1","d1")
& ~ ssRr("d0","d0")
& ssRr("d0","d1")
& ssRr("d1","d0") ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN903-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n008.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:54 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.44 Running: java -jar /export/starexec/sandbox/solver/bin/FMB4J.jar /export/starexec/sandbox/tmp/tmp.ddRfv7oOG7/theBenchmark.cnf 300
% 0.58/0.77 % domain size: 1
% 0.89/0.87 % domain size: 2
% 1.13/0.91 % model found for domain size 2
% 1.13/0.93 % SZS status CounterSatisfiable for theBenchmark
% 1.13/0.93 % SZS output start FiniteModel for theBenchmark
% See solution above
% 1.13/1.03 % FMB4L exiting
%------------------------------------------------------------------------------