%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV693-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n006.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 01:26:15 PM UTC 2026
% Result : Unsatisfiable 9.16s 3.63s
% Output : Refutation 9.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 47
% Syntax : Number of formulae : 104 ( 97 unt; 37 def)
% Number of atoms : 114 ( 97 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 22 ( 12 ~; 10 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 13 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 60 ( 60 usr; 43 con; 0-5 aty)
% Number of variables : 33 ( 33 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1404,axiom,
! [X2,X0,X1] :
( ~ class_Orderings_Olinorder(X0)
| c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X0),c_SetInterval_Oord__class_OgreaterThanLessThan(X1,X2,X0),tc_fun(X0,tc_bool)) = c_SetInterval_Oord__class_OatLeastLessThan(X1,X2,X0)
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,X0),X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ivl__disj__un_I3_J_0) ).
fof(f1405,plain,
! [X2,X0,X1] :
( ~ class_Orderings_Olinorder(X0)
| c_SetInterval_Oord__class_OatLeastLessThan(X1,X2,X0) = c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X0),c_SetInterval_Oord__class_OgreaterThanLessThan(X1,X2,X0),tc_fun(X0,tc_bool))
| ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,X0),X2)) ),
inference(reorient_equations,[],[f1404]) ).
fof(f1448,axiom,
! [X2,X3,X0,X1] : c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(X0,X1,X2),X3,tc_fun(X2,tc_bool)) = c_Set_Oinsert(X0,c_Lattices_Oupper__semilattice__class_Osup(X1,X3,tc_fun(X2,tc_bool)),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Un__insert__left_0) ).
fof(f1449,axiom,
! [X2,X3,X0,X1] : c_Lattices_Oupper__semilattice__class_Osup(X0,c_Set_Oinsert(X1,X2,X3),tc_fun(X3,tc_bool)) = c_Set_Oinsert(X1,c_Lattices_Oupper__semilattice__class_Osup(X0,X2,tc_fun(X3,tc_bool)),X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Un__insert__right_0) ).
fof(f1492,axiom,
! [X0,X1] :
( ~ class_Lattices_Obounded__lattice(X0)
| c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(X0),X1,X0) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_sup__bot__left_0) ).
fof(f1565,axiom,
! [X2,X0,X1] : c_Set_Oinsert(X0,X1,X2) = c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2),X1,tc_fun(X2,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_insert__is__Un_0) ).
fof(f1572,axiom,
hBOOL(hAPP(c_HOL_Oord__class_Oless(v_i,tc_nat),v_n)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_CHAINED_0) ).
fof(f1573,negated_conjecture,
hAPP(hAPP(c_Finite__Set_Osetsum(tc_nat,tc_Complex_Ocomplex),c_COMBS(hAPP(hAPP(c_COMBB(tc_Complex_Ocomplex,tc_fun(tc_Complex_Ocomplex,tc_Complex_Ocomplex),tc_nat),c_HOL_Otimes__class_Otimes(tc_Complex_Ocomplex)),hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_nat,tc_Complex_Ocomplex),tc_fun(tc_fun(tc_nat,tc_bool),tc_Complex_Ocomplex),tc_nat),c_Finite__Set_Osetsum(tc_nat,tc_Complex_Ocomplex)),hAPP(hAPP(c_COMBB(tc_Complex_Ocomplex,tc_fun(tc_nat,tc_Complex_Ocomplex),tc_nat),c_Power_Opower__class_Opower(tc_Complex_Ocomplex)),hAPP(hAPP(c_COMBB(tc_nat,tc_Complex_Ocomplex,tc_nat),hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n))),hAPP(c_COMBC(c_HOL_Ominus__class_Ominus(tc_nat),tc_nat,tc_nat,tc_nat),v_i)))),tc_nat,tc_fun(tc_nat,tc_bool),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),v_n,tc_nat))),v_a,tc_nat,tc_Complex_Ocomplex,tc_Complex_Ocomplex)),c_SetInterval_Oord__class_OatLeastLessThan(v_i,v_n,tc_nat)) != hAPP(hAPP(c_Finite__Set_Osetsum(tc_nat,tc_Complex_Ocomplex),c_COMBS(hAPP(hAPP(c_COMBB(tc_Complex_Ocomplex,tc_fun(tc_Complex_Ocomplex,tc_Complex_Ocomplex),tc_nat),c_HOL_Otimes__class_Otimes(tc_Complex_Ocomplex)),hAPP(c_COMBC(hAPP(hAPP(c_COMBB(tc_fun(tc_nat,tc_Complex_Ocomplex),tc_fun(tc_fun(tc_nat,tc_bool),tc_Complex_Ocomplex),tc_nat),c_Finite__Set_Osetsum(tc_nat,tc_Complex_Ocomplex)),hAPP(hAPP(c_COMBB(tc_Complex_Ocomplex,tc_fun(tc_nat,tc_Complex_Ocomplex),tc_nat),c_Power_Opower__class_Opower(tc_Complex_Ocomplex)),hAPP(hAPP(c_COMBB(tc_nat,tc_Complex_Ocomplex,tc_nat),hAPP(c_Power_Opower__class_Opower(tc_Complex_Ocomplex),c_FFT__Mirabelle_Oroot(v_n))),hAPP(c_COMBC(c_HOL_Ominus__class_Ominus(tc_nat),tc_nat,tc_nat,tc_nat),v_i)))),tc_nat,tc_fun(tc_nat,tc_bool),tc_Complex_Ocomplex),c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),v_n,tc_nat))),v_a,tc_nat,tc_Complex_Ocomplex,tc_Complex_Ocomplex)),c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(v_i,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),c_SetInterval_Oord__class_OgreaterThanLessThan(v_i,v_n,tc_nat),tc_fun(tc_nat,tc_bool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1578,axiom,
! [X0,X1] :
( class_Lattices_Obounded__lattice(tc_fun(X0,X1))
| ~ class_Lattices_Obounded__lattice(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_fun__Lattices_Obounded__lattice) ).
fof(f1617,axiom,
class_Orderings_Olinorder(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_nat__Orderings_Olinorder) ).
fof(f1627,axiom,
class_Lattices_Obounded__lattice(tc_bool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_bool__Lattices_Obounded__lattice) ).
fof(f1733,definition,
sF0 = c_Finite__Set_Osetsum(tc_nat,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f1734,plain,
c_Finite__Set_Osetsum(tc_nat,tc_Complex_Ocomplex) = sF0,
inference(reorient_equations,[],[f1733]) ).
fof(f1735,definition,
sF1 = tc_fun(tc_Complex_Ocomplex,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f1736,plain,
tc_fun(tc_Complex_Ocomplex,tc_Complex_Ocomplex) = sF1,
inference(reorient_equations,[],[f1735]) ).
fof(f1737,definition,
sF2 = c_COMBB(tc_Complex_Ocomplex,sF1,tc_nat),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f1738,plain,
c_COMBB(tc_Complex_Ocomplex,sF1,tc_nat) = sF2,
inference(reorient_equations,[],[f1737]) ).
fof(f1739,definition,
sF3 = c_HOL_Otimes__class_Otimes(tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f1740,plain,
c_HOL_Otimes__class_Otimes(tc_Complex_Ocomplex) = sF3,
inference(reorient_equations,[],[f1739]) ).
fof(f1741,definition,
sF4 = hAPP(sF2,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f1742,plain,
hAPP(sF2,sF3) = sF4,
inference(reorient_equations,[],[f1741]) ).
fof(f1743,definition,
sF5 = tc_fun(tc_nat,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f1744,plain,
tc_fun(tc_nat,tc_Complex_Ocomplex) = sF5,
inference(reorient_equations,[],[f1743]) ).
fof(f1745,definition,
sF6 = tc_fun(tc_nat,tc_bool),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f1746,plain,
tc_fun(tc_nat,tc_bool) = sF6,
inference(reorient_equations,[],[f1745]) ).
fof(f1747,definition,
sF7 = tc_fun(sF6,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f1748,plain,
tc_fun(sF6,tc_Complex_Ocomplex) = sF7,
inference(reorient_equations,[],[f1747]) ).
fof(f1749,definition,
sF8 = c_COMBB(sF5,sF7,tc_nat),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f1750,plain,
c_COMBB(sF5,sF7,tc_nat) = sF8,
inference(reorient_equations,[],[f1749]) ).
fof(f1751,definition,
sF9 = hAPP(sF8,sF0),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f1752,plain,
hAPP(sF8,sF0) = sF9,
inference(reorient_equations,[],[f1751]) ).
fof(f1753,definition,
sF10 = c_COMBB(tc_Complex_Ocomplex,sF5,tc_nat),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f1754,plain,
c_COMBB(tc_Complex_Ocomplex,sF5,tc_nat) = sF10,
inference(reorient_equations,[],[f1753]) ).
fof(f1755,definition,
sF11 = c_Power_Opower__class_Opower(tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f1756,plain,
c_Power_Opower__class_Opower(tc_Complex_Ocomplex) = sF11,
inference(reorient_equations,[],[f1755]) ).
fof(f1757,definition,
sF12 = hAPP(sF10,sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f1758,plain,
hAPP(sF10,sF11) = sF12,
inference(reorient_equations,[],[f1757]) ).
fof(f1759,definition,
sF13 = c_COMBB(tc_nat,tc_Complex_Ocomplex,tc_nat),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f1760,plain,
c_COMBB(tc_nat,tc_Complex_Ocomplex,tc_nat) = sF13,
inference(reorient_equations,[],[f1759]) ).
fof(f1761,definition,
sF14 = c_FFT__Mirabelle_Oroot(v_n),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f1762,plain,
c_FFT__Mirabelle_Oroot(v_n) = sF14,
inference(reorient_equations,[],[f1761]) ).
fof(f1763,definition,
sF15 = hAPP(sF11,sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f1764,plain,
hAPP(sF11,sF14) = sF15,
inference(reorient_equations,[],[f1763]) ).
fof(f1765,definition,
sF16 = hAPP(sF13,sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f1766,plain,
hAPP(sF13,sF15) = sF16,
inference(reorient_equations,[],[f1765]) ).
fof(f1767,definition,
sF17 = c_HOL_Ominus__class_Ominus(tc_nat),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f1768,plain,
c_HOL_Ominus__class_Ominus(tc_nat) = sF17,
inference(reorient_equations,[],[f1767]) ).
fof(f1769,definition,
sF18 = c_COMBC(sF17,tc_nat,tc_nat,tc_nat),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f1770,plain,
c_COMBC(sF17,tc_nat,tc_nat,tc_nat) = sF18,
inference(reorient_equations,[],[f1769]) ).
fof(f1771,definition,
sF19 = hAPP(sF18,v_i),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f1772,plain,
hAPP(sF18,v_i) = sF19,
inference(reorient_equations,[],[f1771]) ).
fof(f1773,definition,
sF20 = hAPP(sF16,sF19),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f1774,plain,
hAPP(sF16,sF19) = sF20,
inference(reorient_equations,[],[f1773]) ).
fof(f1775,definition,
sF21 = hAPP(sF12,sF20),
introduced(definition,[new_symbols(definition,[sF21])],[function_definition]) ).
fof(f1776,plain,
hAPP(sF12,sF20) = sF21,
inference(reorient_equations,[],[f1775]) ).
fof(f1777,definition,
sF22 = hAPP(sF9,sF21),
introduced(definition,[new_symbols(definition,[sF22])],[function_definition]) ).
fof(f1778,plain,
hAPP(sF9,sF21) = sF22,
inference(reorient_equations,[],[f1777]) ).
fof(f1779,definition,
sF23 = c_COMBC(sF22,tc_nat,sF6,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF23])],[function_definition]) ).
fof(f1780,plain,
c_COMBC(sF22,tc_nat,sF6,tc_Complex_Ocomplex) = sF23,
inference(reorient_equations,[],[f1779]) ).
fof(f1781,definition,
sF24 = c_HOL_Ozero__class_Ozero(tc_nat),
introduced(definition,[new_symbols(definition,[sF24])],[function_definition]) ).
fof(f1782,plain,
c_HOL_Ozero__class_Ozero(tc_nat) = sF24,
inference(reorient_equations,[],[f1781]) ).
fof(f1783,definition,
sF25 = c_SetInterval_Oord__class_OatLeastLessThan(sF24,v_n,tc_nat),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
fof(f1784,plain,
c_SetInterval_Oord__class_OatLeastLessThan(sF24,v_n,tc_nat) = sF25,
inference(reorient_equations,[],[f1783]) ).
fof(f1785,definition,
sF26 = hAPP(sF23,sF25),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
fof(f1786,plain,
hAPP(sF23,sF25) = sF26,
inference(reorient_equations,[],[f1785]) ).
fof(f1787,definition,
sF27 = hAPP(sF4,sF26),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
fof(f1788,plain,
hAPP(sF4,sF26) = sF27,
inference(reorient_equations,[],[f1787]) ).
fof(f1789,definition,
sF28 = c_COMBS(sF27,v_a,tc_nat,tc_Complex_Ocomplex,tc_Complex_Ocomplex),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f1790,plain,
c_COMBS(sF27,v_a,tc_nat,tc_Complex_Ocomplex,tc_Complex_Ocomplex) = sF28,
inference(reorient_equations,[],[f1789]) ).
fof(f1791,definition,
sF29 = hAPP(sF0,sF28),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
fof(f1792,plain,
hAPP(sF0,sF28) = sF29,
inference(reorient_equations,[],[f1791]) ).
fof(f1793,definition,
sF30 = c_SetInterval_Oord__class_OatLeastLessThan(v_i,v_n,tc_nat),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f1794,plain,
c_SetInterval_Oord__class_OatLeastLessThan(v_i,v_n,tc_nat) = sF30,
inference(reorient_equations,[],[f1793]) ).
fof(f1795,definition,
sF31 = hAPP(sF29,sF30),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
fof(f1796,plain,
hAPP(sF29,sF30) = sF31,
inference(reorient_equations,[],[f1795]) ).
fof(f1797,definition,
sF32 = c_Orderings_Obot__class_Obot(sF6),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
fof(f1798,plain,
c_Orderings_Obot__class_Obot(sF6) = sF32,
inference(reorient_equations,[],[f1797]) ).
fof(f1799,definition,
sF33 = c_Set_Oinsert(v_i,sF32,tc_nat),
introduced(definition,[new_symbols(definition,[sF33])],[function_definition]) ).
fof(f1800,plain,
c_Set_Oinsert(v_i,sF32,tc_nat) = sF33,
inference(reorient_equations,[],[f1799]) ).
fof(f1801,definition,
sF34 = c_SetInterval_Oord__class_OgreaterThanLessThan(v_i,v_n,tc_nat),
introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).
fof(f1802,plain,
c_SetInterval_Oord__class_OgreaterThanLessThan(v_i,v_n,tc_nat) = sF34,
inference(reorient_equations,[],[f1801]) ).
fof(f1803,definition,
sF35 = c_Lattices_Oupper__semilattice__class_Osup(sF33,sF34,sF6),
introduced(definition,[new_symbols(definition,[sF35])],[function_definition]) ).
fof(f1804,plain,
c_Lattices_Oupper__semilattice__class_Osup(sF33,sF34,sF6) = sF35,
inference(reorient_equations,[],[f1803]) ).
fof(f1805,definition,
sF36 = hAPP(sF29,sF35),
introduced(definition,[new_symbols(definition,[sF36])],[function_definition]) ).
fof(f1806,plain,
hAPP(sF29,sF35) = sF36,
inference(reorient_equations,[],[f1805]) ).
fof(f1807,plain,
sF31 != sF36,
inference(definition_folding,[],[f1573,f1806,f1804,f1746,f1802,f1800,f1798,f1746,f1792,f1790,f1788,f1786,f1784,f1782,f1780,f1746,f1778,f1776,f1774,f1772,f1770,f1768,f1766,f1764,f1762,f1756,f1760,f1758,f1756,f1754,f1744,f1752,f1734,f1750,f1748,f1746,f1744,f1742,f1740,f1738,f1736,f1734,f1796,f1794,f1792,f1790,f1788,f1786,f1784,f1782,f1780,f1746,f1778,f1776,f1774,f1772,f1770,f1768,f1766,f1764,f1762,f1756,f1760,f1758,f1756,f1754,f1744,f1752,f1734,f1750,f1748,f1746,f1744,f1742,f1740,f1738,f1736,f1734]) ).
fof(f1809,plain,
! [X2,X3,X0,X1] : c_Lattices_Oupper__semilattice__class_Osup(c_Set_Oinsert(X0,X1,X2),X3,tc_fun(X2,tc_bool)) = c_Lattices_Oupper__semilattice__class_Osup(X1,c_Set_Oinsert(X0,X3,X2),tc_fun(X2,tc_bool)),
inference(forward_demodulation,[],[f1448,f1449]) ).
fof(f1810,plain,
! [X2,X0,X1] :
( ~ hBOOL(hAPP(c_HOL_Oord__class_Oless(X1,X0),X2))
| ~ class_Orderings_Olinorder(X0)
| c_SetInterval_Oord__class_OatLeastLessThan(X1,X2,X0) = c_Set_Oinsert(X1,c_SetInterval_Oord__class_OgreaterThanLessThan(X1,X2,X0),X0) ),
inference(forward_demodulation,[],[f1405,f1565]) ).
fof(f1855,plain,
( class_Lattices_Obounded__lattice(sF6)
| ~ class_Lattices_Obounded__lattice(tc_bool) ),
inference(superposition,[],[f1578,f1746]) ).
fof(f1856,plain,
class_Lattices_Obounded__lattice(sF6),
inference(forward_subsumption_resolution,[],[f1855,f1627]) ).
fof(f1919,plain,
! [X0] : c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(sF6),X0,sF6) = X0,
inference(resolution,[],[f1492,f1856]) ).
fof(f1920,plain,
! [X0] : c_Lattices_Oupper__semilattice__class_Osup(sF32,X0,sF6) = X0,
inference(forward_demodulation,[],[f1919,f1798]) ).
fof(f10678,plain,
! [X0] : c_Lattices_Oupper__semilattice__class_Osup(sF32,c_Set_Oinsert(v_i,X0,tc_nat),tc_fun(tc_nat,tc_bool)) = c_Lattices_Oupper__semilattice__class_Osup(sF33,X0,tc_fun(tc_nat,tc_bool)),
inference(superposition,[],[f1809,f1800]) ).
fof(f10732,plain,
! [X0] : c_Lattices_Oupper__semilattice__class_Osup(sF33,X0,sF6) = c_Lattices_Oupper__semilattice__class_Osup(sF32,c_Set_Oinsert(v_i,X0,tc_nat),sF6),
inference(forward_demodulation,[],[f10678,f1746]) ).
fof(f10742,plain,
! [X0] : c_Set_Oinsert(v_i,X0,tc_nat) = c_Lattices_Oupper__semilattice__class_Osup(sF33,X0,sF6),
inference(forward_demodulation,[],[f10732,f1920]) ).
fof(f13428,plain,
( ~ class_Orderings_Olinorder(tc_nat)
| c_SetInterval_Oord__class_OatLeastLessThan(v_i,v_n,tc_nat) = c_Set_Oinsert(v_i,c_SetInterval_Oord__class_OgreaterThanLessThan(v_i,v_n,tc_nat),tc_nat) ),
inference(resolution,[],[f1810,f1572]) ).
fof(f13450,plain,
c_SetInterval_Oord__class_OatLeastLessThan(v_i,v_n,tc_nat) = c_Set_Oinsert(v_i,c_SetInterval_Oord__class_OgreaterThanLessThan(v_i,v_n,tc_nat),tc_nat),
inference(forward_subsumption_resolution,[],[f13428,f1617]) ).
fof(f13480,plain,
c_SetInterval_Oord__class_OatLeastLessThan(v_i,v_n,tc_nat) = c_Lattices_Oupper__semilattice__class_Osup(sF33,c_SetInterval_Oord__class_OgreaterThanLessThan(v_i,v_n,tc_nat),sF6),
inference(forward_demodulation,[],[f13450,f10742]) ).
fof(f13494,plain,
c_SetInterval_Oord__class_OatLeastLessThan(v_i,v_n,tc_nat) = c_Lattices_Oupper__semilattice__class_Osup(sF33,sF34,sF6),
inference(forward_demodulation,[],[f13480,f1802]) ).
fof(f13499,plain,
c_SetInterval_Oord__class_OatLeastLessThan(v_i,v_n,tc_nat) = sF35,
inference(forward_demodulation,[],[f13494,f1804]) ).
fof(f13500,plain,
sF30 = sF35,
inference(forward_demodulation,[],[f13499,f1794]) ).
fof(f13501,plain,
hAPP(sF29,sF30) = sF36,
inference(superposition,[],[f1806,f13500]) ).
fof(f13529,plain,
sF31 = sF36,
inference(forward_demodulation,[],[f13501,f1796]) ).
fof(f13530,plain,
$false,
inference(forward_subsumption_resolution,[],[f13529,f1807]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV693-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.17 % Computer : n006.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 12:16:21 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21 Running first-order model finding
% 0.09/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
% 15.75/2.52 % (3925902)Will run a generic schedule for satisfiability detection.
% 15.75/2.52 % (3925908)% WARNING: option uhcvi not known.
% 15.75/2.52 % (3925908)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2804197315:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.75/2.52 % (3925907)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1399130661_2999 on theBenchmark for (2999ds/0Mi)
% 15.75/2.52 % (3925909)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1772613106:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.75/2.52 % (3925910)dis+10_1_sil=32000:sp=arity:random_seed=2900689807:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.75/2.52 % (3925911)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3223017364:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.75/2.52 % (3925912)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1697382724:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.75/2.52 % (3925913)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=193603144:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.75/2.52 % (3925911)Instruction limit reached!
% 15.75/2.52 % (3925911)------------------------------
% 15.75/2.52 % (3925911)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.75/2.52 % (3925911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.75/2.52 % (3925911)CaDiCaL version: 2.1.3
% 15.75/2.52 % (3925911)Termination reason: Instruction limit
% 15.75/2.52 % (3925911)Termination phase: Saturation
% 15.75/2.52 % (3925911)Time elapsed: 0.064 s
% 15.75/2.52 % (3925911)Peak memory usage: 14 MB
% 15.75/2.52 % (3925911)Instructions burned: 117 (million)
% 15.75/2.52 % (3925910)Instruction limit reached!
% 15.75/2.52 % (3925910)------------------------------
% 15.75/2.52 % (3925910)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.75/2.52 % (3925910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.75/2.52 % (3925910)CaDiCaL version: 2.1.3
% 15.75/2.52 % (3925910)Termination reason: Instruction limit
% 15.75/2.52 % (3925910)Termination phase: Saturation
% 15.75/2.52 % (3925910)Time elapsed: 0.067 s
% 15.75/2.52 % (3925910)Peak memory usage: 14 MB
% 15.75/2.52 % (3925910)Instructions burned: 104 (million)
% 15.75/2.52 % (3925912)Instruction limit reached!
% 15.75/2.52 % (3925912)------------------------------
% 15.75/2.52 % (3925912)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.75/2.52 % (3925912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.75/2.52 % (3925912)CaDiCaL version: 2.1.3
% 15.75/2.52 % (3925912)Termination reason: Instruction limit
% 15.75/2.52 % (3925912)Termination phase: Saturation
% 15.75/2.52 % (3925912)Time elapsed: 0.082 s
% 15.75/2.52 % (3925912)Peak memory usage: 15 MB
% 15.75/2.52 % (3925912)Instructions burned: 132 (million)
% 15.75/2.52 % (3925921)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3126268352:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 15.75/2.52 % (3925922)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1221001446:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 15.75/2.52 % (3925923)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=142702497:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.75/2.52 % (3925913)Instruction limit reached!
% 15.75/2.52 % (3925913)------------------------------
% 15.75/2.52 % (3925913)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.75/2.52 % (3925913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.75/2.52 % (3925913)CaDiCaL version: 2.1.3
% 15.75/2.52 % (3925913)Termination reason: Instruction limit
% 15.75/2.52 % (3925913)Termination phase: Saturation
% 15.75/2.52 % (3925913)Time elapsed: 0.109 s
% 15.75/2.52 % (3925913)Peak memory usage: 15 MB
% 15.75/2.52 % (3925913)Instructions burned: 159 (million)
% 15.75/2.52 % (3925927)ott-21_1_sil=16000:fs=off:random_seed=1593274256:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 15.75/2.52 % (3925922)Instruction limit reached!
% 15.75/2.52 % (3925922)------------------------------
% 15.75/2.52 % (3925922)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.75/2.52 % (3925922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.75/2.52 % (3925922)CaDiCaL version: 2.1.3
% 9.16/3.63 % (3925922)Termination reason: Instruction limit
% 9.16/3.63 % (3925922)Termination phase: Saturation
% 9.16/3.63 % (3925922)Time elapsed: 0.076 s
% 9.16/3.63 % (3925922)Peak memory usage: 14 MB
% 9.16/3.63 % (3925922)Instructions burned: 132 (million)
% 9.16/3.63 % (3925929)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3597920886:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 9.16/3.63 % (3925927)Instruction limit reached!
% 9.16/3.63 % (3925927)------------------------------
% 9.16/3.63 % (3925927)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.16/3.63 % (3925927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.16/3.63 % (3925927)CaDiCaL version: 2.1.3
% 9.16/3.63 % (3925927)Termination reason: Instruction limit
% 9.16/3.63 % (3925927)Termination phase: Saturation
% 9.16/3.63 % (3925927)Time elapsed: 0.097 s
% 9.16/3.63 % (3925927)Peak memory usage: 14 MB
% 9.16/3.63 % (3925927)Instructions burned: 180 (million)
% 9.16/3.63 % (3925931)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2473556780:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 9.16/3.63 % (3925921)Instruction limit reached!
% 9.16/3.63 % (3925921)------------------------------
% 9.16/3.63 % (3925921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.16/3.63 % (3925921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.16/3.63 % (3925921)CaDiCaL version: 2.1.3
% 9.16/3.63 % (3925921)Termination reason: Instruction limit
% 9.16/3.63 % (3925921)Termination phase: Finite model building preprocessing
% 9.16/3.63 % (3925921)Time elapsed: 0.355 s
% 9.16/3.63 % (3925921)Peak memory usage: 21 MB
% 9.16/3.63 % (3925921)Instructions burned: 715 (million)
% 9.16/3.63 % (3925933)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=624576602:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 9.16/3.63 % (3925929)Instruction limit reached!
% 9.16/3.63 % (3925929)------------------------------
% 9.16/3.63 % (3925929)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.16/3.63 % (3925929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.16/3.63 % (3925929)CaDiCaL version: 2.1.3
% 9.16/3.63 % (3925929)Termination reason: Instruction limit
% 9.16/3.63 % (3925929)Termination phase: Saturation
% 9.16/3.63 % (3925929)Time elapsed: 0.309 s
% 9.16/3.63 % (3925929)Peak memory usage: 15 MB
% 9.16/3.63 % (3925929)Instructions burned: 478 (million)
% 9.16/3.63 % (3925935)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4166030863:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 9.16/3.63 % TRYING [1]
% 9.16/3.63 % (3925923)Instruction limit reached!
% 9.16/3.63 % (3925923)------------------------------
% 9.16/3.63 % (3925923)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.16/3.63 % (3925923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.16/3.63 % (3925923)CaDiCaL version: 2.1.3
% 9.16/3.63 % (3925923)Termination reason: Instruction limit
% 9.16/3.63 % (3925923)Termination phase: Saturation
% 9.16/3.63 % (3925923)Time elapsed: 0.421 s
% 9.16/3.63 % (3925923)Peak memory usage: 20 MB
% 9.16/3.63 % (3925923)Instructions burned: 685 (million)
% 9.16/3.63 % TRYING [2]
% 9.16/3.63 % (3925937)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2208458625:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2993 on theBenchmark for (2993ds/692Mi)
% 9.16/3.63 % (3925931)Instruction limit reached!
% 9.16/3.63 % (3925931)------------------------------
% 9.16/3.63 % (3925931)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.16/3.63 % (3925931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.16/3.63 % (3925931)CaDiCaL version: 2.1.3
% 9.16/3.63 % (3925931)Termination reason: Instruction limit
% 9.16/3.63 % (3925931)Termination phase: Finite model building preprocessing
% 9.16/3.63 % (3925931)Time elapsed: 0.437 s
% 9.16/3.63 % (3925931)Peak memory usage: 23 MB
% 9.16/3.63 % (3925931)Instructions burned: 866 (million)
% 9.16/3.63 % (3925939)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3980467268:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 9.16/3.63 % TRYING [3]
% 9.16/3.63 % (3925935)Instruction limit reached!
% 9.16/3.63 % (3925935)------------------------------
% 9.16/3.63 % (3925935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.16/3.63 % (3925935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.16/3.63 % (3925935)CaDiCaL version: 2.1.3
% 9.16/3.63 % (3925935)Termination reason: Instruction limit
% 9.16/3.63 % (3925935)Termination phase: Finite model building preprocessing
% 9.16/3.63 % (3925935)Time elapsed: 0.446 s
% 9.16/3.63 % (3925935)Peak memory usage: 27 MB
% 9.16/3.63 % (3925935)Instructions burned: 889 (million)
% 9.16/3.63 % (3925941)fmb+10_1_sil=64000:random_seed=3362529751:i=22061:nm=2:gsp=on_2989 on theBenchmark for (2989ds/22061Mi)
% 9.16/3.63 % (3925937)Instruction limit reached!
% 9.16/3.63 % (3925937)------------------------------
% 9.16/3.63 % (3925937)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.16/3.63 % (3925937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.16/3.63 % (3925937)CaDiCaL version: 2.1.3
% 9.16/3.63 % (3925937)Termination reason: Instruction limit
% 9.16/3.63 % (3925937)Termination phase: Saturation
% 9.16/3.63 % (3925937)Time elapsed: 0.450 s
% 9.16/3.63 % (3925937)Peak memory usage: 21 MB
% 9.16/3.63 % (3925937)Instructions burned: 693 (million)
% 9.16/3.63 % (3925943)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3853219738:i=9515:nm=5_2988 on theBenchmark for (2988ds/9515Mi)
% 9.16/3.63 % (3925939)Instruction limit reached!
% 9.16/3.63 % (3925939)------------------------------
% 9.16/3.63 % (3925939)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.16/3.63 % (3925939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.16/3.63 % (3925939)CaDiCaL version: 2.1.3
% 9.16/3.63 % (3925939)Termination reason: Instruction limit
% 9.16/3.63 % (3925939)Termination phase: Saturation
% 9.16/3.63 % (3925939)Time elapsed: 0.462 s
% 9.16/3.63 % (3925939)Peak memory usage: 20 MB
% 9.16/3.63 % (3925939)Instructions burned: 880 (million)
% 9.16/3.63 % (3925933)Instruction limit reached!
% 9.16/3.63 % (3925933)------------------------------
% 9.16/3.63 % (3925933)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.16/3.63 % (3925933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.16/3.63 % (3925933)CaDiCaL version: 2.1.3
% 9.16/3.63 % (3925933)Termination reason: Instruction limit
% 9.16/3.63 % (3925933)Termination phase: Saturation
% 9.16/3.63 % (3925933)Time elapsed: 0.720 s
% 9.16/3.63 % (3925933)Peak memory usage: 23 MB
% 9.16/3.63 % (3925933)Instructions burned: 1179 (million)
% 9.16/3.63 % (3925945)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3963375853:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi)
% 9.16/3.63 % (3925946)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1306075296:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 9.16/3.63 % TRYING [1]
% 9.16/3.63 % (3925943)Cannot represent all propositional literals internally
% 9.16/3.63 % (3925943)Refutation not found, incomplete strategy
% 9.16/3.63 % (3925943)------------------------------
% 9.16/3.63 % (3925943)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.16/3.63 % (3925943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.16/3.63 % (3925943)CaDiCaL version: 2.1.3
% 9.16/3.63 % (3925943)Termination reason: Refutation not found, incomplete strategy
% 9.16/3.63 % (3925943)Time elapsed: 0.516 s
% 9.16/3.63 % (3925943)Peak memory usage: 27 MB
% 9.16/3.63 % (3925943)Instructions burned: 1008 (million)
% 9.16/3.63 % (3925943)------------------------------
% 9.16/3.63 % (3925943)------------------------------
% 9.16/3.63 % (3925949)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1378244907:i=1472:ins=7:fdi=8:gsp=on_2983 on theBenchmark for (2983ds/1472Mi)
% 9.16/3.63 % TRYING [2]
% 9.16/3.63 % (3925945)Instruction limit reached!
% 9.16/3.63 % (3925945)------------------------------
% 9.16/3.63 % (3925945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.16/3.63 % (3925945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.16/3.63 % (3925945)CaDiCaL version: 2.1.3
% 9.16/3.63 % (3925945)Termination reason: Instruction limit
% 9.16/3.63 % (3925945)Termination phase: Finite model building preprocessing
% 9.16/3.63 % (3925945)Time elapsed: 0.463 s
% 9.16/3.63 % (3925945)Peak memory usage: 27 MB
% 9.16/3.63 % (3925945)Instructions burned: 922 (million)
% 9.16/3.63 % (3925951)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1244652826:i=6324_2982 on theBenchmark for (2982ds/6324Mi)
% 9.16/3.63 % (3925951)Cannot represent all propositional literals internally
% 9.16/3.63 % (3925951)Refutation not found, incomplete strategy
% 9.16/3.63 % (3925951)------------------------------
% 9.16/3.63 % (3925951)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.16/3.63 % (3925951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.16/3.63 % (3925951)CaDiCaL version: 2.1.3
% 9.16/3.63 % (3925951)Termination reason: Refutation not found, incomplete strategy
% 9.16/3.63 % (3925951)Time elapsed: 0.518 s
% 9.16/3.63 % (3925951)Peak memory usage: 27 MB
% 9.16/3.63 % (3925951)Instructions burned: 1049 (million)
% 9.16/3.63 % (3925951)------------------------------
% 9.16/3.63 % (3925951)------------------------------
% 9.16/3.63 % (3925953)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3346213091:fmbsr=2.30978:i=2174_2976 on theBenchmark for (2976ds/2174Mi)
% 9.16/3.63 % (3925949)Instruction limit reached!
% 9.16/3.63 % (3925949)------------------------------
% 9.16/3.63 % (3925949)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.16/3.63 % (3925949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.16/3.63 % (3925949)CaDiCaL version: 2.1.3
% 9.16/3.63 % (3925949)Termination reason: Instruction limit
% 9.16/3.63 % (3925949)Termination phase: Saturation
% 9.16/3.63 % (3925949)Time elapsed: 0.842 s
% 9.16/3.63 % (3925949)Peak memory usage: 32 MB
% 9.16/3.63 % (3925949)Instructions burned: 1473 (million)
% 9.16/3.63 % (3925955)ott-2_1_sil=16000:newcnf=on:random_seed=2027923915:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2974 on theBenchmark for (2974ds/869Mi)
% 9.16/3.63 % (3925955)Instruction limit reached!
% 9.16/3.63 % (3925955)------------------------------
% 9.16/3.63 % (3925955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.16/3.63 % (3925955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.16/3.63 % (3925955)CaDiCaL version: 2.1.3
% 9.16/3.63 % (3925955)Termination reason: Instruction limit
% 9.16/3.63 % (3925955)Termination phase: Saturation
% 9.16/3.63 % (3925955)Time elapsed: 0.431 s
% 9.16/3.63 % (3925955)Peak memory usage: 19 MB
% 9.16/3.63 % (3925955)Instructions burned: 870 (million)
% 9.16/3.63 % TRYING [4]
% 9.16/3.63 % (3925957)ott+10_1_sil=32000:tgt=ground:random_seed=3570975476:i=5114:av=off_2970 on theBenchmark for (2970ds/5114Mi)
% 9.16/3.63 % (3925957) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3925902-3925957"...
% 9.16/3.63 % (3925957)...printing done.
% 9.16/3.63 % (3925957)Refutation found. Thanks to Tanya!
% 9.16/3.63 % SZS status Unsatisfiable for theBenchmark
% 9.16/3.63 % SZS output start Proof for theBenchmark
% See solution above
% 9.16/3.63 % (3925957)------------------------------
% 9.16/3.63 % (3925957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.16/3.63 % (3925957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.16/3.63 % (3925957)CaDiCaL version: 2.1.3
% 9.16/3.63 % (3925957)Termination reason: Refutation
% 9.16/3.63 % (3925957)Time elapsed: 0.371 s
% 9.16/3.63 % (3925957)Peak memory usage: 18 MB
% 9.16/3.63 % (3925957)Instructions burned: 615 (million)
% 9.16/3.63 % (3925902)Success in time 3.402 s
% 9.16/3.63 % Vampire exiting
%------------------------------------------------------------------------------