↑ Up

FMB4J---0.1.SAT-FMo.s

View TPTP
Problem
Process solution in
SystemOnTSTP
Download .tgz
%------------------------------------------------------------------------------
% File     : FMB4J---0.1
% Problem  : NLP151-1 : TPTP v9.3.1. Released v2.4.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 02:15:43 PM UTC 2026

% Result   : Satisfiable 5.58s 7.53s
% Output   : FiniteModel 6.04s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)

% Comments : 
%------------------------------------------------------------------------------
fof(domain,interpretation-domains,
    ! [X] :
      ( X = "d2"
      | X = "d1"
      | X = "d0" ) ).

fof(mappings,interpretation-mappings,
    ( skf12("d2","d0") = "d0"
    & skf10("d2","d2") = "d0"
    & skf10("d1","d1") = "d0"
    & skf12("d0","d2") = "d0"
    & skf10("d0","d0") = "d0"
    & skf12("d1","d2") = "d0"
    & skf12("d2","d1") = "d0"
    & skf10("d1","d0") = "d0"
    & skf10("d0","d1") = "d0"
    & skf12("d0","d0") = "d0"
    & skf12("d2","d2") = "d0"
    & skf10("d0","d2") = "d0"
    & skf12("d1","d1") = "d0"
    & skf10("d2","d0") = "d0"
    & skf12("d0","d1") = "d0"
    & skf12("d1","d0") = "d0"
    & skf10("d1","d2") = "d0"
    & skf10("d2","d1") = "d0"
    & skf13("d2","d1","d0","d2") = "d0"
    & skf13("d0","d1","d2","d0") = "d2"
    & skf13("d0","d1","d0","d2") = "d2"
    & skf13("d0","d2","d0","d2") = "d1"
    & skf13("d1","d1","d0","d1") = "d0"
    & skf13("d1","d0","d0","d2") = "d2"
    & skf13("d2","d0","d2","d0") = "d1"
    & skf13("d0","d0","d1","d1") = "d1"
    & skf13("d1","d1","d1","d0") = "d0"
    & skf13("d2","d1","d2","d0") = "d0"
    & skf13("d1","d2","d0","d2") = "d0"
    & skf13("d2","d2","d1","d0") = "d0"
    & skf13("d1","d0","d2","d0") = "d2"
    & skf13("d2","d0","d0","d2") = "d1"
    & skf13("d2","d2","d0","d1") = "d0"
    & skf13("d1","d2","d2","d0") = "d0"
    & skf13("d0","d0","d2","d2") = "d1"
    & skf13("d0","d2","d2","d0") = "d1"
    & skf13("d0","d0","d0","d0") = "d1"
    & skf13("d2","d0","d2","d1") = "d1"
    & skf13("d2","d1","d1","d2") = "d0"
    & skf13("d1","d1","d2","d2") = "d0"
    & skf13("d0","d2","d2","d1") = "d1"
    & skf13("d0","d0","d1","d0") = "d1"
    & skf13("d0","d0","d0","d1") = "d1"
    & skf13("d0","d2","d1","d2") = "d1"
    & skf13("d1","d0","d2","d1") = "d2"
    & skf13("d0","d1","d2","d1") = "d2"
    & skf13("d2","d1","d2","d1") = "d0"
    & skf13("d1","d1","d1","d1") = "d0"
    & skf13("d2","d2","d2","d2") = "d0"
    & skf13("d2","d2","d0","d0") = "d0"
    & skf13("d2","d0","d1","d2") = "d1"
    & skf13("d1","d0","d1","d2") = "d2"
    & skf13("d1","d2","d2","d1") = "d0"
    & skf13("d2","d2","d1","d1") = "d0"
    & skf13("d1","d2","d1","d2") = "d0"
    & skf13("d0","d1","d1","d2") = "d2"
    & skf13("d1","d1","d0","d0") = "d0"
    & skf13("d0","d1","d2","d2") = "d2"
    & skf13("d1","d0","d1","d1") = "d2"
    & skf13("d1","d1","d2","d1") = "d0"
    & skf13("d2","d0","d1","d1") = "d1"
    & skf13("d0","d2","d0","d0") = "d1"
    & skf13("d1","d2","d0","d0") = "d0"
    & skf13("d1","d2","d1","d1") = "d0"
    & skf13("d0","d0","d2","d0") = "d1"
    & skf13("d2","d2","d2","d1") = "d0"
    & skf13("d2","d1","d2","d2") = "d0"
    & skf13("d2","d0","d2","d2") = "d1"
    & skf13("d1","d0","d2","d2") = "d2"
    & skf13("d0","d1","d1","d1") = "d2"
    & skf13("d2","d1","d1","d1") = "d0"
    & skf13("d0","d2","d1","d1") = "d1"
    & skf13("d0","d0","d0","d2") = "d1"
    & skf13("d0","d1","d0","d0") = "d2"
    & skf13("d2","d1","d0","d0") = "d0"
    & skf13("d0","d2","d2","d2") = "d1"
    & skf13("d1","d1","d1","d2") = "d0"
    & skf13("d1","d2","d2","d2") = "d0"
    & skf13("d2","d2","d1","d2") = "d0"
    & skf13("d1","d0","d0","d0") = "d2"
    & skf13("d2","d0","d0","d0") = "d1"
    & skf13("d0","d2","d1","d0") = "d1"
    & skf13("d1","d1","d2","d0") = "d0"
    & skf13("d1","d2","d1","d0") = "d0"
    & skf13("d2","d1","d0","d1") = "d0"
    & skf13("d0","d0","d1","d2") = "d1"
    & skf13("d1","d2","d0","d1") = "d0"
    & skf13("d1","d0","d0","d1") = "d2"
    & skf13("d1","d0","d1","d0") = "d2"
    & skf13("d2","d2","d0","d2") = "d0"
    & skf13("d2","d0","d1","d0") = "d1"
    & skf13("d0","d1","d0","d1") = "d2"
    & skf13("d2","d0","d0","d1") = "d1"
    & skf13("d2","d2","d2","d0") = "d0"
    & skf13("d0","d0","d2","d1") = "d1"
    & skf13("d0","d2","d0","d1") = "d1"
    & skf13("d1","d1","d0","d2") = "d0"
    & skf13("d2","d1","d1","d0") = "d0"
    & skf13("d0","d1","d1","d0") = "d2"
    & skc8 = "d2"
    & skc9 = "d1"
    & skc7 = "d1"
    & skc6 = "d0"
    & skc5 = "d2"
    & skf8("d2","d2") = "d0"
    & skf8("d1","d1") = "d0"
    & skf8("d0","d0") = "d0"
    & skf8("d1","d0") = "d0"
    & skf8("d0","d1") = "d0"
    & skf8("d0","d2") = "d0"
    & skf8("d2","d0") = "d0"
    & skf8("d1","d2") = "d0"
    & skf8("d2","d1") = "d0"
    & skf5("d0","d1") = "d0"
    & skf5("d1","d0") = "d0"
    & skf5("d2","d2") = "d0"
    & skf5("d0","d0") = "d0"
    & skf5("d1","d1") = "d0"
    & skf5("d1","d2") = "d0"
    & skf5("d2","d1") = "d0"
    & skf5("d0","d2") = "d0"
    & skf5("d2","d0") = "d0" ) ).

