%------------------------------------------------------------------------------
% 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/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n020.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 : CounterSatisfiable 0.07s 0.25s
% Output : Saturation 0.07s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u312,negated_conjecture,
~ sP1 ).
cnf(u316,negated_conjecture,
sP0 ).
cnf(u321,negated_conjecture,
c4_1(a678) ).
cnf(u326,negated_conjecture,
~ c2_1(a678) ).
cnf(u331,negated_conjecture,
ndr1_0 ).
cnf(u336,negated_conjecture,
~ c4_1(a676) ).
cnf(u340,negated_conjecture,
c5_0 ).
cnf(u343,negated_conjecture,
c2_0 ).
cnf(u348,negated_conjecture,
~ c3_1(a676) ).
cnf(u354,negated_conjecture,
~ c3_2(a676,a677) ).
cnf(u359,negated_conjecture,
~ c2_2(a676,a677) ).
cnf(u364,negated_conjecture,
c4_2(a676,a677) ).
cnf(u369,negated_conjecture,
~ ndr1_1(a676) ).
cnf(u378,negated_conjecture,
~ c5_1(a675) ).
cnf(u382,negated_conjecture,
~ c3_1(a675) ).
cnf(u388,negated_conjecture,
c2_1(a674) ).
cnf(u393,negated_conjecture,
~ c4_1(a674) ).
cnf(u398,negated_conjecture,
~ sP2 ).
cnf(u403,negated_conjecture,
~ c1_1(a672) ).
cnf(u406,negated_conjecture,
c4_0 ).
cnf(u412,negated_conjecture,
ndr1_1(a672) ).
cnf(u420,negated_conjecture,
c5_1(a672) ).
cnf(u426,negated_conjecture,
~ c2_2(a669,a670) ).
cnf(u430,negated_conjecture,
~ c1_2(a669,a670) ).
cnf(u436,negated_conjecture,
~ c5_2(a669,a670) ).
cnf(u441,negated_conjecture,
~ ndr1_1(a669) ).
cnf(u446,negated_conjecture,
~ c1_1(a669) ).
cnf(u455,negated_conjecture,
~ sP3 ).
cnf(u459,negated_conjecture,
~ ndr1_1(a666) ).
cnf(u467,negated_conjecture,
~ c3_1(a666) ).
cnf(u473,negated_conjecture,
~ c1_1(a666) ).
cnf(u478,negated_conjecture,
~ ndr1_1(a665) ).
cnf(u486,negated_conjecture,
~ c3_1(a665) ).
cnf(u491,negated_conjecture,
~ c5_1(a665) ).
cnf(u497,negated_conjecture,
sP4 ).
cnf(u503,negated_conjecture,
c2_1(a659) ).
cnf(u508,negated_conjecture,
~ c1_1(a659) ).
cnf(u512,negated_conjecture,
~ ndr1_1(a659) ).
cnf(u516,negated_conjecture,
( ~ c1_2(a659,X24)
| ~ c3_2(a659,X24)
| c5_2(a659,X24) ) ).
cnf(u521,negated_conjecture,
~ c3_0 ).
cnf(u525,negated_conjecture,
( c5_2(X22,a658)
| ndr1_1(X22)
| c1_2(X22,X23)
| ~ c2_2(X22,X23)
| c5_2(X22,X23)
| ~ c4_1(X22) ) ).
cnf(u528,negated_conjecture,
sP5 ).
cnf(u533,negated_conjecture,
( ~ c4_2(X22,a658)
| ndr1_1(X22)
| c1_2(X22,X23)
| ~ c2_2(X22,X23)
| c5_2(X22,X23)
| ~ c4_1(X22) ) ).
cnf(u537,negated_conjecture,
( ~ c3_2(X21,a656)
| ~ c5_1(X21)
| ~ c2_1(X21) ) ).
cnf(u541,negated_conjecture,
( ~ c1_2(X21,a656)
| ~ c5_1(X21)
| ~ c2_1(X21) ) ).
cnf(u545,negated_conjecture,
( ~ c2_2(X21,a656)
| ~ c5_1(X21)
| ~ c2_1(X21) ) ).
cnf(u549,negated_conjecture,
( ~ c2_1(X21)
| ~ ndr1_1(X21)
| ~ c5_1(X21) ) ).
cnf(u556,negated_conjecture,
c1_0 ).
cnf(u565,negated_conjecture,
c5_1(a654) ).
cnf(u570,negated_conjecture,
~ c1_1(a654) ).
cnf(u575,negated_conjecture,
c3_2(a654,a655) ).
cnf(u580,negated_conjecture,
c4_2(a654,a655) ).
cnf(u585,negated_conjecture,
c5_2(a654,a655) ).
cnf(u590,negated_conjecture,
~ ndr1_1(a654) ).
cnf(u595,negated_conjecture,
~ c1_1(a653) ).
cnf(u602,negated_conjecture,
~ c4_1(a653) ).
cnf(u607,negated_conjecture,
~ ndr1_1(a653) ).
cnf(u615,negated_conjecture,
~ ndr1_1(a651) ).
cnf(u624,negated_conjecture,
~ c2_2(a651,a652) ).
cnf(u628,negated_conjecture,
~ c1_2(a651,a652) ).
cnf(u634,negated_conjecture,
~ c5_2(a651,a652) ).
cnf(u640,negated_conjecture,
( sP6(X13)
| c4_1(X13)
| ~ c5_2(X13,a649) ) ).
cnf(u644,negated_conjecture,
( sP6(X13)
| c4_1(X13)
| c1_2(X13,a649) ) ).
cnf(u648,negated_conjecture,
( sP6(X13)
| c4_1(X13)
| ~ c4_2(X13,a649) ) ).
cnf(u652,negated_conjecture,
( sP6(X13)
| c4_1(X13)
| ~ ndr1_1(X13) ) ).
cnf(u657,negated_conjecture,
ndr1_1(a648) ).
cnf(u672,negated_conjecture,
~ c3_1(a648) ).
cnf(u676,negated_conjecture,
( ~ c1_2(X7,a647)
| ~ c2_1(X7)
| c1_1(X7) ) ).
cnf(u680,negated_conjecture,
( ~ c2_2(X7,a647)
| ~ c2_1(X7)
| c1_1(X7) ) ).
cnf(u684,negated_conjecture,
( c5_2(X7,a647)
| ~ c2_1(X7)
| c1_1(X7) ) ).
cnf(u688,negated_conjecture,
( ~ c2_1(X7)
| ~ ndr1_1(X7)
| c1_1(X7) ) ).
cnf(u709,axiom,
~ c5_1(a679) ).
cnf(u714,axiom,
~ ndr1_1(a679) ).
cnf(u722,axiom,
~ c4_1(a679) ).
cnf(u729,axiom,
~ c3_1(a680) ).
cnf(u733,axiom,
~ ndr1_1(a680) ).
cnf(u759,axiom,
~ c1_2(a667,a668) ).
cnf(u763,axiom,
~ c4_2(a667,a668) ).
cnf(u769,axiom,
~ ndr1_1(a667) ).
cnf(u773,axiom,
~ c4_1(a667) ).
cnf(u780,axiom,
~ c2_2(a660,a662) ).
cnf(u785,axiom,
~ c5_2(a660,a662) ).
cnf(u789,axiom,
~ c4_2(a660,a662) ).
cnf(u795,axiom,
~ ndr1_1(a660) ).
cnf(u800,axiom,
~ c3_2(a660,a661) ).
cnf(u804,axiom,
~ c2_2(a660,a661) ).
cnf(u809,axiom,
~ c4_2(a660,a661) ).
cnf(u815,axiom,
~ c4_1(a660) ).
cnf(u838,axiom,
~ sP7 ).
cnf(u842,axiom,
~ c2_1(a645) ).
cnf(u847,axiom,
~ c5_2(a645,a646) ).
cnf(u851,axiom,
~ c2_2(a645,a646) ).
cnf(u856,axiom,
~ c3_2(a645,a646) ).
cnf(u862,axiom,
~ ndr1_1(a645) ).
cnf(u867,axiom,
~ c1_1(a645) ).
cnf(u879,negated_conjecture,
~ c5_1(a659) ).
cnf(u884,negated_conjecture,
~ c5_1(a674) ).
cnf(u888,negated_conjecture,
~ ndr1_1(a674) ).
cnf(u905,negated_conjecture,
~ c1_2(a654,a655) ).
cnf(u911,negated_conjecture,
~ c5_2(a676,a677) ).
cnf(u915,negated_conjecture,
~ c1_2(a676,a677) ).
cnf(u951,negated_conjecture,
~ c5_2(a667,a668) ).
cnf(u37,axiom,
( ~ c3_2(X0,a650)
| ~ sP6(X0) ) ).
cnf(u95,negated_conjecture,
~ c3_0 ).
cnf(u83,negated_conjecture,
c1_0 ).
cnf(u180,axiom,
( ~ c4_2(X0,a650)
| ~ sP6(X0) ) ).
cnf(u941,negated_conjecture,
( c4_1(X0)
| ~ ndr1_1(X0) ) ).
cnf(u179,axiom,
( ~ sP6(X0)
| ~ ndr1_1(X0) ) ).
cnf(u38,axiom,
( c5_2(X0,a650)
| ~ sP6(X0) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SYN537+1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.18 % Computer : n020.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 16:27:50 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.21 Running first-order model finding
% 0.07/0.21 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.07/0.25 % (286268)Will run a generic schedule for satisfiability detection.
% 0.07/0.25 % (286279)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2146646947:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.07/0.25 % (286274)% WARNING: option uhcvi not known.
% 0.07/0.25 % (286279) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-286268-286279"...
% 0.07/0.25 % (286279)...printing done.
% 0.07/0.25 % SZS status CounterSatisfiable for theBenchmark
% 0.07/0.25 % SZS output start Saturation.
% See solution above
% 0.07/0.25 % SZS output start Definitions and Model Updates.
% 0.07/0.25 globally flip the polarity of every occurrence of predicate "sP5"
% 0.07/0.25 globally flip the polarity of every occurrence of predicate "sP4"
% 0.07/0.25 globally flip the polarity of every occurrence of predicate "sP0"
% 0.07/0.25 globally flip the polarity of every occurrence of predicate "c4_1"
% 0.07/0.25 globally flip the polarity of every occurrence of predicate "c4_2"
% 0.07/0.25 globally flip the polarity of every occurrence of predicate "c4_0"
% 0.07/0.25 globally flip the polarity of every occurrence of predicate "c5_0"
% 0.07/0.25 globally flip the polarity of every occurrence of predicate "c5_1"
% 0.07/0.25 globally flip the polarity of every occurrence of predicate "ndr1_1"
% 0.07/0.25 % SZS output end Definitions and Model Updates.
% 0.07/0.25 % (286279)------------------------------
% 0.07/0.25 % (286279)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.07/0.25 % (286279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.07/0.25 % (286279)CaDiCaL version: 2.1.3
% 0.07/0.25 % (286279)Termination reason: Satisfiable
% 0.07/0.25 % (286279)Time elapsed: 0.004 s
% 0.07/0.25 % (286279)Peak memory usage: 12 MB
% 0.07/0.25 % (286279)Instructions burned: 9 (million)
% 0.07/0.25 % (286268)Success in time 0.022 s
% 0.07/0.25 % Vampire exiting
%------------------------------------------------------------------------------