%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL667+1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n013.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 11:59:46 AM UTC 2026
% Result : CounterSatisfiable 0.43s 0.56s
% Output : FiniteModel 0.43s
% 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_r1,type,
r1: ( $i * $i ) > $o ).
tff(predicate_r1,axiom,
r1('fmb_$i_1','fmb_$i_1') ).
tff(declare_p1110,type,
p1110: $i > $o ).
tff(predicate_p1110,axiom,
~ p1110('fmb_$i_1') ).
tff(declare_p1010,type,
p1010: $i > $o ).
tff(predicate_p1010,axiom,
~ p1010('fmb_$i_1') ).
tff(declare_p910,type,
p910: $i > $o ).
tff(predicate_p910,axiom,
~ p910('fmb_$i_1') ).
tff(declare_p810,type,
p810: $i > $o ).
tff(predicate_p810,axiom,
~ p810('fmb_$i_1') ).
tff(declare_p710,type,
p710: $i > $o ).
tff(predicate_p710,axiom,
~ p710('fmb_$i_1') ).
tff(declare_p610,type,
p610: $i > $o ).
tff(predicate_p610,axiom,
~ p610('fmb_$i_1') ).
tff(declare_p510,type,
p510: $i > $o ).
tff(predicate_p510,axiom,
~ p510('fmb_$i_1') ).
tff(declare_p410,type,
p410: $i > $o ).
tff(predicate_p410,axiom,
p410('fmb_$i_1') ).
tff(declare_p310,type,
p310: $i > $o ).
tff(predicate_p310,axiom,
~ p310('fmb_$i_1') ).
tff(declare_p210,type,
p210: $i > $o ).
tff(predicate_p210,axiom,
~ p210('fmb_$i_1') ).
tff(declare_p110,type,
p110: $i > $o ).
tff(predicate_p110,axiom,
~ p110('fmb_$i_1') ).
tff(declare_p1109,type,
p1109: $i > $o ).
tff(predicate_p1109,axiom,
~ p1109('fmb_$i_1') ).
tff(declare_p1009,type,
p1009: $i > $o ).
tff(predicate_p1009,axiom,
p1009('fmb_$i_1') ).
tff(declare_p909,type,
p909: $i > $o ).
tff(predicate_p909,axiom,
~ p909('fmb_$i_1') ).
tff(declare_p809,type,
p809: $i > $o ).
tff(predicate_p809,axiom,
~ p809('fmb_$i_1') ).
tff(declare_p709,type,
p709: $i > $o ).
tff(predicate_p709,axiom,
~ p709('fmb_$i_1') ).
tff(declare_p609,type,
p609: $i > $o ).
tff(predicate_p609,axiom,
~ p609('fmb_$i_1') ).
tff(declare_p509,type,
p509: $i > $o ).
tff(predicate_p509,axiom,
~ p509('fmb_$i_1') ).
tff(declare_p409,type,
p409: $i > $o ).
tff(predicate_p409,axiom,
~ p409('fmb_$i_1') ).
tff(declare_p309,type,
p309: $i > $o ).
tff(predicate_p309,axiom,
~ p309('fmb_$i_1') ).
tff(declare_p209,type,
p209: $i > $o ).
tff(predicate_p209,axiom,
~ p209('fmb_$i_1') ).
tff(declare_p109,type,
p109: $i > $o ).
tff(predicate_p109,axiom,
~ p109('fmb_$i_1') ).
tff(declare_p1108,type,
p1108: $i > $o ).
tff(predicate_p1108,axiom,
~ p1108('fmb_$i_1') ).
tff(declare_p1008,type,
p1008: $i > $o ).
tff(predicate_p1008,axiom,
~ p1008('fmb_$i_1') ).
tff(declare_p908,type,
p908: $i > $o ).
tff(predicate_p908,axiom,
p908('fmb_$i_1') ).
tff(declare_p808,type,
p808: $i > $o ).
tff(predicate_p808,axiom,
~ p808('fmb_$i_1') ).
tff(declare_p708,type,
p708: $i > $o ).
tff(predicate_p708,axiom,
~ p708('fmb_$i_1') ).
tff(declare_p608,type,
p608: $i > $o ).
tff(predicate_p608,axiom,
~ p608('fmb_$i_1') ).
tff(declare_p508,type,
p508: $i > $o ).
tff(predicate_p508,axiom,
~ p508('fmb_$i_1') ).
tff(declare_p408,type,
p408: $i > $o ).
tff(predicate_p408,axiom,
~ p408('fmb_$i_1') ).
tff(declare_p308,type,
p308: $i > $o ).
tff(predicate_p308,axiom,
~ p308('fmb_$i_1') ).
tff(declare_p208,type,
p208: $i > $o ).
tff(predicate_p208,axiom,
~ p208('fmb_$i_1') ).
tff(declare_p108,type,
p108: $i > $o ).
tff(predicate_p108,axiom,
~ p108('fmb_$i_1') ).
tff(declare_p1107,type,
p1107: $i > $o ).
tff(predicate_p1107,axiom,
~ p1107('fmb_$i_1') ).
tff(declare_p1007,type,
p1007: $i > $o ).
tff(predicate_p1007,axiom,
~ p1007('fmb_$i_1') ).
tff(declare_p907,type,
p907: $i > $o ).
tff(predicate_p907,axiom,
~ p907('fmb_$i_1') ).
tff(declare_p807,type,
p807: $i > $o ).
tff(predicate_p807,axiom,
~ p807('fmb_$i_1') ).
tff(declare_p707,type,
p707: $i > $o ).
tff(predicate_p707,axiom,
p707('fmb_$i_1') ).
tff(declare_p607,type,
p607: $i > $o ).
tff(predicate_p607,axiom,
~ p607('fmb_$i_1') ).
tff(declare_p507,type,
p507: $i > $o ).
tff(predicate_p507,axiom,
~ p507('fmb_$i_1') ).
tff(declare_p407,type,
p407: $i > $o ).
tff(predicate_p407,axiom,
~ p407('fmb_$i_1') ).
tff(declare_p307,type,
p307: $i > $o ).
tff(predicate_p307,axiom,
p307('fmb_$i_1') ).
tff(declare_p207,type,
p207: $i > $o ).
tff(predicate_p207,axiom,
~ p207('fmb_$i_1') ).
tff(declare_p107,type,
p107: $i > $o ).
tff(predicate_p107,axiom,
~ p107('fmb_$i_1') ).
tff(declare_p1106,type,
p1106: $i > $o ).
tff(predicate_p1106,axiom,
~ p1106('fmb_$i_1') ).
tff(declare_p1006,type,
p1006: $i > $o ).
tff(predicate_p1006,axiom,
~ p1006('fmb_$i_1') ).
tff(declare_p906,type,
p906: $i > $o ).
tff(predicate_p906,axiom,
~ p906('fmb_$i_1') ).
tff(declare_p806,type,
p806: $i > $o ).
tff(predicate_p806,axiom,
~ p806('fmb_$i_1') ).
tff(declare_p706,type,
p706: $i > $o ).
tff(predicate_p706,axiom,
~ p706('fmb_$i_1') ).
tff(declare_p606,type,
p606: $i > $o ).
tff(predicate_p606,axiom,
~ p606('fmb_$i_1') ).
tff(declare_p506,type,
p506: $i > $o ).
tff(predicate_p506,axiom,
~ p506('fmb_$i_1') ).
tff(declare_p406,type,
p406: $i > $o ).
tff(predicate_p406,axiom,
~ p406('fmb_$i_1') ).
tff(declare_p306,type,
p306: $i > $o ).
tff(predicate_p306,axiom,
~ p306('fmb_$i_1') ).
tff(declare_p206,type,
p206: $i > $o ).
tff(predicate_p206,axiom,
p206('fmb_$i_1') ).
tff(declare_p106,type,
p106: $i > $o ).
tff(predicate_p106,axiom,
~ p106('fmb_$i_1') ).
tff(declare_p1105,type,
p1105: $i > $o ).
tff(predicate_p1105,axiom,
~ p1105('fmb_$i_1') ).
tff(declare_p1005,type,
p1005: $i > $o ).
tff(predicate_p1005,axiom,
~ p1005('fmb_$i_1') ).
tff(declare_p905,type,
p905: $i > $o ).
tff(predicate_p905,axiom,
~ p905('fmb_$i_1') ).
tff(declare_p805,type,
p805: $i > $o ).
tff(predicate_p805,axiom,
~ p805('fmb_$i_1') ).
tff(declare_p705,type,
p705: $i > $o ).
tff(predicate_p705,axiom,
~ p705('fmb_$i_1') ).
tff(declare_p605,type,
p605: $i > $o ).
tff(predicate_p605,axiom,
~ p605('fmb_$i_1') ).
tff(declare_p505,type,
p505: $i > $o ).
tff(predicate_p505,axiom,
p505('fmb_$i_1') ).
tff(declare_p405,type,
p405: $i > $o ).
tff(predicate_p405,axiom,
~ p405('fmb_$i_1') ).
tff(declare_p305,type,
p305: $i > $o ).
tff(predicate_p305,axiom,
~ p305('fmb_$i_1') ).
tff(declare_p205,type,
p205: $i > $o ).
tff(predicate_p205,axiom,
~ p205('fmb_$i_1') ).
tff(declare_p105,type,
p105: $i > $o ).
tff(predicate_p105,axiom,
~ p105('fmb_$i_1') ).
tff(declare_p1104,type,
p1104: $i > $o ).
tff(predicate_p1104,axiom,
~ p1104('fmb_$i_1') ).
tff(declare_p1004,type,
p1004: $i > $o ).
tff(predicate_p1004,axiom,
~ p1004('fmb_$i_1') ).
tff(declare_p904,type,
p904: $i > $o ).
tff(predicate_p904,axiom,
~ p904('fmb_$i_1') ).
tff(declare_p804,type,
p804: $i > $o ).
tff(predicate_p804,axiom,
~ p804('fmb_$i_1') ).
tff(declare_p704,type,
p704: $i > $o ).
tff(predicate_p704,axiom,
~ p704('fmb_$i_1') ).
tff(declare_p604,type,
p604: $i > $o ).
tff(predicate_p604,axiom,
p604('fmb_$i_1') ).
tff(declare_p504,type,
p504: $i > $o ).
tff(predicate_p504,axiom,
~ p504('fmb_$i_1') ).
tff(declare_p404,type,
p404: $i > $o ).
tff(predicate_p404,axiom,
~ p404('fmb_$i_1') ).
tff(declare_p304,type,
p304: $i > $o ).
tff(predicate_p304,axiom,
~ p304('fmb_$i_1') ).
tff(declare_p204,type,
p204: $i > $o ).
tff(predicate_p204,axiom,
~ p204('fmb_$i_1') ).
tff(declare_p104,type,
p104: $i > $o ).
tff(predicate_p104,axiom,
~ p104('fmb_$i_1') ).
tff(declare_p1103,type,
p1103: $i > $o ).
tff(predicate_p1103,axiom,
~ p1103('fmb_$i_1') ).
tff(declare_p1003,type,
p1003: $i > $o ).
tff(predicate_p1003,axiom,
~ p1003('fmb_$i_1') ).
tff(declare_p903,type,
p903: $i > $o ).
tff(predicate_p903,axiom,
~ p903('fmb_$i_1') ).
tff(declare_p803,type,
p803: $i > $o ).
tff(predicate_p803,axiom,
p803('fmb_$i_1') ).
tff(declare_p703,type,
p703: $i > $o ).
tff(predicate_p703,axiom,
~ p703('fmb_$i_1') ).
tff(declare_p603,type,
p603: $i > $o ).
tff(predicate_p603,axiom,
~ p603('fmb_$i_1') ).
tff(declare_p503,type,
p503: $i > $o ).
tff(predicate_p503,axiom,
~ p503('fmb_$i_1') ).
tff(declare_p403,type,
p403: $i > $o ).
tff(predicate_p403,axiom,
~ p403('fmb_$i_1') ).
tff(declare_p303,type,
p303: $i > $o ).
tff(predicate_p303,axiom,
~ p303('fmb_$i_1') ).
tff(declare_p203,type,
p203: $i > $o ).
tff(predicate_p203,axiom,
~ p203('fmb_$i_1') ).
tff(declare_p103,type,
p103: $i > $o ).
tff(predicate_p103,axiom,
~ p103('fmb_$i_1') ).
tff(declare_p1102,type,
p1102: $i > $o ).
tff(predicate_p1102,axiom,
p1102('fmb_$i_1') ).
tff(declare_p1002,type,
p1002: $i > $o ).
tff(predicate_p1002,axiom,
~ p1002('fmb_$i_1') ).
tff(declare_p902,type,
p902: $i > $o ).
tff(predicate_p902,axiom,
~ p902('fmb_$i_1') ).
tff(declare_p802,type,
p802: $i > $o ).
tff(predicate_p802,axiom,
~ p802('fmb_$i_1') ).
tff(declare_p702,type,
p702: $i > $o ).
tff(predicate_p702,axiom,
~ p702('fmb_$i_1') ).
tff(declare_p602,type,
p602: $i > $o ).
tff(predicate_p602,axiom,
~ p602('fmb_$i_1') ).
tff(declare_p502,type,
p502: $i > $o ).
tff(predicate_p502,axiom,
~ p502('fmb_$i_1') ).
tff(declare_p402,type,
p402: $i > $o ).
tff(predicate_p402,axiom,
~ p402('fmb_$i_1') ).
tff(declare_p302,type,
p302: $i > $o ).
tff(predicate_p302,axiom,
~ p302('fmb_$i_1') ).
tff(declare_p202,type,
p202: $i > $o ).
tff(predicate_p202,axiom,
~ p202('fmb_$i_1') ).
tff(declare_p102,type,
p102: $i > $o ).
tff(predicate_p102,axiom,
~ p102('fmb_$i_1') ).
tff(declare_p1101,type,
p1101: $i > $o ).
tff(predicate_p1101,axiom,
~ p1101('fmb_$i_1') ).
tff(declare_p1001,type,
p1001: $i > $o ).
tff(predicate_p1001,axiom,
~ p1001('fmb_$i_1') ).
tff(declare_p901,type,
p901: $i > $o ).
tff(predicate_p901,axiom,
~ p901('fmb_$i_1') ).
tff(declare_p801,type,
p801: $i > $o ).
tff(predicate_p801,axiom,
~ p801('fmb_$i_1') ).
tff(declare_p701,type,
p701: $i > $o ).
tff(predicate_p701,axiom,
~ p701('fmb_$i_1') ).
tff(declare_p601,type,
p601: $i > $o ).
tff(predicate_p601,axiom,
~ p601('fmb_$i_1') ).
tff(declare_p501,type,
p501: $i > $o ).
tff(predicate_p501,axiom,
~ p501('fmb_$i_1') ).
tff(declare_p401,type,
p401: $i > $o ).
tff(predicate_p401,axiom,
~ p401('fmb_$i_1') ).
tff(declare_p301,type,
p301: $i > $o ).
tff(predicate_p301,axiom,
~ p301('fmb_$i_1') ).
tff(declare_p201,type,
p201: $i > $o ).
tff(predicate_p201,axiom,
~ p201('fmb_$i_1') ).
tff(declare_p101,type,
p101: $i > $o ).
tff(predicate_p101,axiom,
p101('fmb_$i_1') ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL667+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.37 % Computer : n013.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 : Sun Sep 27 16:27:07 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.16/0.43 Running first-order model finding
% 0.16/0.43 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.43/0.56 % (390980)Will run a generic schedule for satisfiability detection.
% 0.43/0.56 % (390985)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3580307223_2999 on theBenchmark for (2999ds/0Mi)
% 0.43/0.56 % (390986)% WARNING: option uhcvi not known.
% 0.43/0.56 % (390986)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=28042107:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.43/0.56 % (390989)dis+10_1_sil=32000:sp=arity:random_seed=3722201356:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.43/0.56 % (390990)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1407640937:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.43/0.56 % (390987)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3735886344:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.43/0.56 % (390992)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=881170330:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.43/0.56 % (390991)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1652327844:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.43/0.56 % TRYING [1]
% 0.43/0.56 % Finite Model Found!
% 0.43/0.56 % SZS status CounterSatisfiable for theBenchmark
% 0.43/0.56 % (390985) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-390980-390985"...
% 0.43/0.56 % (390985)...printing done.
% 0.43/0.56 % SZS output start FiniteModel for theBenchmark
% See solution above
% 0.43/0.57 % (390985)------------------------------
% 0.43/0.57 % (390985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.43/0.57 % (390985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.43/0.57 % (390985)CaDiCaL version: 2.1.3
% 0.43/0.57 % (390985)Termination reason: Satisfiable
% 0.43/0.57 % (390985)Time elapsed: 0.088 s
% 0.43/0.57 % (390985)Peak memory usage: 16 MB
% 0.43/0.57 % (390985)Instructions burned: 238 (million)
% 0.43/0.57 % (390980)Success in time 0.126 s
% 0.43/0.57 % Vampire exiting
%------------------------------------------------------------------------------