fof(predicate_mappings,interpretation-mappings,
    ( ~ artifact("d2","d2")
    & artifact("d1","d1")
    & ~ artifact("d0","d0")
    & ~ artifact("d0","d1")
    & ~ artifact("d1","d0")
    & ~ artifact("d0","d2")
    & ~ artifact("d2","d0")
    & ~ artifact("d1","d2")
    & artifact("d2","d1")
    & ~ lonely("d2","d2")
    & ~ lonely("d1","d1")
    & lonely("d0","d0")
    & ~ lonely("d0","d1")
    & lonely("d1","d0")
    & ~ lonely("d0","d2")
    & lonely("d2","d0")
    & ~ lonely("d1","d2")
    & lonely("d2","d1")
    & ~ barrel("d0","d1")
    & barrel("d1","d0")
    & ~ barrel("d2","d2")
    & ~ barrel("d1","d1")
    & barrel("d0","d0")
    & ~ barrel("d1","d2")
    & ~ barrel("d2","d1")
    & ~ barrel("d0","d2")
    & barrel("d2","d0")
    & ~ vehicle("d1","d2")
    & vehicle("d2","d1")
    & ~ vehicle("d0","d2")
    & ~ vehicle("d2","d0")
    & ~ vehicle("d0","d1")
    & ~ vehicle("d1","d0")
    & ~ vehicle("d2","d2")
    & vehicle("d1","d1")
    & ~ vehicle("d0","d0")
    & ~ group("d1","d2")
    & ~ group("d2","d1")
    & ~ group("d0","d2")
    & ~ group("d2","d0")
    & ~ group("d0","d1")
    & ~ group("d1","d0")
    & ~ group("d2","d2")
    & ~ group("d1","d1")
    & ~ group("d0","d0")
    & ~ general("d0","d1")
    & ~ general("d1","d0")
    & general("d2","d2")
    & ~ general("d1","d1")
    & ~ general("d0","d0")
    & ~ general("d1","d2")
    & ~ general("d2","d1")
    & ~ general("d0","d2")
    & ~ general("d2","d0")
    & ~ thing("d0","d1")
    & thing("d1","d0")
    & thing("d2","d2")
    & thing("d1","d1")
    & thing("d0","d0")
    & ~ thing("d1","d2")
    & thing("d2","d1")
    & ~ thing("d0","d2")
    & thing("d2","d0")
    & ~ two("d0","d1")
    & ~ two("d1","d0")
    & ~ two("d2","d2")
    & ~ two("d1","d1")
    & ~ two("d0","d0")
    & ~ two("d1","d2")
    & ~ two("d2","d1")
    & ~ two("d0","d2")
    & ~ two("d2","d0")
    & ~ white("d2","d2")
    & ~ white("d1","d1")
    & white("d0","d0")
    & ~ white("d0","d1")
    & white("d1","d0")
    & ~ white("d0","d2")
    & white("d2","d0")
    & ~ white("d1","d2")
    & white("d2","d1")
    & ~ way("d0","d2")
    & ~ way("d2","d0")
    & ~ way("d1","d2")
    & way("d2","d1")
    & ~ way("d2","d2")
    & ~ way("d1","d1")
    & ~ way("d0","d0")
    & ~ way("d0","d1")
    & ~ way("d1","d0")
    & ~ street("d0","d2")
    & ~ street("d2","d0")
    & ~ street("d1","d2")
    & street("d2","d1")
    & ~ street("d2","d2")
    & ~ street("d1","d1")
    & ~ street("d0","d0")
    & ~ street("d0","d1")
    & ~ street("d1","d0")
    & chevy("d1","d1")
    & ~ chevy("d2","d2")
    & ~ chevy("d0","d0")
    & ~ chevy("d0","d1")
    & ~ chevy("d1","d0")
    & ~ chevy("d0","d2")
    & ~ chevy("d2","d0")
    & ~ chevy("d1","d2")
    & chevy("d2","d1")
    & ~ placename("d1","d1")
    & placename("d2","d2")
    & ~ placename("d0","d0")
    & ~ agent("d2","d2","d2")
    & ~ agent("d0","d0","d2")
    & ~ agent("d1","d2","d1")
    & ~ agent("d2","d1","d1")
    & ~ agent("d0","d2","d0")
    & ~ agent("d2","d0","d0")
    & ~ agent("d1","d1","d2")
    & ~ placename("d0","d1")
    & ~ placename("d1","d0")
    & ~ agent("d0","d1","d2")
    & ~ agent("d1","d0","d2")
    & ~ agent("d0","d2","d1")
    & agent("d2","d0","d1")
    & ~ agent("d1","d2","d0")
    & ~ agent("d2","d1","d0")
    & ~ placename("d0","d2")
    & ~ placename("d2","d0")
    & ~ agent("d0","d2","d2")
    & ~ agent("d2","d0","d2")
    & ~ agent("d0","d1","d1")
    & ~ agent("d1","d0","d1")
    & ~ agent("d1","d1","d0")
    & agent("d0","d0","d0")
    & ~ agent("d2","d2","d0")
    & ~ placename("d1","d2")
    & ~ placename("d2","d1")
    & ~ agent("d1","d2","d2")
    & ~ agent("d2","d1","d2")
    & ~ agent("d2","d2","d1")
    & ~ agent("d1","d1","d1")
    & ~ agent("d0","d0","d1")
    & ~ agent("d0","d1","d0")
    & ~ agent("d1","d0","d0")
    & ~ member("d0","d2","d2")
    & ~ member("d2","d0","d2")
    & ~ member("d0","d1","d1")
    & ~ member("d1","d0","d1")
    & ~ member("d2","d2","d0")
    & ~ member("d1","d1","d0")
    & ~ member("d0","d0","d0")
    & ~ member("d1","d2","d2")
    & ~ member("d2","d1","d2")
    & ~ member("d2","d2","d1")
    & ~ member("d1","d1","d1")
    & ~ member("d0","d0","d1")
    & ~ member("d0","d1","d0")
    & ~ member("d1","d0","d0")
    & ~ member("d2","d2","d2")
    & ~ member("d1","d1","d2")
    & ~ member("d0","d0","d2")
    & ~ member("d1","d2","d1")
    & ~ member("d2","d1","d1")
    & ~ member("d0","d2","d0")
    & ~ member("d2","d0","d0")
    & ~ member("d0","d1","d2")
    & ~ member("d1","d0","d2")
    & ~ member("d0","d2","d1")
    & ~ member("d2","d0","d1")
    & ~ member("d1","d2","d0")
    & ~ member("d2","d1","d0")
    & ~ entity("d0","d2")
    & ~ entity("d2","d0")
    & ~ entity("d1","d2")
    & entity("d2","d1")
    & ~ entity("d2","d2")
    & entity("d1","d1")
    & ~ entity("d0","d0")
    & ~ entity("d0","d1")
    & ~ entity("d1","d0")
    & ~ in("d1","d2","d2")
    & ~ in("d2","d1","d2")
    & ~ in("d2","d2","d1")
    & ~ in("d1","d1","d1")
    & ~ in("d0","d0","d1")
    & ~ in("d0","d1","d0")
    & in("d1","d0","d0")
    & ~ in("d0","d2","d2")
    & ~ in("d2","d0","d2")
    & ~ in("d0","d1","d1")
    & ~ in("d1","d0","d1")
    & ~ in("d2","d2","d0")
    & ~ in("d1","d1","d0")
    & in("d0","d0","d0")
    & ~ in("d0","d1","d2")
    & ~ in("d1","d0","d2")
    & ~ in("d0","d2","d1")
    & in("d2","d0","d1")
    & ~ in("d1","d2","d0")
    & ~ in("d2","d1","d0")
    & ~ in("d2","d2","d2")
    & ~ in("d1","d1","d2")
    & ~ in("d0","d0","d2")
    & ~ in("d1","d2","d1")
    & ~ in("d2","d1","d1")
    & ~ in("d0","d2","d0")
    & ~ in("d2","d0","d0")
    & ~ city("d0","d1")
    & ~ city("d1","d0")
    & ~ city("d2","d2")
    & ~ city("d1","d1")
    & ~ city("d0","d0")
    & ~ city("d1","d2")
    & city("d2","d1")
    & ~ city("d0","d2")
    & ~ city("d2","d0")
    & ~ of("d0","d1","d2")
    & ~ of("d0","d2","d1")
    & ~ of("d2","d0","d1")
    & ~ of("d1","d2","d0")
    & ~ of("d2","d1","d0")
    & ~ of("d1","d0","d2")
    & ~ of("d2","d2","d2")
    & ~ of("d1","d1","d2")
    & ~ of("d0","d0","d2")
    & ~ of("d2","d1","d1")
    & ~ of("d0","d2","d0")
    & of("d2","d0","d0")
    & ~ of("d1","d2","d1")
    & ~ of("d1","d2","d2")
    & ~ of("d2","d1","d2")
    & of("d2","d2","d1")
    & ~ of("d1","d1","d1")
    & of("d1","d0","d0")
    & ~ of("d0","d0","d1")
    & ~ of("d0","d1","d0")
    & ~ of("d0","d2","d2")
    & ~ of("d2","d0","d2")
    & ~ of("d0","d1","d1")
    & ~ of("d1","d0","d1")
    & ~ of("d1","d1","d0")
    & of("d0","d0","d0")
    & ~ of("d2","d2","d0")
    & ~ abstraction("d1","d2")
    & ~ abstraction("d2","d1")
    & ~ abstraction("d0","d2")
    & ~ abstraction("d2","d0")
    & ~ abstraction("d1","d0")
    & ~ abstraction("d0","d1")
    & abstraction("d2","d2")
    & ~ abstraction("d0","d0")
    & ~ abstraction("d1","d1")
    & ~ transport("d1","d2")
    & transport("d2","d1")
    & ~ transport("d0","d2")
    & ~ transport("d2","d0")
    & ~ transport("d0","d1")
    & ~ transport("d1","d0")
    & ~ transport("d2","d2")
    & transport("d1","d1")
    & ~ transport("d0","d0")
    & ~ specific("d2","d2")
    & specific("d1","d1")
    & specific("d0","d0")
    & ~ specific("d0","d1")
    & specific("d1","d0")
    & ~ specific("d0","d2")
    & specific("d2","d0")
    & ~ specific("d1","d2")
    & specific("d2","d1")
    & ~ object("d1","d2")
    & object("d2","d1")
    & ~ object("d0","d2")
    & ~ object("d2","d0")
    & ~ object("d0","d1")
    & ~ object("d1","d0")
    & ~ object("d2","d2")
    & object("d1","d1")
    & ~ object("d0","d0")
    & actual_world("d2")
    & actual_world("d0")
    & actual_world("d1")
    & ~ nonexistent("d1","d2")
    & ~ nonexistent("d2","d1")
    & ~ nonexistent("d0","d2")
    & nonexistent("d2","d0")
    & ~ nonexistent("d0","d1")
    & nonexistent("d1","d0")
    & ~ nonexistent("d2","d2")
    & ~ nonexistent("d1","d1")
    & nonexistent("d0","d0")
    & ~ multiple("d2","d2")
    & ~ multiple("d1","d1")
    & ~ multiple("d0","d0")
    & ~ multiple("d0","d1")
    & ~ multiple("d1","d0")
    & ~ multiple("d0","d2")
    & ~ multiple("d2","d0")
    & ~ multiple("d1","d2")
    & ~ multiple("d2","d1")
    & ~ down("d1","d2","d2")
    & ~ down("d2","d1","d2")
    & ~ down("d2","d2","d1")
    & ~ down("d0","d0","d1")
    & ~ down("d0","d1","d0")
    & ~ down("d1","d1","d1")
    & down("d1","d0","d0")
    & ~ down("d0","d2","d2")
    & ~ down("d2","d0","d2")
    & ~ down("d0","d1","d1")
    & ~ down("d2","d2","d0")
    & ~ down("d1","d1","d0")
    & ~ down("d1","d0","d1")
    & down("d0","d0","d0")
    & ~ down("d0","d1","d2")
    & ~ down("d1","d0","d2")
    & ~ down("d0","d2","d1")
    & down("d2","d0","d1")
    & ~ down("d1","d2","d0")
    & ~ down("d2","d1","d0")
    & ~ down("d2","d2","d2")
    & ~ down("d1","d1","d2")
    & ~ down("d0","d0","d2")
    & ~ down("d1","d2","d1")
    & ~ down("d2","d1","d1")
    & down("d2","d0","d0")
    & ~ down("d0","d2","d0")
    & ~ eventuality("d0","d1")
    & eventuality("d1","d0")
    & ~ eventuality("d2","d2")
    & ~ eventuality("d1","d1")
    & eventuality("d0","d0")
    & ~ eventuality("d1","d2")
    & ~ eventuality("d2","d1")
    & ~ eventuality("d0","d2")
    & eventuality("d2","d0")
    & ~ relation("d1","d2")
    & ~ relation("d2","d1")
    & ~ relation("d0","d2")
    & ~ relation("d2","d0")
    & ~ relation("d0","d1")
    & ~ relation("d1","d0")
    & relation("d2","d2")
    & ~ relation("d1","d1")
    & ~ relation("d0","d0")
    & ~ event("d2","d2")
    & ~ event("d1","d1")
    & event("d0","d0")
    & ~ event("d0","d1")
    & event("d1","d0")
    & ~ event("d0","d2")
    & event("d2","d0")
    & ~ event("d1","d2")
    & ~ event("d2","d1")
    & ~ relname("d0","d1")
    & ~ relname("d1","d0")
    & relname("d2","d2")
    & ~ relname("d1","d1")
    & ~ relname("d0","d0")
    & ~ relname("d1","d2")
    & ~ relname("d2","d1")
    & ~ relname("d0","d2")
    & ~ relname("d2","d0")
    & ~ existent("d0","d2")
    & ~ existent("d2","d0")
    & ~ existent("d1","d2")
    & existent("d2","d1")
    & ~ existent("d2","d2")
    & existent("d1","d1")
    & ~ existent("d0","d0")
    & ~ existent("d0","d1")
    & ~ existent("d1","d0")
    & ~ car("d0","d1")
    & ~ car("d1","d0")
    & ~ car("d2","d2")
    & car("d1","d1")
    & ~ car("d0","d0")
    & ~ car("d1","d2")
    & car("d2","d1")
    & ~ car("d0","d2")
    & ~ car("d2","d0")
    & ~ old("d0","d2")
    & ~ old("d2","d0")
    & ~ old("d1","d2")
    & old("d2","d1")
    & ~ old("d2","d2")
    & ~ old("d1","d1")
    & old("d0","d0")
    & ~ old("d0","d1")
    & ~ old("d1","d0")
    & ssSkP0("d0","d1")
    & ssSkP0("d1","d0")
    & ssSkP0("d2","d2")
    & ssSkP0("d1","d1")
    & ssSkP0("d0","d0")
    & ssSkP0("d1","d2")
    & ssSkP0("d2","d1")
    & ssSkP0("d0","d2")
    & ssSkP0("d2","d0")
    & ~ dirty("d2","d2")
    & ~ dirty("d1","d1")
    & dirty("d0","d0")
    & ~ dirty("d0","d1")
    & dirty("d1","d0")
    & ~ dirty("d0","d2")
    & dirty("d2","d0")
    & ~ dirty("d1","d2")
    & dirty("d2","d1")
    & ~ location("d0","d2")
    & ~ location("d2","d0")
    & ~ location("d1","d2")
    & location("d2","d1")
    & ~ location("d2","d2")
    & ~ location("d1","d1")
    & ~ location("d0","d0")
    & ~ location("d0","d1")
    & ~ location("d1","d0")
    & singleton("d2","d2")
    & singleton("d1","d1")
    & singleton("d0","d0")
    & ~ singleton("d0","d1")
    & singleton("d1","d0")
    & ~ singleton("d0","d2")
    & singleton("d2","d0")
    & ~ singleton("d1","d2")
    & singleton("d2","d1")
    & ~ hollywood_placename("d1","d2")
    & ~ hollywood_placename("d2","d1")
    & ~ hollywood_placename("d0","d2")
    & ~ hollywood_placename("d2","d0")
    & ~ hollywood_placename("d0","d1")
    & ~ hollywood_placename("d1","d0")
    & hollywood_placename("d2","d2")
    & ~ hollywood_placename("d1","d1")
    & ~ hollywood_placename("d0","d0")
    & ~ instrumentality("d0","d1")
    & ~ instrumentality("d1","d0")
    & ~ instrumentality("d2","d2")
    & instrumentality("d1","d1")
    & ~ instrumentality("d0","d0")
    & ~ instrumentality("d1","d2")
    & instrumentality("d2","d1")
    & ~ instrumentality("d0","d2")
    & ~ instrumentality("d2","d0")
    & ~ present("d2","d2")
    & ~ present("d1","d1")
    & present("d0","d0")
    & ~ present("d0","d1")
    & present("d1","d0")
    & ~ present("d0","d2")
    & present("d2","d0")
    & ~ present("d1","d2")
    & ~ present("d2","d1")
    & ~ set("d1","d2")
    & ~ set("d2","d1")
    & ~ set("d0","d2")
    & ~ set("d2","d0")
    & ~ set("d0","d1")
    & ~ set("d1","d0")
    & ~ set("d2","d2")
    & ~ set("d1","d1")
    & ~ set("d0","d0") ) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : NLP151-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04  % Command  : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/5.38  % Computer : n008.cluster.edu
% 0.10/5.38  % Model    : x86_64 x86_64
% 0.10/5.38  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38  % Memory   : 8046.5625MB
% 0.10/5.38  % OS       : Linux 6.8.0-71-generic
% 0.10/5.38  % CPULimit : 300
% 0.10/5.38  % WCLimit  : 300
% 0.10/5.38  % DateTime : Thu Sep 24 02:09:17 UTC 2026
% 0.10/5.39  % CPUTime  : 
% 0.10/5.39  Running run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.14/5.44  Running: java -jar /export/starexec/sandbox/solver/bin/FMB4J.jar /export/starexec/sandbox/tmp/tmp.vS47WAEXHX/theBenchmark.cnf 300
% 0.14/5.77  % domain size: 1
% 0.14/5.86  % domain size: 2
% 0.14/5.93  % domain size: 3
% 5.58/7.52  % model found for domain size 3
% 5.58/7.53  % SZS status CounterSatisfiable for theBenchmark
% 5.58/7.53  % SZS output start FiniteModel for theBenchmark
% See solution above
% 6.04/7.68  % FMB4L exiting
%------------------------------------------------------------------------------