%------------------------------------------------------------------------------
% File : FMB4J---0.1
% Problem : SYN464+1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n015.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:37:50 PM UTC 2026
% Result : CounterSatisfiable 1.23s 1.00s
% Output : FiniteModel 1.80s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(domain,interpretation-domains,
! [X] :
( X = "d2"
| X = "d1"
| X = "d0" ) ).
fof(mappings,interpretation-mappings,
( a2503 = "d2"
& a2501 = "d1"
& a2502 = "d0"
& a2509 = "d2"
& a2505 = "d2"
& a2506 = "d0"
& a2428 = "d1"
& a2429 = "d0"
& a2511 = "d0"
& a2514 = "d0"
& a2513 = "d1"
& a2510 = "d0"
& a2515 = "d0"
& a2468 = "d0"
& a2469 = "d0"
& a2464 = "d1"
& a2466 = "d0"
& a2463 = "d2"
& a2471 = "d0"
& a2472 = "d2"
& a2473 = "d1"
& a2457 = "d1"
& a2456 = "d0"
& a2458 = "d2"
& a2459 = "d0"
& a2455 = "d2"
& a2453 = "d1"
& a2454 = "d1"
& a2452 = "d2"
& a2461 = "d1"
& a2460 = "d2"
& a2462 = "d1"
& a2446 = "d0"
& a2445 = "d1"
& a2447 = "d0"
& a2448 = "d1"
& a2442 = "d0"
& a2441 = "d1"
& a2444 = "d0"
& a2443 = "d0"
& a2451 = "d1"
& a2435 = "d0"
& a2434 = "d0"
& a2437 = "d0"
& a2436 = "d0"
& a2433 = "d2"
& a2432 = "d2"
& a2431 = "d1"
& a2430 = "d2"
& a2439 = "d0"
& a2438 = "d2"
& a2440 = "d0"
& a2498 = "d2"
& a2499 = "d0"
& a2497 = "d2"
& a2489 = "d1"
& a2485 = "d1"
& a2487 = "d2"
& a2486 = "d1"
& a2493 = "d1"
& a2492 = "d0"
& a2494 = "d1"
& a2495 = "d0"
& a2491 = "d0"
& a2478 = "d0"
& a2479 = "d2"
& a2475 = "d0"
& a2476 = "d2"
& a2482 = "d0"
& a2483 = "d0" ) ).
fof(predicate_mappings,interpretation-mappings,
( hskp9
& hskp8
& hskp7
& ~ hskp6
& ~ hskp5
& ~ hskp4
& ~ hskp3
& ~ hskp2
& hskp1
& hskp0
& ~ hskp53
& ~ hskp54
& ~ hskp51
& hskp52
& hskp50
& hskp59
& ~ hskp57
& ~ hskp58
& ~ hskp55
& ~ hskp56
& ~ hskp64
& ~ hskp65
& ~ hskp62
& ~ hskp63
& hskp60
& ~ hskp61
& ~ c3_1("d2")
& c3_1("d1")
& ~ c3_1("d0")
& ~ hskp68
& hskp69
& ~ hskp66
& ~ hskp67
& ~ hskp31
& ~ hskp32
& hskp30
& hskp39
& hskp37
& ~ hskp38
& ~ hskp35
& ~ hskp36
& ~ hskp33
& ~ hskp34
& ~ hskp42
& ~ hskp43
& ~ hskp40
& ~ hskp41
& ~ hskp48
& ~ hskp49
& ~ hskp46
& ndr1_0
& ~ hskp47
& ~ hskp44
& ~ hskp45
& ~ hskp10
& ~ hskp19
& hskp17
& ~ hskp18
& ~ hskp15
& hskp16
& ~ hskp13
& hskp14
& ~ hskp11
& ~ hskp12
& hskp20
& hskp21
& ~ c1_1("d1")
& ~ c1_1("d0")
& ~ c1_1("d2")
& ~ hskp28
& ~ hskp29
& ~ hskp26
& hskp27
& hskp24
& ~ hskp25
& ~ hskp22
& hskp23
& ~ c2_1("d0")
& c2_1("d1")
& c2_1("d2")
& c0_1("d2")
& ~ c0_1("d0")
& ~ c0_1("d1") ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN464+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.04 % Command : run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n015.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 01:22:41 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_fmb4j /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.44 Running: java -jar /export/starexec/sandbox/solver/bin/FMB4J.jar /export/starexec/sandbox/tmp/tmp.SZzeHsmHTg/theBenchmark.cnf 300
% 0.59/0.77 % domain size: 1
% 0.93/0.87 % domain size: 2
% 1.23/0.92 % domain size: 3
% 1.23/0.99 % model found for domain size 3
% 1.23/1.00 % SZS status CounterSatisfiable for theBenchmark
% 1.23/1.00 % SZS output start FiniteModel for theBenchmark
% See solution above
% 1.80/1.07 % FMB4L exiting
%------------------------------------------------------------------------------