%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL681+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 : n010.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:05 PM UTC 2026
% Result : CounterSatisfiable 0.59s 0.57s
% Output : Saturation 0.59s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u95,negated_conjecture,
~ p1(X313) ).
cnf(u105,negated_conjecture,
r1(X282,sK45(X282)) ).
cnf(u110,negated_conjecture,
r1(X303,sK47(X303)) ).
cnf(u115,negated_conjecture,
r1(X252,sK42(X252)) ).
cnf(u127,negated_conjecture,
r1(X212,sK38(X212)) ).
cnf(u141,negated_conjecture,
r1(X162,sK33(X162)) ).
cnf(u157,negated_conjecture,
r1(X102,sK27(X102)) ).
cnf(u175,negated_conjecture,
r1(X32,sK20(X32)) ).
cnf(u195,negated_conjecture,
sP0(sK19(X25)) ).
cnf(u210,negated_conjecture,
r1(X25,sK19(X25)) ).
cnf(u233,negated_conjecture,
r1(X8,sK17(X8)) ).
cnf(u261,negated_conjecture,
r1(X261,sK43(X261)) ).
cnf(u312,negated_conjecture,
r1(X292,sK46(X292)) ).
cnf(u366,negated_conjecture,
r1(X221,sK39(X221)) ).
cnf(u424,negated_conjecture,
r1(X171,sK34(X171)) ).
cnf(u486,negated_conjecture,
r1(X111,sK28(X111)) ).
cnf(u552,negated_conjecture,
r1(X41,sK21(X41)) ).
cnf(u622,negated_conjecture,
sP1(sK18(X17)) ).
cnf(u677,negated_conjecture,
r1(X17,sK18(X17)) ).
cnf(u718,negated_conjecture,
r1(X230,sK40(X230)) ).
cnf(u798,negated_conjecture,
r1(X271,sK44(X271)) ).
cnf(u881,negated_conjecture,
r1(X180,sK35(X180)) ).
cnf(u968,negated_conjecture,
r1(X120,sK29(X120)) ).
cnf(u1059,negated_conjecture,
r1(X50,sK22(X50)) ).
cnf(u1151,axiom,
r1(X0,X2) ).
cnf(u1178,negated_conjecture,
r1(X0,sK17(X1)) ).
cnf(u1227,negated_conjecture,
r1(X0,sK18(X1)) ).
cnf(u1276,negated_conjecture,
r1(X0,sK19(X1)) ).
cnf(u1325,negated_conjecture,
r1(X0,sK20(X1)) ).
cnf(u1374,negated_conjecture,
r1(X0,sK21(X1)) ).
cnf(u1423,negated_conjecture,
r1(X0,sK22(X1)) ).
cnf(u1472,negated_conjecture,
r1(X0,sK27(X1)) ).
cnf(u1521,negated_conjecture,
r1(X0,sK28(X1)) ).
cnf(u1570,negated_conjecture,
r1(X0,sK29(X1)) ).
cnf(u1619,negated_conjecture,
r1(X0,sK33(X1)) ).
cnf(u1668,negated_conjecture,
r1(X0,sK34(X1)) ).
cnf(u1717,negated_conjecture,
r1(X0,sK35(X1)) ).
cnf(u1766,negated_conjecture,
r1(X0,sK38(X1)) ).
cnf(u1815,negated_conjecture,
r1(X0,sK39(X1)) ).
cnf(u1864,negated_conjecture,
r1(X0,sK40(X1)) ).
cnf(u1913,negated_conjecture,
r1(X0,sK42(X1)) ).
cnf(u1962,negated_conjecture,
r1(X0,sK43(X1)) ).
cnf(u2011,negated_conjecture,
r1(X0,sK44(X1)) ).
cnf(u2060,negated_conjecture,
r1(X0,sK45(X1)) ).
cnf(u2109,negated_conjecture,
r1(X0,sK46(X1)) ).
cnf(u2158,negated_conjecture,
r1(X0,sK47(X1)) ).
cnf(u1154,negated_conjecture,
( r1(X0,sK18(X1))
| ~ r1(X0,X1) ) ).
cnf(u1157,negated_conjecture,
( r1(X0,sK21(X1))
| ~ r1(X0,X1) ) ).
cnf(u55,negated_conjecture,
( ~ r1(sK16,X210)
| ~ r1(X210,X211)
| ~ r1(X211,X212)
| r1(X212,sK38(X212)) ) ).
cnf(u1171,negated_conjecture,
( r1(X0,sK45(X1))
| ~ r1(X0,X1) ) ).
cnf(u24,axiom,
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| r1(X0,X2) ) ).
cnf(u68,negated_conjecture,
( ~ r1(sK16,X98)
| ~ r1(X98,X99)
| ~ r1(X99,X100)
| ~ r1(X100,X101)
| ~ r1(X101,X102)
| r1(X102,sK27(X102)) ) ).
cnf(u1156,negated_conjecture,
( r1(X0,sK20(X1))
| ~ r1(X0,X1) ) ).
cnf(u1160,negated_conjecture,
( r1(X0,sK28(X1))
| ~ r1(X0,X1) ) ).
cnf(u1162,negated_conjecture,
( r1(X0,sK33(X1))
| ~ r1(X0,X1) ) ).
cnf(u1155,negated_conjecture,
( r1(X0,sK19(X1))
| ~ r1(X0,X1) ) ).
cnf(u1153,negated_conjecture,
( r1(X0,sK17(X1))
| ~ r1(X0,X1) ) ).
cnf(u76,negated_conjecture,
( ~ r1(sK16,X27)
| ~ r1(X27,X28)
| ~ r1(X28,X29)
| ~ r1(X29,X30)
| ~ r1(X30,X31)
| ~ r1(X31,X32)
| r1(X32,sK20(X32)) ) ).
cnf(u60,negated_conjecture,
( ~ r1(sK33(X162),X164)
| ~ r1(X159,X160)
| ~ r1(X160,X161)
| ~ r1(X161,X162)
| ~ r1(sK16,X159)
| ~ r1(X164,X165)
| ~ r1(X165,X166)
| ~ r1(X166,X167)
| ~ r1(X167,X168)
| ~ r1(X168,X169)
| ~ r1(X169,X170)
| ~ r1(X170,X171)
| r1(X171,sK34(X171)) ) ).
cnf(u1164,negated_conjecture,
( r1(X0,sK35(X1))
| ~ r1(X0,X1) ) ).
cnf(u59,negated_conjecture,
( ~ r1(sK34(X171),X173)
| ~ r1(X159,X160)
| ~ r1(X160,X161)
| ~ r1(X161,X162)
| ~ r1(sK33(X162),X164)
| ~ r1(X164,X165)
| ~ r1(X165,X166)
| ~ r1(X166,X167)
| ~ r1(X167,X168)
| ~ r1(X168,X169)
| ~ r1(X169,X170)
| ~ r1(X170,X171)
| ~ r1(sK16,X159)
| ~ r1(X173,X174)
| ~ r1(X174,X175)
| ~ r1(X175,X176)
| ~ r1(X176,X177)
| ~ r1(X177,X178)
| ~ r1(X178,X179)
| ~ r1(X179,X180)
| r1(X180,sK35(X180)) ) ).
cnf(u1169,negated_conjecture,
( r1(X0,sK43(X1))
| ~ r1(X0,X1) ) ).
cnf(u1159,negated_conjecture,
( r1(X0,sK27(X1))
| ~ r1(X0,X1) ) ).
cnf(u67,negated_conjecture,
( ~ r1(sK27(X102),X104)
| ~ r1(X98,X99)
| ~ r1(X99,X100)
| ~ r1(X100,X101)
| ~ r1(X101,X102)
| ~ r1(sK16,X98)
| ~ r1(X104,X105)
| ~ r1(X105,X106)
| ~ r1(X106,X107)
| ~ r1(X107,X108)
| ~ r1(X108,X109)
| ~ r1(X109,X110)
| ~ r1(X110,X111)
| r1(X111,sK28(X111)) ) ).
cnf(u41,negated_conjecture,
~ p1(sK16) ).
cnf(u83,negated_conjecture,
( r1(X303,sK47(X303))
| ~ r1(sK16,X303) ) ).
cnf(u1161,negated_conjecture,
( r1(X0,sK29(X1))
| ~ r1(X0,X1) ) ).
cnf(u75,negated_conjecture,
( ~ r1(sK20(X32),X34)
| ~ r1(X27,X28)
| ~ r1(X28,X29)
| ~ r1(X29,X30)
| ~ r1(X30,X31)
| ~ r1(X31,X32)
| ~ r1(sK16,X27)
| ~ r1(X34,X35)
| ~ r1(X35,X36)
| ~ r1(X36,X37)
| ~ r1(X37,X38)
| ~ r1(X38,X39)
| ~ r1(X39,X40)
| ~ r1(X40,X41)
| r1(X41,sK21(X41)) ) ).
cnf(u49,negated_conjecture,
( ~ r1(sK42(X252),X254)
| ~ r1(X251,X252)
| ~ r1(sK16,X251)
| ~ r1(X254,X255)
| ~ r1(X255,X256)
| ~ r1(X256,X257)
| ~ r1(X257,X258)
| ~ r1(X258,X259)
| ~ r1(X259,X260)
| ~ r1(X260,X261)
| r1(X261,sK43(X261)) ) ).
cnf(u306,negated_conjecture,
( ~ r1(sK45(X282),X284)
| ~ r1(sK16,X282)
| ~ r1(X284,X285)
| ~ r1(X285,X286)
| ~ r1(X286,X287)
| ~ r1(X287,X288)
| ~ r1(X288,X289)
| ~ r1(X289,X290)
| ~ r1(X290,X291)
| ~ r1(X291,X292)
| r1(X292,sK46(X292)) ) ).
cnf(u1163,negated_conjecture,
( r1(X0,sK34(X1))
| ~ r1(X0,X1) ) ).
cnf(u54,negated_conjecture,
( ~ r1(sK38(X212),X214)
| ~ r1(X210,X211)
| ~ r1(X211,X212)
| ~ r1(sK16,X210)
| ~ r1(X214,X215)
| ~ r1(X215,X216)
| ~ r1(X216,X217)
| ~ r1(X217,X218)
| ~ r1(X218,X219)
| ~ r1(X219,X220)
| ~ r1(X220,X221)
| r1(X221,sK39(X221)) ) ).
cnf(u1158,negated_conjecture,
( r1(X0,sK22(X1))
| ~ r1(X0,X1) ) ).
cnf(u1174,negated_conjecture,
( r1(X0,sK47(X1))
| ~ r1(X0,X1) ) ).
cnf(u78,negated_conjecture,
( ~ r1(sK16,X19)
| ~ r1(X19,X20)
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| ~ r1(X23,X24)
| ~ r1(X24,X25)
| r1(X25,sK19(X25)) ) ).
cnf(u80,negated_conjecture,
( ~ r1(sK17(X8),X10)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(sK16,X1)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| ~ r1(X14,X15)
| ~ r1(X15,X16)
| ~ r1(X16,X17)
| r1(X17,sK18(X17)) ) ).
cnf(u1166,negated_conjecture,
( r1(X0,sK39(X1))
| ~ r1(X0,X1) ) ).
cnf(u23,axiom,
r1(X0,X0) ).
cnf(u79,negated_conjecture,
( ~ r1(sK17(X8),X10)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(sK16,X1)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| ~ r1(X14,X15)
| ~ r1(X15,X16)
| ~ r1(X16,X17)
| sP1(sK18(X17)) ) ).
cnf(u53,negated_conjecture,
( ~ r1(sK39(X221),X223)
| ~ r1(X210,X211)
| ~ r1(X211,X212)
| ~ r1(sK38(X212),X214)
| ~ r1(X214,X215)
| ~ r1(X215,X216)
| ~ r1(X216,X217)
| ~ r1(X217,X218)
| ~ r1(X218,X219)
| ~ r1(X219,X220)
| ~ r1(X220,X221)
| ~ r1(sK16,X210)
| ~ r1(X223,X224)
| ~ r1(X224,X225)
| ~ r1(X225,X226)
| ~ r1(X226,X227)
| ~ r1(X227,X228)
| ~ r1(X228,X229)
| ~ r1(X229,X230)
| r1(X230,sK40(X230)) ) ).
cnf(u81,negated_conjecture,
( ~ r1(sK16,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| r1(X8,sK17(X8)) ) ).
cnf(u1173,negated_conjecture,
( r1(X0,sK46(X1))
| ~ r1(X0,X1) ) ).
cnf(u77,negated_conjecture,
( ~ r1(sK16,X19)
| ~ r1(X19,X20)
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| ~ r1(X23,X24)
| ~ r1(X24,X25)
| sP0(sK19(X25)) ) ).
cnf(u1170,negated_conjecture,
( r1(X0,sK44(X1))
| ~ r1(X0,X1) ) ).
cnf(u61,negated_conjecture,
( ~ r1(sK16,X159)
| ~ r1(X159,X160)
| ~ r1(X160,X161)
| ~ r1(X161,X162)
| r1(X162,sK33(X162)) ) ).
cnf(u1165,negated_conjecture,
( r1(X0,sK38(X1))
| ~ r1(X0,X1) ) ).
cnf(u66,negated_conjecture,
( ~ r1(sK28(X111),X113)
| ~ r1(X98,X99)
| ~ r1(X99,X100)
| ~ r1(X100,X101)
| ~ r1(X101,X102)
| ~ r1(sK27(X102),X104)
| ~ r1(X104,X105)
| ~ r1(X105,X106)
| ~ r1(X106,X107)
| ~ r1(X107,X108)
| ~ r1(X108,X109)
| ~ r1(X109,X110)
| ~ r1(X110,X111)
| ~ r1(sK16,X98)
| ~ r1(X113,X114)
| ~ r1(X114,X115)
| ~ r1(X115,X116)
| ~ r1(X116,X117)
| ~ r1(X117,X118)
| ~ r1(X118,X119)
| ~ r1(X119,X120)
| r1(X120,sK29(X120)) ) ).
cnf(u50,negated_conjecture,
( ~ r1(sK16,X251)
| ~ r1(X251,X252)
| r1(X252,sK42(X252)) ) ).
cnf(u1168,negated_conjecture,
( r1(X0,sK42(X1))
| ~ r1(X0,X1) ) ).
cnf(u82,negated_conjecture,
( ~ r1(sK47(X303),X305)
| ~ r1(sK16,X303)
| ~ r1(X305,X306)
| ~ r1(X306,X307)
| ~ r1(X307,X308)
| ~ r1(X308,X309)
| ~ r1(X309,X310)
| ~ r1(X310,X311)
| ~ r1(X311,X312)
| ~ r1(X312,X313)
| ~ p1(X313) ) ).
cnf(u792,negated_conjecture,
( ~ r1(sK43(X261),X263)
| ~ r1(X251,X252)
| ~ r1(sK42(X252),X254)
| ~ r1(X254,X255)
| ~ r1(X255,X256)
| ~ r1(X256,X257)
| ~ r1(X257,X258)
| ~ r1(X258,X259)
| ~ r1(X259,X260)
| ~ r1(X260,X261)
| ~ r1(sK16,X251)
| ~ r1(X263,X264)
| ~ r1(X264,X265)
| ~ r1(X265,X266)
| ~ r1(X266,X267)
| ~ r1(X267,X268)
| ~ r1(X268,X269)
| ~ r1(X269,X270)
| ~ r1(X270,X271)
| r1(X271,sK44(X271)) ) ).
cnf(u1167,negated_conjecture,
( r1(X0,sK40(X1))
| ~ r1(X0,X1) ) ).
cnf(u46,negated_conjecture,
( r1(X282,sK45(X282))
| ~ r1(sK16,X282) ) ).
cnf(u74,negated_conjecture,
( ~ r1(sK21(X41),X43)
| ~ r1(X27,X28)
| ~ r1(X28,X29)
| ~ r1(X29,X30)
| ~ r1(X30,X31)
| ~ r1(X31,X32)
| ~ r1(sK20(X32),X34)
| ~ r1(X34,X35)
| ~ r1(X35,X36)
| ~ r1(X36,X37)
| ~ r1(X37,X38)
| ~ r1(X38,X39)
| ~ r1(X39,X40)
| ~ r1(X40,X41)
| ~ r1(sK16,X27)
| ~ r1(X43,X44)
| ~ r1(X44,X45)
| ~ r1(X45,X46)
| ~ r1(X46,X47)
| ~ r1(X47,X48)
| ~ r1(X48,X49)
| ~ r1(X49,X50)
| r1(X50,sK22(X50)) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL681+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.42 % Computer : n010.cluster.edu
% 0.11/0.42 % Model : x86_64 x86_64
% 0.11/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.42 % Memory : 8046.5625MB
% 0.11/0.42 % OS : Linux 6.8.0-71-generic
% 0.11/0.42 % CPULimit : 300
% 0.11/0.42 % WCLimit : 300
% 0.11/0.42 % DateTime : Sun Sep 27 16:36:54 UTC 2026
% 0.11/0.42 % CPUTime :
% 0.11/0.42 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.45 Running first-order model finding
% 0.11/0.45 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.59/0.57 % (1152601)Will run a generic schedule for satisfiability detection.
% 0.59/0.57 % (1152608)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2643563709:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.59/0.57 % (1152607)% WARNING: option uhcvi not known.
% 0.59/0.57 % (1152606)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3545777249_2999 on theBenchmark for (2999ds/0Mi)
% 0.59/0.57 % (1152607)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1079503452:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.59/0.57 % (1152612)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=501467464:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.59/0.57 % (1152609)dis+10_1_sil=32000:sp=arity:random_seed=4135195100:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.59/0.57 % (1152610)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2793794855:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.59/0.57 % (1152611)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=312091849:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.59/0.57 % (1152609)Instruction limit reached!
% 0.59/0.57 % (1152609)------------------------------
% 0.59/0.57 % (1152609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.59/0.57 % (1152609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.59/0.57 % (1152609)CaDiCaL version: 2.1.3
% 0.59/0.57 % (1152609)Termination reason: Instruction limit
% 0.59/0.57 % (1152609)Termination phase: Saturation
% 0.59/0.57 % (1152609)Time elapsed: 0.044 s
% 0.59/0.57 % (1152609)Peak memory usage: 12 MB
% 0.59/0.57 % (1152609)Instructions burned: 103 (million)
% 0.59/0.57 % (1152611)Instruction limit reached!
% 0.59/0.57 % (1152611)------------------------------
% 0.59/0.57 % (1152611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.59/0.57 % (1152611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.59/0.57 % (1152611)CaDiCaL version: 2.1.3
% 0.59/0.57 % (1152611)Termination reason: Instruction limit
% 0.59/0.57 % (1152611)Termination phase: Saturation
% 0.59/0.57 % (1152611)Time elapsed: 0.052 s
% 0.59/0.57 % (1152611)Peak memory usage: 13 MB
% 0.59/0.57 % (1152611)Instructions burned: 131 (million)
% 0.59/0.57 % (1152610)Instruction limit reached!
% 0.59/0.57 % (1152610)------------------------------
% 0.59/0.57 % (1152610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.59/0.57 % (1152610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.59/0.57 % (1152610)CaDiCaL version: 2.1.3
% 0.59/0.57 % (1152610)Termination reason: Instruction limit
% 0.59/0.57 % (1152610)Termination phase: Blocked clause elimination
% 0.59/0.57 % (1152610)Time elapsed: 0.057 s
% 0.59/0.57 % (1152610)Peak memory usage: 11 MB
% 0.59/0.57 % (1152610)Instructions burned: 116 (million)
% 0.59/0.57 % (1152620)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2414989066:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.59/0.57 % (1152608) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1152601-1152608"...
% 0.59/0.57 % (1152608)...printing done.
% 0.59/0.57 % SZS status CounterSatisfiable for theBenchmark
% 0.59/0.57 % SZS output start Saturation.
% See solution above
% 0.59/0.57 % SZS output start Definitions and Model Updates.
% 0.59/0.57 for all inputs,
% 0.59/0.57 define p2(X0) := $false
% 0.59/0.57 % SZS output end Definitions and Model Updates.
% 0.59/0.57 % (1152608)------------------------------
% 0.59/0.57 % (1152608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.59/0.57 % (1152608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.59/0.57 % (1152608)CaDiCaL version: 2.1.3
% 0.59/0.57 % (1152608)Termination reason: Satisfiable
% 0.59/0.57 % (1152608)Time elapsed: 0.076 s
% 0.59/0.57 % (1152608)Peak memory usage: 14 MB
% 0.59/0.57 % (1152608)Instructions burned: 350 (million)
% 0.59/0.57 % (1152601)Success in time 0.113 s
% 0.59/0.57 % Vampire exiting
%------------------------------------------------------------------------------