%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL643+1.015 : 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 : 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 11:59:09 AM UTC 2026
% Result : CounterSatisfiable 0.13s 0.44s
% Output : Saturation 0.13s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u592,axiom,
~ p2(sK54(X0)) ).
cnf(u595,axiom,
~ sP45(X0) ).
cnf(u598,axiom,
~ p2(sK61(X0)) ).
cnf(u601,axiom,
~ sP43(X0) ).
cnf(u604,axiom,
~ p1(sK66(X0)) ).
cnf(u607,axiom,
~ sP41(X0) ).
cnf(u610,negated_conjecture,
~ r1(sK124,sK131) ).
cnf(u615,negated_conjecture,
sP47(sK124) ).
cnf(u619,axiom,
~ p1(sK68(X0)) ).
cnf(u622,axiom,
~ sP39(X0) ).
cnf(u625,axiom,
~ p1(sK69(X0)) ).
cnf(u628,axiom,
~ sP38(X0) ).
cnf(u631,axiom,
~ p1(sK71(X0)) ).
cnf(u634,axiom,
~ sP37(X0) ).
cnf(u637,axiom,
~ p1(sK72(X0)) ).
cnf(u640,axiom,
~ sP36(X0) ).
cnf(u644,axiom,
~ p1(sK74(X0)) ).
cnf(u647,axiom,
~ sP35(X0) ).
cnf(u650,axiom,
~ p1(sK76(X0)) ).
cnf(u653,axiom,
~ sP33(X0) ).
cnf(u656,axiom,
~ p1(sK77(X0)) ).
cnf(u659,axiom,
~ sP32(X0) ).
cnf(u662,axiom,
~ p1(sK79(X0)) ).
cnf(u665,axiom,
~ sP31(X0) ).
cnf(u668,axiom,
~ p1(sK80(X0)) ).
cnf(u671,axiom,
~ sP30(X0) ).
cnf(u674,axiom,
~ p1(sK82(X0)) ).
cnf(u677,axiom,
~ sP28(X0) ).
cnf(u680,axiom,
~ p1(sK83(X0)) ).
cnf(u683,axiom,
~ sP27(X0) ).
cnf(u686,axiom,
~ p1(sK85(X0)) ).
cnf(u689,axiom,
~ sP26(X0) ).
cnf(u692,axiom,
~ p1(sK86(X0)) ).
cnf(u695,axiom,
~ sP25(X0) ).
cnf(u698,axiom,
~ p1(sK88(X0)) ).
cnf(u701,axiom,
~ sP23(X0) ).
cnf(u704,axiom,
~ p1(sK89(X0)) ).
cnf(u707,axiom,
~ sP22(X0) ).
cnf(u710,axiom,
~ p1(sK91(X0)) ).
cnf(u713,axiom,
~ sP21(X0) ).
cnf(u716,axiom,
~ p1(sK92(X0)) ).
cnf(u719,axiom,
~ sP20(X0) ).
cnf(u722,axiom,
~ p1(sK94(X0)) ).
cnf(u725,axiom,
~ sP19(X0) ).
cnf(u728,axiom,
~ p1(sK96(X0)) ).
cnf(u731,axiom,
~ sP17(X0) ).
cnf(u734,axiom,
~ p1(sK98(X0)) ).
cnf(u737,axiom,
~ sP16(X0) ).
cnf(u740,axiom,
~ p1(sK100(X0)) ).
cnf(u743,axiom,
~ sP15(X0) ).
cnf(u747,negated_conjecture,
~ p2(sK131) ).
cnf(u751,axiom,
~ p1(sK102(X0)) ).
cnf(u754,axiom,
~ sP13(X0) ).
cnf(u757,axiom,
~ p1(sK104(X0)) ).
cnf(u760,axiom,
~ sP12(X0) ).
cnf(u763,axiom,
~ p1(sK106(X0)) ).
cnf(u766,axiom,
~ sP10(X0) ).
cnf(u769,axiom,
~ p1(sK108(X0)) ).
cnf(u772,axiom,
~ sP9(X0) ).
cnf(u775,axiom,
~ p1(sK110(X0)) ).
cnf(u778,axiom,
~ sP7(X0) ).
cnf(u781,axiom,
~ p1(sK112(X0)) ).
cnf(u784,axiom,
~ sP6(X0) ).
cnf(u787,axiom,
~ p1(sK114(X0)) ).
cnf(u790,axiom,
~ sP5(X0) ).
cnf(u793,axiom,
~ p1(sK118(X0)) ).
cnf(u796,axiom,
~ sP3(X0) ).
cnf(u799,negated_conjecture,
~ r1(sK124,X7) ).
cnf(u805,negated_conjecture,
p1(sK129(X7)) ).
cnf(u903,axiom,
~ r1(X0,X1) ).
cnf(u937,negated_conjecture,
~ r1(sK131,X13) ).
cnf(u940,negated_conjecture,
sP44(X13) ).
cnf(u943,negated_conjecture,
~ p2(X13) ).
cnf(u946,negated_conjecture,
~ p1(sK130(X7)) ).
cnf(u352,axiom,
( ~ p1(sK89(X0))
| ~ sP22(X0) ) ).
cnf(u215,axiom,
( ~ p2(sK54(X0))
| ~ sP45(X0) ) ).
cnf(u264,axiom,
( ~ p1(sK71(X0))
| ~ sP37(X0) ) ).
cnf(u442,axiom,
( ~ p1(sK110(X0))
| ~ sP7(X0) ) ).
cnf(u289,axiom,
( ~ p1(sK76(X0))
| ~ sP33(X0) ) ).
cnf(u426,axiom,
( ~ p1(sK106(X0))
| ~ sP10(X0) ) ).
cnf(u384,axiom,
( ~ p1(sK96(X0))
| ~ sP17(X0) ) ).
cnf(u230,axiom,
( ~ p2(sK61(X0))
| ~ sP43(X0) ) ).
cnf(u301,axiom,
( ~ p1(sK79(X0))
| ~ sP31(X0) ) ).
cnf(u409,axiom,
( ~ p1(sK102(X0))
| ~ sP13(X0) ) ).
cnf(u336,axiom,
( ~ p1(sK86(X0))
| ~ sP25(X0) ) ).
cnf(u346,axiom,
( ~ p1(sK88(X0))
| ~ sP23(X0) ) ).
cnf(u390,axiom,
( ~ p1(sK98(X0))
| ~ sP16(X0) ) ).
cnf(u364,axiom,
( ~ p1(sK92(X0))
| ~ sP20(X0) ) ).
cnf(u238,axiom,
( ~ p1(sK66(X0))
| ~ sP41(X0) ) ).
cnf(u199,axiom,
( ~ r1(X0,X1)
| p2(X1)
| p2(sK49(X1))
| ~ sP47(X0) ) ).
cnf(u448,axiom,
( ~ p1(sK112(X0))
| ~ sP6(X0) ) ).
cnf(u258,axiom,
( ~ p1(sK69(X0))
| ~ sP38(X0) ) ).
cnf(u276,axiom,
( ~ p1(sK74(X0))
| ~ sP35(X0) ) ).
cnf(u432,axiom,
( ~ p1(sK108(X0))
| ~ sP9(X0) ) ).
cnf(u415,axiom,
( ~ p1(sK104(X0))
| ~ sP12(X0) ) ).
cnf(u396,axiom,
( ~ p1(sK100(X0))
| ~ sP15(X0) ) ).
cnf(u589,negated_conjecture,
~ p3(sK124) ).
cnf(u295,axiom,
( ~ p1(sK77(X0))
| ~ sP32(X0) ) ).
cnf(u330,axiom,
( ~ p1(sK85(X0))
| ~ sP26(X0) ) ).
cnf(u358,axiom,
( ~ p1(sK91(X0))
| ~ sP21(X0) ) ).
cnf(u370,axiom,
( ~ p1(sK94(X0))
| ~ sP19(X0) ) ).
cnf(u252,axiom,
( ~ p1(sK68(X0))
| ~ sP39(X0) ) ).
cnf(u270,axiom,
( ~ p1(sK72(X0))
| ~ sP36(X0) ) ).
cnf(u579,negated_conjecture,
~ p1(sK124) ).
cnf(u575,negated_conjecture,
( ~ r1(sK124,X7)
| p1(X7)
| p1(sK129(X7)) ) ).
cnf(u576,negated_conjecture,
( ~ p1(sK130(X7))
| p1(X7)
| ~ r1(sK124,X7) ) ).
cnf(u307,axiom,
( ~ p1(sK80(X0))
| ~ sP30(X0) ) ).
cnf(u468,axiom,
( ~ p1(sK118(X0))
| ~ sP3(X0) ) ).
cnf(u324,axiom,
( ~ p1(sK83(X0))
| ~ sP27(X0) ) ).
cnf(u318,axiom,
( ~ p1(sK82(X0))
| ~ sP28(X0) ) ).
cnf(u454,axiom,
( ~ p1(sK114(X0))
| ~ sP5(X0) ) ).
cnf(u584,negated_conjecture,
~ p2(sK124) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL643+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.36 % Computer : n014.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 27 16:11:46 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.39 Running first-order model finding
% 0.13/0.39 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.13/0.44 % (979125)Will run a generic schedule for satisfiability detection.
% 0.13/0.44 % (979132)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=130805093:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.13/0.44 % (979131)% WARNING: option uhcvi not known.
% 0.13/0.44 % (979130)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1381645938_2999 on theBenchmark for (2999ds/0Mi)
% 0.13/0.44 % (979131)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=689372854:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.13/0.44 % (979133)dis+10_1_sil=32000:sp=arity:random_seed=974850211:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.13/0.44 % (979134)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3551065913:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.13/0.44 % (979136)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1052729456:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.13/0.44 % (979135)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1054006959:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.13/0.44 % (979132) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-979125-979132"...
% 0.13/0.44 % (979132)...printing done.
% 0.13/0.44 % SZS status CounterSatisfiable for theBenchmark
% 0.13/0.44 % SZS output start Saturation.
% See solution above
% 0.13/0.44 % SZS output start Definitions and Model Updates.
% 0.13/0.44 % SZS output end Definitions and Model Updates.
% 0.13/0.44 % (979132)------------------------------
% 0.13/0.44 % (979132)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.13/0.44 % (979132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.13/0.44 % (979132)CaDiCaL version: 2.1.3
% 0.13/0.44 % (979132)Termination reason: Satisfiable
% 0.13/0.44 % (979132)Time elapsed: 0.010 s
% 0.13/0.44 % (979132)Peak memory usage: 13 MB
% 0.13/0.44 % (979132)Instructions burned: 32 (million)
% 0.13/0.44 % (979125)Success in time 0.039 s
% 0.13/0.44 % Vampire exiting
%------------------------------------------------------------------------------