%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO582+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n015.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:31:43 PM UTC 2026
% Result : CounterSatisfiable 0.33s 0.42s
% Output : Saturation 0.33s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u164,negated_conjecture,
( ~ k04_buttercup10225(X4)
| b48_buttercup10519(X4) ) ).
cnf(u181,negated_conjecture,
~ k04_buttercup10225(sK30) ).
cnf(u186,negated_conjecture,
b48_buttercup10519(sK30) ).
cnf(u192,axiom,
k04_buttercup10419(sK10) ).
cnf(u195,axiom,
~ b48_buttercup10421(sK10) ).
cnf(u248,negated_conjecture,
b48_buttercup10417(sK14) ).
cnf(u102,axiom,
~ b48_buttercup10227(sK1) ).
cnf(u130,axiom,
b48_buttercup10417(sK13) ).
cnf(u104,axiom,
( ~ b48_buttercup10227(X0)
| k04_buttercup10225(X0) ) ).
cnf(u148,axiom,
b48_buttercup10228(sK26) ).
cnf(u114,axiom,
~ k04_buttercup10516(sK6) ).
cnf(u262,axiom,
k04_buttercup10516(sK20) ).
cnf(u264,axiom,
b48_buttercup10417(sK18) ).
cnf(u228,negated_conjecture,
k04_buttercup10516(sK1) ).
cnf(u205,negated_conjecture,
b48_buttercup10519(sK14) ).
cnf(u254,negated_conjecture,
b48_buttercup10519(sK22) ).
cnf(u215,axiom,
b48_buttercup10515(sK18) ).
cnf(u128,axiom,
( ~ k04_buttercup10517(X0)
| b48_buttercup10421(X0) ) ).
cnf(u110,axiom,
~ b48_buttercup10222(sK4) ).
cnf(u138,axiom,
k04_buttercup10516(sK16) ).
cnf(u112,axiom,
b48_buttercup10222(sK3) ).
cnf(u255,negated_conjecture,
b48_buttercup10515(sK22) ).
cnf(u122,axiom,
( ~ b48_buttercup10515(X0)
| k04_buttercup10516(X0) ) ).
cnf(u103,axiom,
k04_buttercup10225(sK1) ).
cnf(u219,axiom,
b48_buttercup10222(sK26) ).
cnf(u212,negated_conjecture,
b48_buttercup10515(sK30) ).
cnf(u129,axiom,
( ~ b48_buttercup10421(X0)
| k04_buttercup10517(X0) ) ).
cnf(u111,axiom,
k04_buttercup10419(sK4) ).
cnf(u93,axiom,
( ~ b48_buttercup10521(X0)
| b48_buttercup10515(X0) ) ).
cnf(u209,negated_conjecture,
b48_buttercup10515(sK7) ).
cnf(u113,axiom,
k04_buttercup10419(sK3) ).
cnf(u245,axiom,
k04_buttercup10517(sK20) ).
cnf(u227,axiom,
k04_buttercup10225(sK22) ).
cnf(u235,axiom,
k04_buttercup10516(sK29) ).
cnf(u91,axiom,
( ~ b48_buttercup10519(X0)
| b48_buttercup10515(X0) ) ).
cnf(u135,axiom,
k04_buttercup10419(sK11) ).
cnf(u109,axiom,
~ k04_buttercup10419(sK5) ).
cnf(u137,axiom,
k04_buttercup10517(sK15) ).
cnf(u119,axiom,
( ~ b48_buttercup10229(X0)
| k04_buttercup10225(X0) ) ).
cnf(u147,axiom,
b48_buttercup10515(sK25) ).
cnf(u121,axiom,
k04_buttercup10516(sK8) ).
cnf(u242,negated_conjecture,
b48_buttercup10222(sK32) ).
cnf(u203,negated_conjecture,
b48_buttercup10519(sK1) ).
cnf(u132,axiom,
~ b48_buttercup10417(sK12) ).
cnf(u105,axiom,
~ b48_buttercup10228(sK2) ).
cnf(u98,axiom,
( ~ b48_buttercup10229(X0)
| b48_buttercup10222(X0) ) ).
cnf(u263,negated_conjecture,
b48_buttercup10417(sK22) ).
cnf(u90,axiom,
( ~ b48_buttercup10518(X0)
| b48_buttercup10515(X0) ) ).
cnf(u265,axiom,
b48_buttercup10417(sK27) ).
cnf(u230,negated_conjecture,
k04_buttercup10516(sK14) ).
cnf(u232,axiom,
k04_buttercup10516(sK25) ).
cnf(u238,negated_conjecture,
b48_buttercup10417(sK30) ).
cnf(u217,axiom,
b48_buttercup10417(sK19) ).
cnf(u240,axiom,
b48_buttercup10222(sK7) ).
cnf(u94,axiom,
( ~ b48_buttercup10421(X0)
| b48_buttercup10417(X0) ) ).
cnf(u250,negated_conjecture,
b48_buttercup10519(sK21) ).
cnf(u96,axiom,
( ~ b48_buttercup10227(X0)
| b48_buttercup10222(X0) ) ).
cnf(u140,axiom,
b48_buttercup10521(sK18) ).
cnf(u106,axiom,
k04_buttercup10419(sK2) ).
cnf(u150,axiom,
b48_buttercup10518(sK28) ).
cnf(u124,axiom,
b48_buttercup10222(sK9) ).
cnf(u152,negated_conjecture,
k04_buttercup10225(sK32) ).
cnf(u241,axiom,
b48_buttercup10222(sK14) ).
cnf(u95,axiom,
( ~ b48_buttercup10422(X0)
| b48_buttercup10417(X0) ) ).
cnf(u97,axiom,
( ~ b48_buttercup10228(X0)
| b48_buttercup10222(X0) ) ).
cnf(u99,axiom,
~ b48_buttercup10422(sK0) ).
cnf(u125,axiom,
( ~ k04_buttercup10225(X0)
| b48_buttercup10222(X0) ) ).
cnf(u256,axiom,
b48_buttercup10417(sK25) ).
cnf(u266,axiom,
b48_buttercup10417(sK28) ).
cnf(u220,axiom,
b48_buttercup10222(sK22) ).
cnf(u237,negated_conjecture,
k04_buttercup10516(sK32) ).
cnf(u239,axiom,
b48_buttercup10222(sK1) ).
cnf(u247,negated_conjecture,
b48_buttercup10417(sK7) ).
cnf(u107,axiom,
( ~ b48_buttercup10228(X0)
| k04_buttercup10419(X0) ) ).
cnf(u204,negated_conjecture,
b48_buttercup10519(sK7) ).
cnf(u214,axiom,
b48_buttercup10515(sK29) ).
cnf(u131,axiom,
~ k04_buttercup10419(sK13) ).
cnf(u216,axiom,
b48_buttercup10417(sK20) ).
cnf(u149,axiom,
b48_buttercup10519(sK27) ).
cnf(u115,axiom,
b48_buttercup10417(sK6) ).
cnf(u244,negated_conjecture,
b48_buttercup10417(sK32) ).
cnf(u229,negated_conjecture,
k04_buttercup10516(sK7) ).
cnf(u260,negated_conjecture,
b48_buttercup10417(sK21) ).
cnf(u92,axiom,
( ~ b48_buttercup10520(X0)
| b48_buttercup10515(X0) ) ).
cnf(u222,axiom,
k04_buttercup10225(sK21) ).
cnf(u139,axiom,
k04_buttercup10419(sK17) ).
cnf(u257,negated_conjecture,
k04_buttercup10516(sK22) ).
cnf(u224,axiom,
b48_buttercup10417(sK8) ).
cnf(u226,axiom,
b48_buttercup10417(sK15) ).
cnf(u123,axiom,
~ k04_buttercup10225(sK9) ).
cnf(u267,axiom,
b48_buttercup10417(sK29) ).
cnf(u252,negated_conjecture,
k04_buttercup10516(sK21) ).
cnf(u213,negated_conjecture,
b48_buttercup10515(sK32) ).
cnf(u134,axiom,
b48_buttercup10417(sK11) ).
cnf(u108,axiom,
b48_buttercup10222(sK5) ).
cnf(u136,axiom,
k04_buttercup10225(sK14) ).
cnf(u118,axiom,
k04_buttercup10225(sK7) ).
cnf(u146,axiom,
b48_buttercup10222(sK24) ).
cnf(u120,axiom,
~ b48_buttercup10515(sK8) ).
cnf(u234,axiom,
k04_buttercup10516(sK28) ).
cnf(u101,axiom,
( ~ b48_buttercup10422(X0)
| k04_buttercup10419(X0) ) ).
cnf(u221,axiom,
k04_buttercup10419(sK19) ).
cnf(u142,axiom,
b48_buttercup10421(sK20) ).
cnf(u116,axiom,
( ~ k04_buttercup10516(X0)
| b48_buttercup10417(X0) ) ).
cnf(u144,axiom,
b48_buttercup10229(sK22) ).
cnf(u223,axiom,
k04_buttercup10419(sK26) ).
cnf(u225,axiom,
b48_buttercup10417(sK16) ).
cnf(u243,axiom,
b48_buttercup10421(sK15) ).
cnf(u89,axiom,
( ~ k04_buttercup10517(X0)
| k04_buttercup10516(X0) ) ).
cnf(u133,axiom,
k04_buttercup10419(sK12) ).
cnf(u210,negated_conjecture,
b48_buttercup10515(sK14) ).
cnf(u143,axiom,
b48_buttercup10227(sK21) ).
cnf(u117,axiom,
~ b48_buttercup10229(sK7) ).
cnf(u145,axiom,
b48_buttercup10417(sK23) ).
cnf(u211,axiom,
b48_buttercup10515(sK27) ).
cnf(u231,axiom,
k04_buttercup10516(sK18) ).
cnf(u233,axiom,
k04_buttercup10516(sK27) ).
cnf(u100,axiom,
k04_buttercup10419(sK0) ).
cnf(u206,axiom,
k04_buttercup10516(sK15) ).
cnf(u251,negated_conjecture,
b48_buttercup10515(sK21) ).
cnf(u208,negated_conjecture,
b48_buttercup10515(sK1) ).
cnf(u141,axiom,
b48_buttercup10422(sK19) ).
cnf(u218,axiom,
b48_buttercup10222(sK21) ).
cnf(u151,axiom,
b48_buttercup10520(sK29) ).
cnf(u236,negated_conjecture,
k04_buttercup10516(sK30) ).
cnf(u153,negated_conjecture,
b48_buttercup10519(sK32) ).
cnf(u246,negated_conjecture,
b48_buttercup10417(sK1) ).
cnf(u207,axiom,
b48_buttercup10515(sK28) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SYO582+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.30 % Computer : n015.cluster.edu
% 0.11/0.30 % Model : x86_64 x86_64
% 0.11/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.30 % Memory : 8046.5625MB
% 0.11/0.30 % OS : Linux 6.8.0-71-generic
% 0.11/0.30 % CPULimit : 300
% 0.11/0.30 % WCLimit : 300
% 0.11/0.30 % DateTime : Mon Sep 28 17:52:32 UTC 2026
% 0.11/0.31 % CPUTime :
% 0.11/0.31 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.29/0.36 Running first-order model finding
% 0.29/0.36 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.33/0.42 % (2847402)Will run a generic schedule for satisfiability detection.
% 0.33/0.42 % (2847412)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2145878420:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.33/0.42 % (2847412) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2847402-2847412"...
% 0.33/0.42 % (2847412)...printing done.
% 0.33/0.42 % SZS status CounterSatisfiable for theBenchmark
% 0.33/0.42 % SZS output start Saturation.
% See solution above
% 0.33/0.43 % SZS output start Definitions and Model Updates.
% 0.33/0.43 % SZS output end Definitions and Model Updates.
% 0.33/0.43 % (2847412)------------------------------
% 0.33/0.43 % (2847412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.33/0.43 % (2847412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.33/0.43 % (2847412)CaDiCaL version: 2.1.3
% 0.33/0.43 % (2847412)Termination reason: Satisfiable
% 0.33/0.43 % (2847412)Time elapsed: 0.004 s
% 0.33/0.43 % (2847412)Peak memory usage: 11 MB
% 0.33/0.43 % (2847412)Instructions burned: 3 (million)
% 0.33/0.43 % (2847402)Success in time 0.044 s
% 0.33/0.43 % Vampire exiting
%------------------------------------------------------------------------------