%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYN537-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 : n014.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.25s
% 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_a659,type,
a659: $i ).
tff(a659_definition,axiom,
a659 = 'fmb_$i_1' ).
tff(declare_a666,type,
a666: $i ).
tff(a666_definition,axiom,
a666 = 'fmb_$i_1' ).
tff(declare_a643,type,
a643: $i ).
tff(a643_definition,axiom,
a643 = 'fmb_$i_1' ).
tff(declare_a674,type,
a674: $i ).
tff(a674_definition,axiom,
a674 = 'fmb_$i_1' ).
tff(declare_a669,type,
a669: $i ).
tff(a669_definition,axiom,
a669 = 'fmb_$i_1' ).
tff(declare_a667,type,
a667: $i ).
tff(a667_definition,axiom,
a667 = 'fmb_$i_1' ).
tff(declare_a665,type,
a665: $i ).
tff(a665_definition,axiom,
a665 = 'fmb_$i_1' ).
tff(declare_a660,type,
a660: $i ).
tff(a660_definition,axiom,
a660 = 'fmb_$i_1' ).
tff(declare_a679,type,
a679: $i ).
tff(a679_definition,axiom,
a679 = 'fmb_$i_1' ).
tff(declare_a678,type,
a678: $i ).
tff(a678_definition,axiom,
a678 = 'fmb_$i_1' ).
tff(declare_a672,type,
a672: $i ).
tff(a672_definition,axiom,
a672 = 'fmb_$i_1' ).
tff(declare_a649,type,
a649: $i ).
tff(a649_definition,axiom,
a649 = 'fmb_$i_1' ).
tff(declare_a644,type,
a644: $i ).
tff(a644_definition,axiom,
a644 = 'fmb_$i_1' ).
tff(declare_a680,type,
a680: $i ).
tff(a680_definition,axiom,
a680 = 'fmb_$i_1' ).
tff(declare_a670,type,
a670: $i ).
tff(a670_definition,axiom,
a670 = 'fmb_$i_1' ).
tff(declare_a661,type,
a661: $i ).
tff(a661_definition,axiom,
a661 = 'fmb_$i_1' ).
tff(declare_a676,type,
a676: $i ).
tff(a676_definition,axiom,
a676 = 'fmb_$i_1' ).
tff(declare_a668,type,
a668: $i ).
tff(a668_definition,axiom,
a668 = 'fmb_$i_1' ).
tff(declare_a662,type,
a662: $i ).
tff(a662_definition,axiom,
a662 = 'fmb_$i_1' ).
tff(declare_a651,type,
a651: $i ).
tff(a651_definition,axiom,
a651 = 'fmb_$i_1' ).
tff(declare_a652,type,
a652: $i ).
tff(a652_definition,axiom,
a652 = 'fmb_$i_1' ).
tff(declare_a677,type,
a677: $i ).
tff(a677_definition,axiom,
a677 = 'fmb_$i_1' ).
tff(declare_a657,type,
a657: $i ).
tff(a657_definition,axiom,
a657 = 'fmb_$i_1' ).
tff(declare_a650,type,
a650: $i ).
tff(a650_definition,axiom,
a650 = 'fmb_$i_1' ).
tff(declare_a653,type,
a653: $i ).
tff(a653_definition,axiom,
a653 = 'fmb_$i_1' ).
tff(declare_a656,type,
a656: $i ).
tff(a656_definition,axiom,
a656 = 'fmb_$i_1' ).
tff(declare_a647,type,
a647: $i ).
tff(a647_definition,axiom,
a647 = 'fmb_$i_1' ).
tff(declare_a673,type,
a673: $i ).
tff(a673_definition,axiom,
a673 = 'fmb_$i_1' ).
tff(declare_a654,type,
a654: $i ).
tff(a654_definition,axiom,
a654 = 'fmb_$i_1' ).
tff(declare_a655,type,
a655: $i ).
tff(a655_definition,axiom,
a655 = 'fmb_$i_1' ).
tff(declare_a658,type,
a658: $i ).
tff(a658_definition,axiom,
a658 = 'fmb_$i_1' ).
tff(declare_a675,type,
a675: $i ).
tff(a675_definition,axiom,
a675 = 'fmb_$i_1' ).
tff(declare_a648,type,
a648: $i ).
tff(a648_definition,axiom,
a648 = 'fmb_$i_1' ).
tff(declare_a640,type,
a640: $i ).
tff(a640_definition,axiom,
a640 = 'fmb_$i_1' ).
tff(declare_c1_0,type,
c1_0: $o ).
tff(c1_0_definition,axiom,
c1_0 ).
tff(declare_ndr1_0,type,
ndr1_0: $o ).
tff(ndr1_0_definition,axiom,
ndr1_0 ).
tff(declare_c5_0,type,
c5_0: $o ).
tff(c5_0_definition,axiom,
c5_0 ).
tff(declare_c3_0,type,
c3_0: $o ).
tff(c3_0_definition,axiom,
~ c3_0 ).
tff(declare_ssSkC5,type,
ssSkC5: $o ).
tff(ssSkC5_definition,axiom,
ssSkC5 ).
tff(declare_ssSkC4,type,
ssSkC4: $o ).
tff(ssSkC4_definition,axiom,
~ ssSkC4 ).
tff(declare_ssSkC3,type,
ssSkC3: $o ).
tff(ssSkC3_definition,axiom,
ssSkC3 ).
tff(declare_ssSkC2,type,
ssSkC2: $o ).
tff(ssSkC2_definition,axiom,
~ ssSkC2 ).
tff(declare_ssSkC0,type,
ssSkC0: $o ).
tff(ssSkC0_definition,axiom,
ssSkC0 ).
tff(declare_c2_0,type,
c2_0: $o ).
tff(c2_0_definition,axiom,
~ c2_0 ).
tff(declare_c4_0,type,
c4_0: $o ).
tff(c4_0_definition,axiom,
c4_0 ).
tff(declare_ssSkC1,type,
ssSkC1: $o ).
tff(ssSkC1_definition,axiom,
ssSkC1 ).
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_ndr1_1,type,
ndr1_1: $i > $o ).
tff(predicate_ndr1_1,axiom,
ndr1_1('fmb_$i_1') ).
tff(declare_ssSkP0,type,
ssSkP0: $i > $o ).
tff(predicate_ssSkP0,axiom,
ssSkP0('fmb_$i_1') ).
tff(declare_c4_1,type,
c4_1: $i > $o ).
tff(predicate_c4_1,axiom,
~ c4_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_c5_1,type,
c5_1: $i > $o ).
tff(predicate_c5_1,axiom,
~ c5_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_c1_2,type,
c1_2: ( $i * $i ) > $o ).
tff(predicate_c1_2,axiom,
c1_2('fmb_$i_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_c2_2,type,
c2_2: ( $i * $i ) > $o ).
tff(predicate_c2_2,axiom,
~ c2_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') ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN537-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n014.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:26:46 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 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.25 % (1906845)Will run a generic schedule for satisfiability detection.
% 0.08/0.25 % (1906851)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=535101172_2999 on theBenchmark for (2999ds/0Mi)
% 0.08/0.25 % Detected minimum model sizes of [1]
% 0.08/0.25 % Detected maximum model sizes of [32]
% 0.08/0.25 % TRYING [1]
% 0.08/0.25 % Finite Model Found!
% 0.08/0.25 % SZS status Satisfiable for theBenchmark
% 0.08/0.25 % (1906851) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1906845-1906851"...
% 0.08/0.25 % (1906852)% WARNING: option uhcvi not known.
% 0.08/0.25 % (1906851)...printing done.
% 0.08/0.25 % SZS output start FiniteModel for theBenchmark
% See solution above
% 0.08/0.25 % (1906851)------------------------------
% 0.08/0.25 % (1906851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.08/0.25 % (1906851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.08/0.25 % (1906851)CaDiCaL version: 2.1.3
% 0.08/0.25 % (1906851)Termination reason: Satisfiable
% 0.08/0.25 % (1906851)Time elapsed: 0.004 s
% 0.08/0.25 % (1906851)Peak memory usage: 11 MB
% 0.08/0.25 % (1906851)Instructions burned: 11 (million)
% 0.08/0.25 % (1906845)Success in time 0.02 s
% 0.08/0.25 % Vampire exiting
%------------------------------------------------------------------------------