%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN539-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n016.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 : Tue Sep 29 02:17:31 PM UTC 2026
% Result : Satisfiable 0.08s 0.24s
% Output : FiniteModel 0.08s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
tff('declare_$i1',type,
'fmb_$i_1': $i ).
tff('finite_domain_$i',axiom,
! [X: $i] : ( X = 'fmb_$i_1' ) ).
tff(declare_a637,type,
a637: $i ).
tff(a637_definition,axiom,
a637 = 'fmb_$i_1' ).
tff(declare_a587,type,
a587: $i ).
tff(a587_definition,axiom,
a587 = 'fmb_$i_1' ).
tff(declare_a624,type,
a624: $i ).
tff(a624_definition,axiom,
a624 = 'fmb_$i_1' ).
tff(declare_a608,type,
a608: $i ).
tff(a608_definition,axiom,
a608 = 'fmb_$i_1' ).
tff(declare_a593,type,
a593: $i ).
tff(a593_definition,axiom,
a593 = 'fmb_$i_1' ).
tff(declare_a638,type,
a638: $i ).
tff(a638_definition,axiom,
a638 = 'fmb_$i_1' ).
tff(declare_a631,type,
a631: $i ).
tff(a631_definition,axiom,
a631 = 'fmb_$i_1' ).
tff(declare_a594,type,
a594: $i ).
tff(a594_definition,axiom,
a594 = 'fmb_$i_1' ).
tff(declare_a634,type,
a634: $i ).
tff(a634_definition,axiom,
a634 = 'fmb_$i_1' ).
tff(declare_a626,type,
a626: $i ).
tff(a626_definition,axiom,
a626 = 'fmb_$i_1' ).
tff(declare_a625,type,
a625: $i ).
tff(a625_definition,axiom,
a625 = 'fmb_$i_1' ).
tff(declare_a621,type,
a621: $i ).
tff(a621_definition,axiom,
a621 = 'fmb_$i_1' ).
tff(declare_a609,type,
a609: $i ).
tff(a609_definition,axiom,
a609 = 'fmb_$i_1' ).
tff(declare_a603,type,
a603: $i ).
tff(a603_definition,axiom,
a603 = 'fmb_$i_1' ).
tff(declare_a602,type,
a602: $i ).
tff(a602_definition,axiom,
a602 = 'fmb_$i_1' ).
tff(declare_a599,type,
a599: $i ).
tff(a599_definition,axiom,
a599 = 'fmb_$i_1' ).
tff(declare_a592,type,
a592: $i ).
tff(a592_definition,axiom,
a592 = 'fmb_$i_1' ).
tff(declare_a633,type,
a633: $i ).
tff(a633_definition,axiom,
a633 = 'fmb_$i_1' ).
tff(declare_a629,type,
a629: $i ).
tff(a629_definition,axiom,
a629 = 'fmb_$i_1' ).
tff(declare_a619,type,
a619: $i ).
tff(a619_definition,axiom,
a619 = 'fmb_$i_1' ).
tff(declare_a616,type,
a616: $i ).
tff(a616_definition,axiom,
a616 = 'fmb_$i_1' ).
tff(declare_a611,type,
a611: $i ).
tff(a611_definition,axiom,
a611 = 'fmb_$i_1' ).
tff(declare_a630,type,
a630: $i ).
tff(a630_definition,axiom,
a630 = 'fmb_$i_1' ).
tff(declare_a620,type,
a620: $i ).
tff(a620_definition,axiom,
a620 = 'fmb_$i_1' ).
tff(declare_a615,type,
a615: $i ).
tff(a615_definition,axiom,
a615 = 'fmb_$i_1' ).
tff(declare_a612,type,
a612: $i ).
tff(a612_definition,axiom,
a612 = 'fmb_$i_1' ).
tff(declare_a600,type,
a600: $i ).
tff(a600_definition,axiom,
a600 = 'fmb_$i_1' ).
tff(declare_a639,type,
a639: $i ).
tff(a639_definition,axiom,
a639 = 'fmb_$i_1' ).
tff(declare_a613,type,
a613: $i ).
tff(a613_definition,axiom,
a613 = 'fmb_$i_1' ).
tff(declare_a601,type,
a601: $i ).
tff(a601_definition,axiom,
a601 = 'fmb_$i_1' ).
tff(declare_a622,type,
a622: $i ).
tff(a622_definition,axiom,
a622 = 'fmb_$i_1' ).
tff(declare_a614,type,
a614: $i ).
tff(a614_definition,axiom,
a614 = 'fmb_$i_1' ).
tff(declare_a618,type,
a618: $i ).
tff(a618_definition,axiom,
a618 = 'fmb_$i_1' ).
tff(declare_a588,type,
a588: $i ).
tff(a588_definition,axiom,
a588 = 'fmb_$i_1' ).
tff(declare_a591,type,
a591: $i ).
tff(a591_definition,axiom,
a591 = 'fmb_$i_1' ).
tff(declare_a590,type,
a590: $i ).
tff(a590_definition,axiom,
a590 = 'fmb_$i_1' ).
tff(declare_a589,type,
a589: $i ).
tff(a589_definition,axiom,
a589 = 'fmb_$i_1' ).
tff(declare_a596,type,
a596: $i ).
tff(a596_definition,axiom,
a596 = 'fmb_$i_1' ).
tff(declare_a598,type,
a598: $i ).
tff(a598_definition,axiom,
a598 = 'fmb_$i_1' ).
tff(declare_a597,type,
a597: $i ).
tff(a597_definition,axiom,
a597 = 'fmb_$i_1' ).
tff(declare_a635,type,
a635: $i ).
tff(a635_definition,axiom,
a635 = 'fmb_$i_1' ).
tff(declare_a595,type,
a595: $i ).
tff(a595_definition,axiom,
a595 = 'fmb_$i_1' ).
tff(declare_a632,type,
a632: $i ).
tff(a632_definition,axiom,
a632 = 'fmb_$i_1' ).
tff(declare_a628,type,
a628: $i ).
tff(a628_definition,axiom,
a628 = 'fmb_$i_1' ).
tff(declare_a617,type,
a617: $i ).
tff(a617_definition,axiom,
a617 = 'fmb_$i_1' ).
tff(declare_a610,type,
a610: $i ).
tff(a610_definition,axiom,
a610 = 'fmb_$i_1' ).
tff(declare_a627,type,
a627: $i ).
tff(a627_definition,axiom,
a627 = 'fmb_$i_1' ).
tff(declare_a604,type,
a604: $i ).
tff(a604_definition,axiom,
a604 = 'fmb_$i_1' ).
tff(declare_a636,type,
a636: $i ).
tff(a636_definition,axiom,
a636 = 'fmb_$i_1' ).
tff(declare_a605,type,
a605: $i ).
tff(a605_definition,axiom,
a605 = 'fmb_$i_1' ).
tff(declare_a623,type,
a623: $i ).
tff(a623_definition,axiom,
a623 = 'fmb_$i_1' ).
tff(declare_c5_0,type,
c5_0: $o ).
tff(c5_0_definition,axiom,
c5_0 ).
tff(declare_ndr1_0,type,
ndr1_0: $o ).
tff(ndr1_0_definition,axiom,
ndr1_0 ).
tff(declare_c3_0,type,
c3_0: $o ).
tff(c3_0_definition,axiom,
c3_0 ).
tff(declare_c4_0,type,
c4_0: $o ).
tff(c4_0_definition,axiom,
c4_0 ).
tff(declare_ssSkC7,type,
ssSkC7: $o ).
tff(ssSkC7_definition,axiom,
~ ssSkC7 ).
tff(declare_ssSkC4,type,
ssSkC4: $o ).
tff(ssSkC4_definition,axiom,
ssSkC4 ).
tff(declare_ssSkC3,type,
ssSkC3: $o ).
tff(ssSkC3_definition,axiom,
ssSkC3 ).
tff(declare_ssSkC1,type,
ssSkC1: $o ).
tff(ssSkC1_definition,axiom,
ssSkC1 ).
tff(declare_ssSkC0,type,
ssSkC0: $o ).
tff(ssSkC0_definition,axiom,
ssSkC0 ).
tff(declare_ssSkC5,type,
ssSkC5: $o ).
tff(ssSkC5_definition,axiom,
~ ssSkC5 ).
tff(declare_c1_0,type,
c1_0: $o ).
tff(c1_0_definition,axiom,
~ c1_0 ).
tff(declare_ssSkC6,type,
ssSkC6: $o ).
tff(ssSkC6_definition,axiom,
ssSkC6 ).
tff(declare_c2_0,type,
c2_0: $o ).
tff(c2_0_definition,axiom,
~ c2_0 ).
tff(declare_ssSkC2,type,
ssSkC2: $o ).
tff(ssSkC2_definition,axiom,
ssSkC2 ).
tff(declare_ndr1_1,type,
ndr1_1: $i > $o ).
tff(predicate_ndr1_1,axiom,
ndr1_1('fmb_$i_1') ).
tff(declare_c2_1,type,
c2_1: $i > $o ).
tff(predicate_c2_1,axiom,
~ c2_1('fmb_$i_1') ).
tff(declare_c3_1,type,
c3_1: $i > $o ).
tff(predicate_c3_1,axiom,
~ c3_1('fmb_$i_1') ).
tff(declare_c5_1,type,
c5_1: $i > $o ).
tff(predicate_c5_1,axiom,
c5_1('fmb_$i_1') ).
tff(declare_ssSkP3,type,
ssSkP3: $i > $o ).
tff(predicate_ssSkP3,axiom,
ssSkP3('fmb_$i_1') ).
tff(declare_ssSkP2,type,
ssSkP2: $i > $o ).
tff(predicate_ssSkP2,axiom,
ssSkP2('fmb_$i_1') ).
tff(declare_ssSkP1,type,
ssSkP1: $i > $o ).
tff(predicate_ssSkP1,axiom,
ssSkP1('fmb_$i_1') ).
tff(declare_ssSkP0,type,
ssSkP0: $i > $o ).
tff(predicate_ssSkP0,axiom,
ssSkP0('fmb_$i_1') ).
tff(declare_c1_2,type,
c1_2: ( $i * $i ) > $o ).
tff(predicate_c1_2,axiom,
~ c1_2('fmb_$i_1','fmb_$i_1') ).
tff(declare_c1_1,type,
c1_1: $i > $o ).
tff(predicate_c1_1,axiom,
c1_1('fmb_$i_1') ).
tff(declare_c4_1,type,
c4_1: $i > $o ).
tff(predicate_c4_1,axiom,
c4_1('fmb_$i_1') ).
tff(declare_c5_2,type,
c5_2: ( $i * $i ) > $o ).
tff(predicate_c5_2,axiom,
c5_2('fmb_$i_1','fmb_$i_1') ).
tff(declare_c4_2,type,
c4_2: ( $i * $i ) > $o ).
tff(predicate_c4_2,axiom,
c4_2('fmb_$i_1','fmb_$i_1') ).
tff(declare_c3_2,type,
c3_2: ( $i * $i ) > $o ).
tff(predicate_c3_2,axiom,
~ c3_2('fmb_$i_1','fmb_$i_1') ).
tff(declare_c2_2,type,
c2_2: ( $i * $i ) > $o ).
tff(predicate_c2_2,axiom,
c2_2('fmb_$i_1','fmb_$i_1') ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN539-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n016.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 16:31:49 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.24 % (3746982)Will run a generic schedule for satisfiability detection.
% 0.08/0.24 % (3746987)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=420841282_2999 on theBenchmark for (2999ds/0Mi)
% 0.08/0.24 % Detected minimum model sizes of [1]
% 0.08/0.24 % Detected maximum model sizes of [51]
% 0.08/0.24 % TRYING [1]
% 0.08/0.24 % Finite Model Found!
% 0.08/0.24 % SZS status Satisfiable for theBenchmark
% 0.08/0.24 % (3746987) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3746982-3746987"...
% 0.08/0.24 % (3746987)...printing done.
% 0.08/0.24 % SZS output start FiniteModel for theBenchmark
% See solution above
% 0.08/0.24 % (3746987)------------------------------
% 0.08/0.24 % (3746987)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.08/0.24 % (3746987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.08/0.24 % (3746987)CaDiCaL version: 2.1.3
% 0.08/0.24 % (3746987)Termination reason: Satisfiable
% 0.08/0.24 % (3746987)Time elapsed: 0.005 s
% 0.08/0.24 % (3746987)Peak memory usage: 11 MB
% 0.08/0.24 % (3746987)Instructions burned: 17 (million)
% 0.08/0.24 % (3746982)Success in time 0.021 s
% 0.08/0.24 % Vampire exiting
%------------------------------------------------------------------------------