%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL685+1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n001.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 12:00:17 PM UTC 2026
% Result : CounterSatisfiable 0.17s 0.54s
% Output : FiniteModel 0.17s
% 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.02 % Problem : LCL685+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.38 % Computer : n001.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 16:44:02 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.41 Running first-order model finding
% 0.10/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.54 % (3772207)Will run a generic schedule for satisfiability detection.
% 0.17/0.54 % (3772212)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2782126083_2999 on theBenchmark for (2999ds/0Mi)
% 0.17/0.54 % (3772213)% WARNING: option uhcvi not known.
% 0.17/0.54 % (3772213)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=684503062:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.17/0.54 % (3772214)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1897658130:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.17/0.54 % (3772215)dis+10_1_sil=32000:sp=arity:random_seed=677850975:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.17/0.54 % (3772218)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1130189500:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.17/0.54 % (3772216)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1665599216:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.17/0.54 % (3772217)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=191322226:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.17/0.54 % TRYING [1]
% 0.17/0.54 % (3772215)Instruction limit reached!
% 0.17/0.54 % (3772215)------------------------------
% 0.17/0.54 % (3772215)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.17/0.54 % (3772215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/0.54 % (3772215)CaDiCaL version: 2.1.3
% 0.17/0.54 % (3772215)Termination reason: Instruction limit
% 0.17/0.54 % (3772215)Termination phase: Saturation
% 0.17/0.54 % (3772215)Time elapsed: 0.053 s
% 0.17/0.54 % (3772215)Peak memory usage: 15 MB
% 0.17/0.54 % (3772215)Instructions burned: 103 (million)
% 0.17/0.54 % (3772216)Instruction limit reached!
% 0.17/0.54 % (3772216)------------------------------
% 0.17/0.54 % (3772216)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.17/0.54 % (3772216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/0.54 % (3772216)CaDiCaL version: 2.1.3
% 0.17/0.54 % (3772216)Termination reason: Instruction limit
% 0.17/0.54 % (3772216)Termination phase: Saturation
% 0.17/0.54 % (3772216)Time elapsed: 0.060 s
% 0.17/0.54 % (3772216)Peak memory usage: 14 MB
% 0.17/0.54 % (3772216)Instructions burned: 118 (million)
% 0.17/0.54 % (3772217)Instruction limit reached!
% 0.17/0.54 % (3772217)------------------------------
% 0.17/0.54 % (3772217)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.17/0.54 % (3772217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/0.54 % (3772217)CaDiCaL version: 2.1.3
% 0.17/0.54 % (3772217)Termination reason: Instruction limit
% 0.17/0.54 % (3772217)Termination phase: Saturation
% 0.17/0.54 % (3772217)Time elapsed: 0.068 s
% 0.17/0.54 % (3772217)Peak memory usage: 16 MB
% 0.17/0.54 % (3772217)Instructions burned: 136 (million)
% 0.17/0.54 % Finite Model Found!
% 0.17/0.54 % SZS status CounterSatisfiable for theBenchmark
% 0.17/0.54 % (3772226)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1386292513:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.17/0.54 % (3772212) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3772207-3772212"...
% 0.17/0.54 % (3772212)...printing done.
% 0.17/0.54 % SZS output start FiniteModel for theBenchmark
% See solution above
% 0.17/0.55 % (3772212)------------------------------
% 0.17/0.55 % (3772212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.17/0.55 % (3772212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/0.55 % (3772212)CaDiCaL version: 2.1.3
% 0.17/0.55 % (3772212)Termination reason: Satisfiable
% 0.17/0.55 % (3772212)Time elapsed: 0.082 s
% 0.17/0.55 % (3772212)Peak memory usage: 19 MB
% 0.17/0.55 % (3772212)Instructions burned: 312 (million)
% 0.17/0.55 % (3772207)Success in time 0.123 s
% 0.17/0.55 % Vampire exiting
%------------------------------------------------------------------------------