search

ontologyportal / sigmakee

Sigma Knowledge Engineering Environment
https://www.ontologyportal.org
GNU General Public License v3.0
103 stars 35 forks source link

CVC4 with TF0 translation #48

Closed arademaker closed 5 years ago

arademaker commented 5 years ago

http://aitp-conference.org/2019/slides/AP.pdf

It says

Also works in CVC4 – thanks Geoff! Will be part of CASC-TPTP after CASC 2019

How can I run CVC4 with the TFO file produced by SigmaKEE?

apease commented 5 years ago

Using the SystemOnTPTP interface to Geoff’s servers is the easiest way. In theory you should be able to run Cvc4 locally with an extra script Geoff has but I t didn’t work for me although I didn’t spend much time on that approach

arademaker commented 5 years ago

Is this script in the repo? Can you share?

apease commented 5 years ago

sorry for the delay, trying to track this down but didn't find it right away

apease commented 5 years ago

maybe here - https://github.com/CVC4/CVC4/blob/master/contrib/run-script-cascj7-tff

apease commented 5 years ago

here's the link to SystemOnTPTP where you can upload a SUMO TFF0 file and select CVC4 as the prover - http://www.tptp.org/cgi-bin/SystemOnTPTP

arademaker commented 5 years ago

Thank you @apease ! I was able to run the script and I obtained the same output I reported in https://github.com/CVC4/CVC4/issues/3077#issuecomment-506986477. The problem is that I am not sure how to interpret the result. If CVC4 says it is a theorem, it proved the conjecture?

If I changed the conjecture in the minimal.tptp file to fof(q1, conjecture, s_instance(bslug, s_Vertebrate))., Vampire produces a Satisfiable answer. In a refutation based method, this means that the conjecture is not a logical consequence from the theory. CVC4 does not finish with this conjecture. Vampire proof below. 

% lrs-11_4:1_afp=4000:afq=2.0:anc=none:br=off:gs=on:lwlo=on:nm=64:nwc=3:stl=30:urr=on_2 on minimal
% Refutation not found, incomplete strategy
% ------------------------------
% Version: Vampire 4.3.0 (commit 83de4041 on 2019-05-17 12:56:57 +0200)
% Termination reason: Refutation not found, incomplete strategy

% Memory used [KB]: 9722
% Time elapsed: 0.003 s
% ------------------------------
% ------------------------------
% WARNING: value z3 for option sas not known
% dis+10_50_add=large:afr=on:afp=4000:afq=1.0:amm=off:anc=none:cond=on:fsr=off:gs=on:lma=on:nm=64:nwc=1:sas=z3:sos=on:sp=occurrence:thf=on:updr=off_2 on minimal
% Refutation not found, incomplete strategy
% ------------------------------
% Version: Vampire 4.3.0 (commit 83de4041 on 2019-05-17 12:56:57 +0200)
% Termination reason: Refutation not found, incomplete strategy

% Memory used [KB]: 9594
% Time elapsed: 0.001 s
% ------------------------------
% ------------------------------
% dis+11_3_afr=on:afp=4000:afq=1.4:anc=none:cond=on:fsr=off:gs=on:lcm=reverse:nm=64:nwc=1:sos=on:sp=reverse_arity_3 on minimal
% Refutation not found, incomplete strategy
% ------------------------------
% Version: Vampire 4.3.0 (commit 83de4041 on 2019-05-17 12:56:57 +0200)
% Termination reason: Refutation not found, incomplete strategy

% Memory used [KB]: 9594
% Time elapsed: 0.002 s
% ------------------------------
% ------------------------------
% lrs+4_32_add=large:afp=10000:afq=1.2:amm=sco:anc=none:cond=on:fsr=off:gsp=input_only:lcm=predicate:lma=on:nm=2:nwc=1:stl=30:sac=on:sp=occurrence:urr=on_11 on minimal
% SZS status CounterSatisfiable for minimal
% # SZS output start Saturation.
tff(u1943,axiom,
    (![X1, X3, X0, X2] : ((~s_instance(X3,s_Entity) | s_instance(X3,X2) | ~s_instance(X3,X0) | ~s_exhaustiveDecomposition3(X0,X2,X1) | ~s_instance(X0,s_SetOrClass) | ~s_instance(X0,s_Class) | ~s_instance(X1,s_Class) | ~s_instance(X1,s_SetOrClass) | ~s_instance(X2,s_Class) | ~s_instance(X2,s_SetOrClass) | s_instance(X3,X1))))).

tff(u1942,axiom,
    (![X1, X0, X2] : ((~s_instance(X2,s_Entity) | ~s_instance(X2,X1) | ~s_disjoint(X1,X0) | ~s_instance(X0,s_SetOrClass) | ~s_instance(X1,s_SetOrClass) | ~s_instance(X2,X0))))).

tff(u1941,axiom,
    (![X5, X4] : ((~s_instance(X5,s_Class) | ~s_instance(X4,s_Class) | sP1(X4,s_Animal,X5))))).

tff(u1940,axiom,
    (![X3, X2] : ((~s_instance(X3,s_Class) | ~s_instance(X2,s_Class) | sP1(X2,s_Invertebrate,X3))))).

tff(u1939,axiom,
    (![X1, X0] : ((~s_instance(X1,s_Class) | ~s_instance(X0,s_Class) | sP1(X0,s_Vertebrate,X1))))).

tff(u1938,axiom,
    (![X1, X0, X2] : ((~s_instance(X2,s_Class) | ~s_instance(X0,s_Class) | ~s_instance(X1,s_Class) | sP1(X0,X2,X1))))).

tff(u1937,axiom,
    (![X0] : ((~s_instance(X0,s_Animal) | s_part(sK2(X0),X0) | ~s_instance(X0,s_Vertebrate))))).

tff(u1936,axiom,
    (![X1, X0, X2] : ((~s_instance(X2,s_SetOrClass) | ~s_disjointDecomposition3(X0,X2,X1) | ~s_instance(X1,s_SetOrClass) | ~s_instance(X1,s_Class) | ~s_instance(X0,s_Class) | ~s_instance(X2,s_Class) | s_disjoint(X2,X1))))).

tff(u1935,axiom,
    (![X1, X0, X2] : ((~s_instance(X2,s_SetOrClass) | ~s_disjoint(X2,X1) | ~s_instance(X1,s_SetOrClass) | ~s_instance(X1,s_Class) | ~s_instance(X0,s_Class) | ~s_instance(X2,s_Class) | s_disjointDecomposition3(X0,X2,X1))))).

tff(u1934,axiom,
    ((~(![X1, X0] : ((~s_instance(X1,s_SetOrClass) | s_disjoint(s_Vertebrate,X1) | ~s_instance(X0,s_Class) | ~s_instance(X1,s_Class) | ~s_disjointDecomposition3(X0,s_Vertebrate,X1))))) | (![X1, X0] : ((~s_instance(X1,s_SetOrClass) | s_disjoint(s_Vertebrate,X1) | ~s_instance(X0,s_Class) | ~s_instance(X1,s_Class) | ~s_disjointDecomposition3(X0,s_Vertebrate,X1)))))).

tff(u1933,axiom,
    ((~(![X3, X2] : ((~s_instance(X3,s_SetOrClass) | s_disjoint(s_Invertebrate,X3) | ~s_instance(X2,s_Class) | ~s_instance(X3,s_Class) | ~s_disjointDecomposition3(X2,s_Invertebrate,X3))))) | (![X3, X2] : ((~s_instance(X3,s_SetOrClass) | s_disjoint(s_Invertebrate,X3) | ~s_instance(X2,s_Class) | ~s_instance(X3,s_Class) | ~s_disjointDecomposition3(X2,s_Invertebrate,X3)))))).

tff(u1932,axiom,
    ((~(![X5, X4] : ((~s_instance(X5,s_SetOrClass) | s_disjoint(s_Animal,X5) | ~s_instance(X4,s_Class) | ~s_instance(X5,s_Class) | ~s_disjointDecomposition3(X4,s_Animal,X5))))) | (![X5, X4] : ((~s_instance(X5,s_SetOrClass) | s_disjoint(s_Animal,X5) | ~s_instance(X4,s_Class) | ~s_instance(X5,s_Class) | ~s_disjointDecomposition3(X4,s_Animal,X5)))))).

tff(u1931,axiom,
    ((~(![X3, X2] : ((~s_instance(X3,s_SetOrClass) | s_instance(bslug,X3) | ~s_instance(X2,s_SetOrClass) | ~s_instance(X2,s_Class) | s_instance(bslug,X2) | ~s_instance(X3,s_Class) | ~s_exhaustiveDecomposition3(s_Animal,X2,X3))))) | (![X3, X2] : ((~s_instance(X3,s_SetOrClass) | s_instance(bslug,X3) | ~s_instance(X2,s_SetOrClass) | ~s_instance(X2,s_Class) | s_instance(bslug,X2) | ~s_instance(X3,s_Class) | ~s_exhaustiveDecomposition3(s_Animal,X2,X3)))))).

tff(u1930,negated_conjecture,
    ((~(![X5, X4] : ((~s_instance(X5,s_SetOrClass) | s_instance(bslug,X5) | ~s_instance(X4,s_SetOrClass) | ~s_instance(X4,s_Class) | s_instance(bslug,X4) | ~s_instance(X5,s_Class) | ~s_exhaustiveDecomposition3(s_Invertebrate,X4,X5))))) | (![X5, X4] : ((~s_instance(X5,s_SetOrClass) | s_instance(bslug,X5) | ~s_instance(X4,s_SetOrClass) | ~s_instance(X4,s_Class) | s_instance(bslug,X4) | ~s_instance(X5,s_Class) | ~s_exhaustiveDecomposition3(s_Invertebrate,X4,X5)))))).

tff(u1929,negated_conjecture,
    ~s_instance(bslug,s_Vertebrate)).

tff(u1928,axiom,
    (![X1, X0, X2] : ((~s_instance(bslug,X1) | s_instance(bslug,X0) | ~s_exhaustiveDecomposition3(X1,X0,X2) | ~s_instance(X1,s_SetOrClass) | ~s_instance(X1,s_Class) | ~s_instance(X2,s_Class) | ~s_instance(X2,s_SetOrClass) | ~s_instance(X0,s_Class) | ~s_instance(X0,s_SetOrClass) | s_instance(bslug,X2))))).

tff(u1927,axiom,
    (![X1, X0] : ((~s_instance(bslug,X1) | ~s_disjoint(X0,X1) | ~s_instance(X1,s_SetOrClass) | ~s_instance(X0,s_SetOrClass) | ~s_instance(bslug,X0))))).

tff(u1926,axiom,
    ((~~s_instance(s_Entity,s_SetOrClass)) | ~s_instance(s_Entity,s_SetOrClass))).

tff(u1925,axiom,
    s_instance(bslug,s_Entity)).

tff(u1924,negated_conjecture,
    s_instance(bslug,s_Invertebrate)).

tff(u1923,axiom,
    s_instance(bslug,s_Animal)).

tff(u1922,axiom,
    s_instance(s_Vertebrate,s_Class)).

tff(u1921,axiom,
    s_instance(s_Vertebrate,s_SetOrClass)).

tff(u1920,axiom,
    s_instance(s_Invertebrate,s_Class)).

tff(u1919,axiom,
    s_instance(s_Invertebrate,s_SetOrClass)).

tff(u1918,axiom,
    s_instance(s_Animal,s_Class)).

tff(u1917,axiom,
    s_instance(s_Animal,s_SetOrClass)).

tff(u1916,axiom,
    (![X0] : (s_instance(sK2(X0),s_Object)))).

tff(u1915,axiom,
    (![X0] : ((s_instance(sK2(X0),s_SpinalColumn) | ~s_instance(X0,s_Vertebrate) | ~s_instance(X0,s_Animal))))).

tff(u1914,axiom,
    (![X0] : ((~s_subclass(X0,s_Entity) | s_instance(X0,s_Class))))).

tff(u1913,axiom,
    (![X0] : ((s_subclass(X0,s_Entity) | ~s_instance(X0,s_Class))))).

tff(u1912,axiom,
    s_subclass(s_Vertebrate,s_Entity)).

tff(u1911,axiom,
    s_subclass(s_Invertebrate,s_Entity)).

tff(u1910,axiom,
    s_subclass(s_Animal,s_Entity)).

tff(u1909,axiom,
    ((~(![X1] : ((~s_disjoint(X1,s_Animal) | ~s_instance(bslug,X1) | ~s_instance(X1,s_SetOrClass))))) | (![X1] : ((~s_disjoint(X1,s_Animal) | ~s_instance(bslug,X1) | ~s_instance(X1,s_SetOrClass)))))).

tff(u1908,negated_conjecture,
    ((~(![X2] : ((~s_disjoint(X2,s_Invertebrate) | ~s_instance(bslug,X2) | ~s_instance(X2,s_SetOrClass))))) | (![X2] : ((~s_disjoint(X2,s_Invertebrate) | ~s_instance(bslug,X2) | ~s_instance(X2,s_SetOrClass)))))).

tff(u1907,axiom,
    ((~(![X0] : ((~s_disjointDecomposition3(X0,s_Vertebrate,s_Vertebrate) | ~s_instance(X0,s_Class))))) | ~s_disjoint(s_Vertebrate,s_Vertebrate))).

tff(u1906,axiom,
    ((~(![X2] : ((~s_disjointDecomposition3(X2,s_Vertebrate,s_Animal) | ~s_instance(X2,s_Class))))) | ~s_disjoint(s_Vertebrate,s_Animal))).

tff(u1905,axiom,
    ((~(![X1, X0] : ((~s_disjoint(s_Vertebrate,X0) | ~s_instance(X1,s_Class) | s_disjointDecomposition3(X1,s_Vertebrate,X0) | ~s_instance(X0,s_Class) | ~s_instance(X0,s_SetOrClass))))) | (![X1, X0] : ((~s_disjoint(s_Vertebrate,X0) | ~s_instance(X1,s_Class) | s_disjointDecomposition3(X1,s_Vertebrate,X0) | ~s_instance(X0,s_Class) | ~s_instance(X0,s_SetOrClass)))))).

tff(u1904,axiom,
    ((~(![X3, X2] : ((~s_disjoint(s_Invertebrate,X2) | ~s_instance(X3,s_Class) | s_disjointDecomposition3(X3,s_Invertebrate,X2) | ~s_instance(X2,s_Class) | ~s_instance(X2,s_SetOrClass))))) | (![X3, X2] : ((~s_disjoint(s_Invertebrate,X2) | ~s_instance(X3,s_Class) | s_disjointDecomposition3(X3,s_Invertebrate,X2) | ~s_instance(X2,s_Class) | ~s_instance(X2,s_SetOrClass)))))).

tff(u1903,axiom,
    ((~(![X0] : ((~s_disjointDecomposition3(X0,s_Invertebrate,s_Vertebrate) | ~s_instance(X0,s_Class))))) | ~s_disjoint(s_Invertebrate,s_Vertebrate))).

tff(u1902,negated_conjecture,
    ~s_disjoint(s_Invertebrate,s_Invertebrate)).

tff(u1901,negated_conjecture,
    ~s_disjoint(s_Invertebrate,s_Animal)).

tff(u1900,axiom,
    ((~(![X5, X4] : ((~s_disjoint(s_Animal,X4) | ~s_instance(X5,s_Class) | s_disjointDecomposition3(X5,s_Animal,X4) | ~s_instance(X4,s_Class) | ~s_instance(X4,s_SetOrClass))))) | (![X5, X4] : ((~s_disjoint(s_Animal,X4) | ~s_instance(X5,s_Class) | s_disjointDecomposition3(X5,s_Animal,X4) | ~s_instance(X4,s_Class) | ~s_instance(X4,s_SetOrClass)))))).

tff(u1899,axiom,
    ((~(![X0] : ((~s_disjointDecomposition3(X0,s_Animal,s_Vertebrate) | ~s_instance(X0,s_Class))))) | ~s_disjoint(s_Animal,s_Vertebrate))).

tff(u1898,negated_conjecture,
    ~s_disjoint(s_Animal,s_Invertebrate)).

tff(u1897,axiom,
    ~s_disjoint(s_Animal,s_Animal)).

tff(u1896,axiom,
    s_disjoint(s_Vertebrate,s_Invertebrate)).

tff(u1895,axiom,
    ((~(![X0] : ((~s_exhaustiveDecomposition3(s_Animal,X0,s_Vertebrate) | ~s_instance(X0,s_SetOrClass) | s_instance(bslug,X0) | ~s_instance(X0,s_Class))))) | (![X0] : ((~s_exhaustiveDecomposition3(s_Animal,X0,s_Vertebrate) | ~s_instance(X0,s_SetOrClass) | s_instance(bslug,X0) | ~s_instance(X0,s_Class)))))).

tff(u1894,negated_conjecture,
    ((~(![X0] : ((~s_exhaustiveDecomposition3(s_Invertebrate,X0,s_Vertebrate) | ~s_instance(X0,s_SetOrClass) | s_instance(bslug,X0) | ~s_instance(X0,s_Class))))) | (![X0] : ((~s_exhaustiveDecomposition3(s_Invertebrate,X0,s_Vertebrate) | ~s_instance(X0,s_SetOrClass) | s_instance(bslug,X0) | ~s_instance(X0,s_Class)))))).

tff(u1893,axiom,
    ((~~sP0(s_Invertebrate,s_Vertebrate,s_Vertebrate)) | ~s_exhaustiveDecomposition3(s_Vertebrate,s_Vertebrate,s_Invertebrate))).

tff(u1892,axiom,
    ((~~sP0(s_Invertebrate,s_Vertebrate,s_Invertebrate)) | ~s_exhaustiveDecomposition3(s_Invertebrate,s_Vertebrate,s_Invertebrate))).

tff(u1891,negated_conjecture,
    ~s_exhaustiveDecomposition3(s_Animal,s_Vertebrate,s_Vertebrate)).

tff(u1890,negated_conjecture,
    ~s_exhaustiveDecomposition3(s_Invertebrate,s_Vertebrate,s_Vertebrate)).

tff(u1889,axiom,
    ((~~s_exhaustiveDecomposition3(s_Vertebrate,s_Vertebrate,s_Vertebrate)) | ~s_exhaustiveDecomposition3(s_Vertebrate,s_Vertebrate,s_Vertebrate))).

tff(u1888,axiom,
    ((~~s_exhaustiveDecomposition3(s_Vertebrate,s_Vertebrate,s_Animal)) | ~s_exhaustiveDecomposition3(s_Vertebrate,s_Vertebrate,s_Animal))).

tff(u1887,axiom,
    ((~~s_exhaustiveDecomposition3(s_Invertebrate,s_Vertebrate,s_Animal)) | ~s_exhaustiveDecomposition3(s_Invertebrate,s_Vertebrate,s_Animal))).

tff(u1886,axiom,
    ((~~s_exhaustiveDecomposition3(s_Animal,s_Vertebrate,s_Animal)) | ~s_exhaustiveDecomposition3(s_Animal,s_Vertebrate,s_Animal))).

tff(u1885,axiom,
    ((~~s_exhaustiveDecomposition3(s_Vertebrate,s_Invertebrate,s_Vertebrate)) | ~s_exhaustiveDecomposition3(s_Vertebrate,s_Invertebrate,s_Vertebrate))).

tff(u1884,axiom,
    ((~~s_exhaustiveDecomposition3(s_Vertebrate,s_Invertebrate,s_Invertebrate)) | ~s_exhaustiveDecomposition3(s_Vertebrate,s_Invertebrate,s_Invertebrate))).

tff(u1883,axiom,
    ((~~s_exhaustiveDecomposition3(s_Vertebrate,s_Invertebrate,s_Animal)) | ~s_exhaustiveDecomposition3(s_Vertebrate,s_Invertebrate,s_Animal))).

tff(u1882,axiom,
    ((~~s_exhaustiveDecomposition3(s_Invertebrate,s_Invertebrate,s_Vertebrate)) | ~s_exhaustiveDecomposition3(s_Invertebrate,s_Invertebrate,s_Vertebrate))).

tff(u1881,axiom,
    ((~~s_exhaustiveDecomposition3(s_Invertebrate,s_Invertebrate,s_Invertebrate)) | ~s_exhaustiveDecomposition3(s_Invertebrate,s_Invertebrate,s_Invertebrate))).

tff(u1880,axiom,
    ((~~s_exhaustiveDecomposition3(s_Invertebrate,s_Invertebrate,s_Animal)) | ~s_exhaustiveDecomposition3(s_Invertebrate,s_Invertebrate,s_Animal))).

tff(u1879,axiom,
    ((~~s_exhaustiveDecomposition3(s_Animal,s_Invertebrate,s_Vertebrate)) | ~s_exhaustiveDecomposition3(s_Animal,s_Invertebrate,s_Vertebrate))).

tff(u1878,axiom,
    ((~~s_exhaustiveDecomposition3(s_Vertebrate,s_Animal,s_Vertebrate)) | ~s_exhaustiveDecomposition3(s_Vertebrate,s_Animal,s_Vertebrate))).

tff(u1877,axiom,
    ((~~s_exhaustiveDecomposition3(s_Invertebrate,s_Animal,s_Vertebrate)) | ~s_exhaustiveDecomposition3(s_Invertebrate,s_Animal,s_Vertebrate))).

tff(u1876,axiom,
    ((~~s_exhaustiveDecomposition3(s_Animal,s_Animal,s_Vertebrate)) | ~s_exhaustiveDecomposition3(s_Animal,s_Animal,s_Vertebrate))).

tff(u1875,axiom,
    s_exhaustiveDecomposition3(s_Animal,s_Vertebrate,s_Invertebrate)).

tff(u1874,axiom,
    ((~(![X0] : ((~s_disjointDecomposition3(X0,s_Vertebrate,s_Vertebrate) | ~s_instance(X0,s_Class))))) | (![X0] : ((~s_partition3(X0,s_Vertebrate,s_Vertebrate) | ~s_instance(X0,s_Class)))))).

tff(u1873,axiom,
    (![X2] : ((~s_partition3(X2,s_Vertebrate,s_Vertebrate) | ~s_instance(X2,s_Class) | s_exhaustiveDecomposition3(X2,s_Vertebrate,s_Vertebrate))))).

tff(u1872,axiom,
    (![X2] : ((~s_partition3(X2,s_Vertebrate,s_Invertebrate) | ~s_instance(X2,s_Class) | s_exhaustiveDecomposition3(X2,s_Vertebrate,s_Invertebrate))))).

tff(u1871,axiom,
    ((~(![X2] : ((~s_disjointDecomposition3(X2,s_Vertebrate,s_Animal) | ~s_instance(X2,s_Class))))) | (![X0] : ((~s_partition3(X0,s_Vertebrate,s_Animal) | ~s_instance(X0,s_Class)))))).

tff(u1870,axiom,
    (![X2] : ((~s_partition3(X2,s_Vertebrate,s_Animal) | ~s_instance(X2,s_Class) | s_exhaustiveDecomposition3(X2,s_Vertebrate,s_Animal))))).

tff(u1869,axiom,
    ((~(![X0] : ((~s_disjointDecomposition3(X0,s_Invertebrate,s_Vertebrate) | ~s_instance(X0,s_Class))))) | (![X0] : ((~s_partition3(X0,s_Invertebrate,s_Vertebrate) | ~s_instance(X0,s_Class)))))).

tff(u1868,axiom,
    (![X2] : ((~s_partition3(X2,s_Invertebrate,s_Vertebrate) | ~s_instance(X2,s_Class) | s_exhaustiveDecomposition3(X2,s_Invertebrate,s_Vertebrate))))).

tff(u1867,axiom,
    ((~(![X1] : ((~s_disjointDecomposition3(X1,s_Invertebrate,s_Invertebrate) | ~s_instance(X1,s_Class))))) | (![X0] : ((~s_partition3(X0,s_Invertebrate,s_Invertebrate) | ~s_instance(X0,s_Class)))))).

tff(u1866,axiom,
    (![X2] : ((~s_partition3(X2,s_Invertebrate,s_Invertebrate) | ~s_instance(X2,s_Class) | s_exhaustiveDecomposition3(X2,s_Invertebrate,s_Invertebrate))))).

tff(u1865,axiom,
    ((~(![X2] : ((~s_disjointDecomposition3(X2,s_Invertebrate,s_Animal) | ~s_instance(X2,s_Class))))) | (![X0] : ((~s_partition3(X0,s_Invertebrate,s_Animal) | ~s_instance(X0,s_Class)))))).

tff(u1864,axiom,
    (![X2] : ((~s_partition3(X2,s_Invertebrate,s_Animal) | ~s_instance(X2,s_Class) | s_exhaustiveDecomposition3(X2,s_Invertebrate,s_Animal))))).

tff(u1863,axiom,
    ((~(![X0] : ((~s_disjointDecomposition3(X0,s_Animal,s_Vertebrate) | ~s_instance(X0,s_Class))))) | (![X0] : ((~s_partition3(X0,s_Animal,s_Vertebrate) | ~s_instance(X0,s_Class)))))).

tff(u1862,axiom,
    (![X2] : ((~s_partition3(X2,s_Animal,s_Vertebrate) | ~s_instance(X2,s_Class) | s_exhaustiveDecomposition3(X2,s_Animal,s_Vertebrate))))).

tff(u1861,axiom,
    ((~(![X1] : ((~s_disjointDecomposition3(X1,s_Animal,s_Invertebrate) | ~s_instance(X1,s_Class))))) | (![X0] : ((~s_partition3(X0,s_Animal,s_Invertebrate) | ~s_instance(X0,s_Class)))))).

tff(u1860,axiom,
    (![X2] : ((~s_partition3(X2,s_Animal,s_Invertebrate) | ~s_instance(X2,s_Class) | s_exhaustiveDecomposition3(X2,s_Animal,s_Invertebrate))))).

tff(u1859,axiom,
    ((~(![X2] : ((~s_disjointDecomposition3(X2,s_Animal,s_Animal) | ~s_instance(X2,s_Class))))) | (![X0] : ((~s_partition3(X0,s_Animal,s_Animal) | ~s_instance(X0,s_Class)))))).

tff(u1858,axiom,
    (![X2] : ((~s_partition3(X2,s_Animal,s_Animal) | ~s_instance(X2,s_Class) | s_exhaustiveDecomposition3(X2,s_Animal,s_Animal))))).

tff(u1857,axiom,
    ((~~sP0(s_Vertebrate,s_Vertebrate,s_Vertebrate)) | ~s_partition3(s_Vertebrate,s_Vertebrate,s_Vertebrate))).

tff(u1856,axiom,
    ((~~sP0(s_Invertebrate,s_Vertebrate,s_Vertebrate)) | ~s_partition3(s_Vertebrate,s_Vertebrate,s_Invertebrate))).

tff(u1855,axiom,
    ((~~sP0(s_Animal,s_Vertebrate,s_Vertebrate)) | ~s_partition3(s_Vertebrate,s_Vertebrate,s_Animal))).

tff(u1854,axiom,
    ~s_partition3(s_Vertebrate,s_Animal,s_Animal)).

tff(u1853,negated_conjecture,
    ~s_partition3(s_Vertebrate,s_Animal,s_Invertebrate)).

tff(u1852,axiom,
    ((~~sP0(s_Vertebrate,s_Animal,s_Vertebrate)) | ~s_partition3(s_Vertebrate,s_Animal,s_Vertebrate))).

tff(u1851,axiom,
    ((~~sP0(s_Vertebrate,s_Invertebrate,s_Vertebrate)) | ~s_partition3(s_Vertebrate,s_Invertebrate,s_Vertebrate))).

tff(u1850,axiom,
    ((~~sP0(s_Invertebrate,s_Invertebrate,s_Vertebrate)) | ~s_partition3(s_Vertebrate,s_Invertebrate,s_Invertebrate))).

tff(u1849,axiom,
    ((~~sP0(s_Animal,s_Invertebrate,s_Vertebrate)) | ~s_partition3(s_Vertebrate,s_Invertebrate,s_Animal))).

tff(u1848,axiom,
    ~s_partition3(s_Invertebrate,s_Animal,s_Animal)).

tff(u1847,negated_conjecture,
    ~s_partition3(s_Invertebrate,s_Animal,s_Invertebrate)).

tff(u1846,axiom,
    ((~~sP0(s_Vertebrate,s_Animal,s_Invertebrate)) | ~s_partition3(s_Invertebrate,s_Animal,s_Vertebrate))).

tff(u1845,axiom,
    ((~~sP0(s_Vertebrate,s_Vertebrate,s_Invertebrate)) | ~s_partition3(s_Invertebrate,s_Vertebrate,s_Vertebrate))).

tff(u1844,axiom,
    ((~~sP0(s_Invertebrate,s_Vertebrate,s_Invertebrate)) | ~s_partition3(s_Invertebrate,s_Vertebrate,s_Invertebrate))).

tff(u1843,axiom,
    ((~~sP0(s_Animal,s_Vertebrate,s_Invertebrate)) | ~s_partition3(s_Invertebrate,s_Vertebrate,s_Animal))).

tff(u1842,axiom,
    ((~~sP0(s_Vertebrate,s_Invertebrate,s_Invertebrate)) | ~s_partition3(s_Invertebrate,s_Invertebrate,s_Vertebrate))).

tff(u1841,axiom,
    ((~~sP0(s_Invertebrate,s_Invertebrate,s_Invertebrate)) | ~s_partition3(s_Invertebrate,s_Invertebrate,s_Invertebrate))).

tff(u1840,axiom,
    ((~~sP0(s_Animal,s_Invertebrate,s_Invertebrate)) | ~s_partition3(s_Invertebrate,s_Invertebrate,s_Animal))).

tff(u1839,axiom,
    ~s_partition3(s_Animal,s_Animal,s_Animal)).

tff(u1838,negated_conjecture,
    ~s_partition3(s_Animal,s_Animal,s_Invertebrate)).

tff(u1837,axiom,
    ((~~sP0(s_Vertebrate,s_Animal,s_Animal)) | ~s_partition3(s_Animal,s_Animal,s_Vertebrate))).

tff(u1836,axiom,
    ((~~sP0(s_Vertebrate,s_Vertebrate,s_Animal)) | ~s_partition3(s_Animal,s_Vertebrate,s_Vertebrate))).

tff(u1835,axiom,
    ((~~sP0(s_Animal,s_Vertebrate,s_Animal)) | ~s_partition3(s_Animal,s_Vertebrate,s_Animal))).

tff(u1834,axiom,
    ((~~sP0(s_Vertebrate,s_Invertebrate,s_Animal)) | ~s_partition3(s_Animal,s_Invertebrate,s_Vertebrate))).

tff(u1833,negated_conjecture,
    ~s_partition3(s_Animal,s_Invertebrate,s_Invertebrate)).

tff(u1832,negated_conjecture,
    ~s_partition3(s_Animal,s_Invertebrate,s_Animal)).

tff(u1831,axiom,
    s_partition3(s_Animal,s_Vertebrate,s_Invertebrate)).

tff(u1830,axiom,
    ((~(![X0] : ((s_disjointDecomposition3(X0,s_Vertebrate,s_Invertebrate) | ~s_instance(X0,s_Class))))) | (![X0] : ((s_partition3(X0,s_Vertebrate,s_Invertebrate) | ~s_instance(X0,s_Class) | ~s_exhaustiveDecomposition3(X0,s_Vertebrate,s_Invertebrate)))))).

tff(u1829,axiom,
    ((~(![X2] : ((~s_disjointDecomposition3(X2,s_Animal,s_Animal) | ~s_instance(X2,s_Class))))) | (![X2] : ((~s_disjointDecomposition3(X2,s_Animal,s_Animal) | ~s_instance(X2,s_Class)))))).

tff(u1828,axiom,
    (![X0] : ((~s_disjointDecomposition3(X0,s_Animal,s_Animal) | s_partition3(X0,s_Animal,s_Animal) | ~s_instance(X0,s_Class) | ~s_exhaustiveDecomposition3(X0,s_Animal,s_Animal))))).

tff(u1827,axiom,
    ~s_disjointDecomposition3(s_Vertebrate,s_Animal,s_Animal)).

tff(u1826,axiom,
    ~s_disjointDecomposition3(s_Invertebrate,s_Animal,s_Animal)).

tff(u1825,axiom,
    ~s_disjointDecomposition3(s_Animal,s_Animal,s_Animal)).

tff(u1824,axiom,
    ((~(![X1] : ((~s_disjointDecomposition3(X1,s_Animal,s_Invertebrate) | ~s_instance(X1,s_Class))))) | (![X1] : ((~s_disjointDecomposition3(X1,s_Animal,s_Invertebrate) | ~s_instance(X1,s_Class)))))).

tff(u1823,axiom,
    (![X0] : ((~s_disjointDecomposition3(X0,s_Animal,s_Invertebrate) | s_partition3(X0,s_Animal,s_Invertebrate) | ~s_instance(X0,s_Class) | ~s_exhaustiveDecomposition3(X0,s_Animal,s_Invertebrate))))).

tff(u1822,negated_conjecture,
    ~s_disjointDecomposition3(s_Vertebrate,s_Animal,s_Invertebrate)).

tff(u1821,negated_conjecture,
    ~s_disjointDecomposition3(s_Invertebrate,s_Animal,s_Invertebrate)).

tff(u1820,negated_conjecture,
    ~s_disjointDecomposition3(s_Animal,s_Animal,s_Invertebrate)).

tff(u1819,axiom,
    ((~(![X0] : ((~s_disjointDecomposition3(X0,s_Animal,s_Vertebrate) | ~s_instance(X0,s_Class))))) | (![X0] : ((~s_disjointDecomposition3(X0,s_Animal,s_Vertebrate) | ~s_instance(X0,s_Class)))))).

tff(u1818,axiom,
    (![X0] : ((~s_disjointDecomposition3(X0,s_Animal,s_Vertebrate) | s_partition3(X0,s_Animal,s_Vertebrate) | ~s_instance(X0,s_Class) | ~s_exhaustiveDecomposition3(X0,s_Animal,s_Vertebrate))))).

tff(u1817,axiom,
    ((~(![X0] : ((~s_disjointDecomposition3(X0,s_Animal,s_Vertebrate) | ~s_instance(X0,s_Class))))) | ~s_disjointDecomposition3(s_Vertebrate,s_Animal,s_Vertebrate))).

tff(u1816,axiom,
    ((~(![X0] : ((~s_disjointDecomposition3(X0,s_Animal,s_Vertebrate) | ~s_instance(X0,s_Class))))) | ~s_disjointDecomposition3(s_Invertebrate,s_Animal,s_Vertebrate))).

tff(u1815,axiom,
    ((~(![X0] : ((~s_disjointDecomposition3(X0,s_Animal,s_Vertebrate) | ~s_instance(X0,s_Class))))) | ~s_disjointDecomposition3(s_Animal,s_Animal,s_Vertebrate))).

tff(u1814,axiom,
    ((~(![X1] : ((~s_disjointDecomposition3(X1,s_Invertebrate,s_Invertebrate) | ~s_instance(X1,s_Class))))) | (![X1] : ((~s_disjointDecomposition3(X1,s_Invertebrate,s_Invertebrate) | ~s_instance(X1,s_Class)))))).

tff(u1813,axiom,
    (![X0] : ((~s_disjointDecomposition3(X0,s_Invertebrate,s_Invertebrate) | s_partition3(X0,s_Invertebrate,s_Invertebrate) | ~s_instance(X0,s_Class) | ~s_exhaustiveDecomposition3(X0,s_Invertebrate,s_Invertebrate))))).

tff(u1812,negated_conjecture,
    ~s_disjointDecomposition3(s_Vertebrate,s_Invertebrate,s_Invertebrate)).

tff(u1811,negated_conjecture,
    ~s_disjointDecomposition3(s_Invertebrate,s_Invertebrate,s_Invertebrate)).

tff(u1810,negated_conjecture,
    ~s_disjointDecomposition3(s_Animal,s_Invertebrate,s_Invertebrate)).

tff(u1809,axiom,
    ((~(![X2] : ((~s_disjointDecomposition3(X2,s_Invertebrate,s_Animal) | ~s_instance(X2,s_Class))))) | (![X2] : ((~s_disjointDecomposition3(X2,s_Invertebrate,s_Animal) | ~s_instance(X2,s_Class)))))).

tff(u1808,axiom,
    (![X0] : ((~s_disjointDecomposition3(X0,s_Invertebrate,s_Animal) | s_partition3(X0,s_Invertebrate,s_Animal) | ~s_instance(X0,s_Class) | ~s_exhaustiveDecomposition3(X0,s_Invertebrate,s_Animal))))).

tff(u1807,negated_conjecture,
    ~s_disjointDecomposition3(s_Vertebrate,s_Invertebrate,s_Animal)).

tff(u1806,negated_conjecture,
    ~s_disjointDecomposition3(s_Invertebrate,s_Invertebrate,s_Animal)).

tff(u1805,negated_conjecture,
    ~s_disjointDecomposition3(s_Animal,s_Invertebrate,s_Animal)).

tff(u1804,axiom,
    ((~(![X0] : ((~s_disjointDecomposition3(X0,s_Invertebrate,s_Vertebrate) | ~s_instance(X0,s_Class))))) | (![X0] : ((~s_disjointDecomposition3(X0,s_Invertebrate,s_Vertebrate) | ~s_instance(X0,s_Class)))))).

tff(u1803,axiom,
    (![X0] : ((~s_disjointDecomposition3(X0,s_Invertebrate,s_Vertebrate) | s_partition3(X0,s_Invertebrate,s_Vertebrate) | ~s_instance(X0,s_Class) | ~s_exhaustiveDecomposition3(X0,s_Invertebrate,s_Vertebrate))))).

tff(u1802,axiom,
    ((~(![X0] : ((~s_disjointDecomposition3(X0,s_Invertebrate,s_Vertebrate) | ~s_instance(X0,s_Class))))) | ~s_disjointDecomposition3(s_Vertebrate,s_Invertebrate,s_Vertebrate))).

tff(u1801,axiom,
    ((~(![X0] : ((~s_disjointDecomposition3(X0,s_Invertebrate,s_Vertebrate) | ~s_instance(X0,s_Class))))) | ~s_disjointDecomposition3(s_Invertebrate,s_Invertebrate,s_Vertebrate))).

tff(u1800,axiom,
    ((~(![X0] : ((~s_disjointDecomposition3(X0,s_Invertebrate,s_Vertebrate) | ~s_instance(X0,s_Class))))) | ~s_disjointDecomposition3(s_Animal,s_Invertebrate,s_Vertebrate))).

tff(u1799,axiom,
    ((~(![X0] : ((~s_disjointDecomposition3(X0,s_Vertebrate,s_Vertebrate) | ~s_instance(X0,s_Class))))) | (![X0] : ((~s_disjointDecomposition3(X0,s_Vertebrate,s_Vertebrate) | ~s_instance(X0,s_Class)))))).

tff(u1798,axiom,
    (![X0] : ((~s_disjointDecomposition3(X0,s_Vertebrate,s_Vertebrate) | s_partition3(X0,s_Vertebrate,s_Vertebrate) | ~s_instance(X0,s_Class) | ~s_exhaustiveDecomposition3(X0,s_Vertebrate,s_Vertebrate))))).

tff(u1797,axiom,
    (![X0] : ((~s_disjointDecomposition3(X0,s_Vertebrate,s_Invertebrate) | s_partition3(X0,s_Vertebrate,s_Invertebrate) | ~s_instance(X0,s_Class) | ~s_exhaustiveDecomposition3(X0,s_Vertebrate,s_Invertebrate))))).

tff(u1796,axiom,
    ((~(![X2] : ((~s_disjointDecomposition3(X2,s_Vertebrate,s_Animal) | ~s_instance(X2,s_Class))))) | (![X2] : ((~s_disjointDecomposition3(X2,s_Vertebrate,s_Animal) | ~s_instance(X2,s_Class)))))).

tff(u1795,axiom,
    (![X0] : ((~s_disjointDecomposition3(X0,s_Vertebrate,s_Animal) | s_partition3(X0,s_Vertebrate,s_Animal) | ~s_instance(X0,s_Class) | ~s_exhaustiveDecomposition3(X0,s_Vertebrate,s_Animal))))).

tff(u1794,axiom,
    ((~(![X0] : ((~s_disjointDecomposition3(X0,s_Vertebrate,s_Vertebrate) | ~s_instance(X0,s_Class))))) | ~s_disjointDecomposition3(s_Vertebrate,s_Vertebrate,s_Vertebrate))).

tff(u1793,axiom,
    ((~(![X2] : ((~s_disjointDecomposition3(X2,s_Vertebrate,s_Animal) | ~s_instance(X2,s_Class))))) | ~s_disjointDecomposition3(s_Vertebrate,s_Vertebrate,s_Animal))).

tff(u1792,axiom,
    ((~(![X0] : ((~s_disjointDecomposition3(X0,s_Vertebrate,s_Vertebrate) | ~s_instance(X0,s_Class))))) | ~s_disjointDecomposition3(s_Invertebrate,s_Vertebrate,s_Vertebrate))).

tff(u1791,axiom,
    ((~(![X2] : ((~s_disjointDecomposition3(X2,s_Vertebrate,s_Animal) | ~s_instance(X2,s_Class))))) | ~s_disjointDecomposition3(s_Invertebrate,s_Vertebrate,s_Animal))).

tff(u1790,axiom,
    ((~(![X0] : ((~s_disjointDecomposition3(X0,s_Vertebrate,s_Vertebrate) | ~s_instance(X0,s_Class))))) | ~s_disjointDecomposition3(s_Animal,s_Vertebrate,s_Vertebrate))).

tff(u1789,axiom,
    ((~(![X2] : ((~s_disjointDecomposition3(X2,s_Vertebrate,s_Animal) | ~s_instance(X2,s_Class))))) | ~s_disjointDecomposition3(s_Animal,s_Vertebrate,s_Animal))).

tff(u1788,axiom,
    ((~(![X0] : ((s_disjointDecomposition3(X0,s_Vertebrate,s_Invertebrate) | ~s_instance(X0,s_Class))))) | (![X0] : ((s_disjointDecomposition3(X0,s_Vertebrate,s_Invertebrate) | ~s_instance(X0,s_Class)))))).

tff(u1787,axiom,
    (![X1] : ((s_disjointDecomposition3(X1,s_Vertebrate,s_Invertebrate) | ~s_instance(X1,s_Class) | ~s_partition3(X1,s_Vertebrate,s_Invertebrate))))).

tff(u1786,axiom,
    s_disjointDecomposition3(s_Vertebrate,s_Vertebrate,s_Invertebrate)).

tff(u1785,axiom,
    s_disjointDecomposition3(s_Invertebrate,s_Vertebrate,s_Invertebrate)).

tff(u1784,axiom,
    s_disjointDecomposition3(s_Animal,s_Vertebrate,s_Invertebrate)).

tff(u1783,axiom,
    (![X1] : ((s_disjointDecomposition3(X1,s_Vertebrate,s_Vertebrate) | ~s_instance(X1,s_Class) | ~s_partition3(X1,s_Vertebrate,s_Vertebrate))))).

tff(u1782,axiom,
    (![X1] : ((s_disjointDecomposition3(X1,s_Vertebrate,s_Animal) | ~s_instance(X1,s_Class) | ~s_partition3(X1,s_Vertebrate,s_Animal))))).

tff(u1781,axiom,
    (![X1] : ((s_disjointDecomposition3(X1,s_Invertebrate,s_Vertebrate) | ~s_instance(X1,s_Class) | ~s_partition3(X1,s_Invertebrate,s_Vertebrate))))).

tff(u1780,axiom,
    (![X1] : ((s_disjointDecomposition3(X1,s_Invertebrate,s_Invertebrate) | ~s_instance(X1,s_Class) | ~s_partition3(X1,s_Invertebrate,s_Invertebrate))))).

tff(u1779,axiom,
    (![X1] : ((s_disjointDecomposition3(X1,s_Invertebrate,s_Animal) | ~s_instance(X1,s_Class) | ~s_partition3(X1,s_Invertebrate,s_Animal))))).

tff(u1778,axiom,
    (![X1] : ((s_disjointDecomposition3(X1,s_Animal,s_Vertebrate) | ~s_instance(X1,s_Class) | ~s_partition3(X1,s_Animal,s_Vertebrate))))).

tff(u1777,axiom,
    (![X1] : ((s_disjointDecomposition3(X1,s_Animal,s_Invertebrate) | ~s_instance(X1,s_Class) | ~s_partition3(X1,s_Animal,s_Invertebrate))))).

tff(u1776,axiom,
    (![X1] : ((s_disjointDecomposition3(X1,s_Animal,s_Animal) | ~s_instance(X1,s_Class) | ~s_partition3(X1,s_Animal,s_Animal))))).

tff(u1775,axiom,
    (![X0] : ((~s_part(X0,bslug) | ~s_instance(X0,s_SpinalColumn) | ~s_instance(X0,s_Object))))).

tff(u1774,axiom,
    (![X1, X0, X2] : ((~sP0(X0,X1,X2) | s_disjointDecomposition3(X2,X1,X0))))).

tff(u1773,axiom,
    (![X1, X0, X2] : ((~sP0(X0,X1,X2) | s_exhaustiveDecomposition3(X2,X1,X0))))).

tff(u1772,axiom,
    (![X0] : ((~sP0(s_Vertebrate,s_Vertebrate,X0) | ~s_instance(X0,s_Class) | s_partition3(X0,s_Vertebrate,s_Vertebrate))))).

tff(u1771,axiom,
    ((~~sP0(s_Vertebrate,s_Vertebrate,s_Vertebrate)) | ~sP0(s_Vertebrate,s_Vertebrate,s_Vertebrate))).

tff(u1770,axiom,
    ((~~sP0(s_Vertebrate,s_Vertebrate,s_Invertebrate)) | ~sP0(s_Vertebrate,s_Vertebrate,s_Invertebrate))).

tff(u1769,axiom,
    ((~~sP0(s_Vertebrate,s_Vertebrate,s_Animal)) | ~sP0(s_Vertebrate,s_Vertebrate,s_Animal))).

tff(u1768,axiom,
    (![X0] : ((~sP0(s_Vertebrate,s_Invertebrate,X0) | ~s_instance(X0,s_Class) | s_partition3(X0,s_Invertebrate,s_Vertebrate))))).

tff(u1767,axiom,
    ((~~sP0(s_Vertebrate,s_Invertebrate,s_Vertebrate)) | ~sP0(s_Vertebrate,s_Invertebrate,s_Vertebrate))).

tff(u1766,axiom,
    ((~~sP0(s_Vertebrate,s_Invertebrate,s_Invertebrate)) | ~sP0(s_Vertebrate,s_Invertebrate,s_Invertebrate))).

tff(u1765,axiom,
    ((~~sP0(s_Vertebrate,s_Invertebrate,s_Animal)) | ~sP0(s_Vertebrate,s_Invertebrate,s_Animal))).

tff(u1764,axiom,
    (![X0] : ((~sP0(s_Vertebrate,s_Animal,X0) | ~s_instance(X0,s_Class) | s_partition3(X0,s_Animal,s_Vertebrate))))).

tff(u1763,axiom,
    ((~~sP0(s_Vertebrate,s_Animal,s_Vertebrate)) | ~sP0(s_Vertebrate,s_Animal,s_Vertebrate))).

tff(u1762,axiom,
    ((~~sP0(s_Vertebrate,s_Animal,s_Invertebrate)) | ~sP0(s_Vertebrate,s_Animal,s_Invertebrate))).

tff(u1761,axiom,
    ((~~sP0(s_Vertebrate,s_Animal,s_Animal)) | ~sP0(s_Vertebrate,s_Animal,s_Animal))).

tff(u1760,axiom,
    ((~~sP0(s_Invertebrate,s_Vertebrate,s_Vertebrate)) | ~sP0(s_Invertebrate,s_Vertebrate,s_Vertebrate))).

tff(u1759,axiom,
    ((~~sP0(s_Invertebrate,s_Vertebrate,s_Invertebrate)) | ~sP0(s_Invertebrate,s_Vertebrate,s_Invertebrate))).

tff(u1758,axiom,
    (![X0] : ((~sP0(s_Invertebrate,s_Vertebrate,X0) | ~s_instance(X0,s_Class) | s_partition3(X0,s_Vertebrate,s_Invertebrate))))).

tff(u1757,axiom,
    (![X0] : ((~sP0(s_Invertebrate,s_Invertebrate,X0) | ~s_instance(X0,s_Class) | s_partition3(X0,s_Invertebrate,s_Invertebrate))))).

tff(u1756,axiom,
    ((~~sP0(s_Invertebrate,s_Invertebrate,s_Vertebrate)) | ~sP0(s_Invertebrate,s_Invertebrate,s_Vertebrate))).

tff(u1755,axiom,
    ((~~sP0(s_Invertebrate,s_Invertebrate,s_Invertebrate)) | ~sP0(s_Invertebrate,s_Invertebrate,s_Invertebrate))).

tff(u1754,negated_conjecture,
    ~sP0(s_Invertebrate,s_Invertebrate,s_Animal)).

tff(u1753,axiom,
    (![X0] : ((~sP0(s_Invertebrate,s_Animal,X0) | ~s_instance(X0,s_Class) | s_partition3(X0,s_Animal,s_Invertebrate))))).

tff(u1752,negated_conjecture,
    ~sP0(s_Invertebrate,s_Animal,s_Vertebrate)).

tff(u1751,negated_conjecture,
    ~sP0(s_Invertebrate,s_Animal,s_Invertebrate)).

tff(u1750,negated_conjecture,
    ~sP0(s_Invertebrate,s_Animal,s_Animal)).

tff(u1749,axiom,
    (![X0] : ((~sP0(s_Animal,s_Vertebrate,X0) | ~s_instance(X0,s_Class) | s_partition3(X0,s_Vertebrate,s_Animal))))).

tff(u1748,axiom,
    (![X0] : ((~sP0(s_Animal,s_Invertebrate,X0) | ~s_instance(X0,s_Class) | s_partition3(X0,s_Invertebrate,s_Animal))))).

tff(u1747,axiom,
    (![X0] : ((~sP0(s_Animal,s_Animal,X0) | ~s_instance(X0,s_Class) | s_partition3(X0,s_Animal,s_Animal))))).

tff(u1746,axiom,
    ((~~sP0(s_Animal,s_Vertebrate,s_Vertebrate)) | ~sP0(s_Animal,s_Vertebrate,s_Vertebrate))).

tff(u1745,axiom,
    ~sP0(s_Animal,s_Animal,s_Vertebrate)).

tff(u1744,axiom,
    ((~~sP0(s_Animal,s_Invertebrate,s_Vertebrate)) | ~sP0(s_Animal,s_Invertebrate,s_Vertebrate))).

tff(u1743,axiom,
    ~sP0(s_Animal,s_Animal,s_Invertebrate)).

tff(u1742,axiom,
    ((~~sP0(s_Animal,s_Vertebrate,s_Invertebrate)) | ~sP0(s_Animal,s_Vertebrate,s_Invertebrate))).

tff(u1741,axiom,
    ((~~sP0(s_Animal,s_Invertebrate,s_Invertebrate)) | ~sP0(s_Animal,s_Invertebrate,s_Invertebrate))).

tff(u1740,axiom,
    ~sP0(s_Animal,s_Animal,s_Animal)).

tff(u1739,axiom,
    ((~~sP0(s_Animal,s_Vertebrate,s_Animal)) | ~sP0(s_Animal,s_Vertebrate,s_Animal))).

tff(u1738,negated_conjecture,
    ~sP0(s_Animal,s_Invertebrate,s_Animal)).

tff(u1737,axiom,
    (![X1, X0, X2] : ((sP0(X0,X1,X2) | ~s_disjointDecomposition3(X2,X1,X0) | ~s_exhaustiveDecomposition3(X2,X1,X0))))).

tff(u1736,axiom,
    (![X1] : ((sP0(s_Vertebrate,s_Vertebrate,X1) | ~s_partition3(X1,s_Vertebrate,s_Vertebrate) | ~s_instance(X1,s_Class))))).

tff(u1735,axiom,
    (![X1] : ((sP0(s_Vertebrate,s_Invertebrate,X1) | ~s_partition3(X1,s_Invertebrate,s_Vertebrate) | ~s_instance(X1,s_Class))))).

tff(u1734,axiom,
    (![X1] : ((sP0(s_Vertebrate,s_Animal,X1) | ~s_partition3(X1,s_Animal,s_Vertebrate) | ~s_instance(X1,s_Class))))).

tff(u1733,axiom,
    sP0(s_Invertebrate,s_Vertebrate,s_Animal)).

tff(u1732,axiom,
    (![X1] : ((sP0(s_Invertebrate,s_Vertebrate,X1) | ~s_partition3(X1,s_Vertebrate,s_Invertebrate) | ~s_instance(X1,s_Class))))).

tff(u1731,axiom,
    (![X1] : ((sP0(s_Invertebrate,s_Invertebrate,X1) | ~s_partition3(X1,s_Invertebrate,s_Invertebrate) | ~s_instance(X1,s_Class))))).

tff(u1730,axiom,
    (![X1] : ((sP0(s_Invertebrate,s_Animal,X1) | ~s_partition3(X1,s_Animal,s_Invertebrate) | ~s_instance(X1,s_Class))))).

tff(u1729,axiom,
    (![X1] : ((sP0(s_Animal,s_Vertebrate,X1) | ~s_partition3(X1,s_Vertebrate,s_Animal) | ~s_instance(X1,s_Class))))).

tff(u1728,axiom,
    (![X1] : ((sP0(s_Animal,s_Invertebrate,X1) | ~s_partition3(X1,s_Invertebrate,s_Animal) | ~s_instance(X1,s_Class))))).

tff(u1727,axiom,
    (![X1] : ((sP0(s_Animal,s_Animal,X1) | ~s_partition3(X1,s_Animal,s_Animal) | ~s_instance(X1,s_Class))))).

tff(u1726,axiom,
    (![X1, X0, X2] : ((~sP1(X0,X1,X2) | ~sP0(X2,X1,X0) | s_partition3(X0,X1,X2))))).

tff(u1725,axiom,
    (![X1, X0, X2] : ((~sP1(X0,X1,X2) | ~s_partition3(X0,X1,X2) | sP0(X2,X1,X0))))).

tff(u1724,axiom,
    (![X0] : ((sP1(X0,s_Vertebrate,s_Vertebrate) | ~s_instance(X0,s_Class))))).

tff(u1723,axiom,
    (![X1] : ((sP1(X1,s_Vertebrate,s_Invertebrate) | ~s_instance(X1,s_Class))))).

tff(u1722,axiom,
    (![X2] : ((sP1(X2,s_Vertebrate,s_Animal) | ~s_instance(X2,s_Class))))).

tff(u1721,axiom,
    sP1(s_Vertebrate,s_Vertebrate,s_Vertebrate)).

tff(u1720,axiom,
    sP1(s_Vertebrate,s_Vertebrate,s_Invertebrate)).

tff(u1719,axiom,
    sP1(s_Vertebrate,s_Vertebrate,s_Animal)).

tff(u1718,axiom,
    sP1(s_Invertebrate,s_Vertebrate,s_Vertebrate)).

tff(u1717,axiom,
    sP1(s_Invertebrate,s_Vertebrate,s_Invertebrate)).

tff(u1716,axiom,
    sP1(s_Invertebrate,s_Vertebrate,s_Animal)).

tff(u1715,axiom,
    sP1(s_Animal,s_Vertebrate,s_Vertebrate)).

tff(u1714,axiom,
    sP1(s_Animal,s_Vertebrate,s_Invertebrate)).

tff(u1713,axiom,
    sP1(s_Animal,s_Vertebrate,s_Animal)).

tff(u1712,axiom,
    (![X0] : ((sP1(X0,s_Invertebrate,s_Vertebrate) | ~s_instance(X0,s_Class))))).

tff(u1711,axiom,
    (![X1] : ((sP1(X1,s_Invertebrate,s_Invertebrate) | ~s_instance(X1,s_Class))))).

tff(u1710,axiom,
    (![X2] : ((sP1(X2,s_Invertebrate,s_Animal) | ~s_instance(X2,s_Class))))).

tff(u1709,axiom,
    sP1(s_Vertebrate,s_Invertebrate,s_Vertebrate)).

tff(u1708,axiom,
    sP1(s_Vertebrate,s_Invertebrate,s_Invertebrate)).

tff(u1707,axiom,
    sP1(s_Vertebrate,s_Invertebrate,s_Animal)).

tff(u1706,axiom,
    sP1(s_Invertebrate,s_Invertebrate,s_Vertebrate)).

tff(u1705,axiom,
    sP1(s_Invertebrate,s_Invertebrate,s_Invertebrate)).

tff(u1704,axiom,
    sP1(s_Invertebrate,s_Invertebrate,s_Animal)).

tff(u1703,axiom,
    sP1(s_Animal,s_Invertebrate,s_Vertebrate)).

tff(u1702,axiom,
    sP1(s_Animal,s_Invertebrate,s_Invertebrate)).

tff(u1701,axiom,
    sP1(s_Animal,s_Invertebrate,s_Animal)).

tff(u1700,axiom,
    (![X0] : ((sP1(X0,s_Animal,s_Vertebrate) | ~s_instance(X0,s_Class))))).

tff(u1699,axiom,
    (![X1] : ((sP1(X1,s_Animal,s_Invertebrate) | ~s_instance(X1,s_Class))))).

tff(u1698,axiom,
    (![X2] : ((sP1(X2,s_Animal,s_Animal) | ~s_instance(X2,s_Class))))).

tff(u1697,axiom,
    sP1(s_Vertebrate,s_Animal,s_Vertebrate)).

tff(u1696,axiom,
    sP1(s_Vertebrate,s_Animal,s_Invertebrate)).

tff(u1695,axiom,
    sP1(s_Vertebrate,s_Animal,s_Animal)).

tff(u1694,axiom,
    sP1(s_Invertebrate,s_Animal,s_Vertebrate)).

tff(u1693,axiom,
    sP1(s_Invertebrate,s_Animal,s_Invertebrate)).

tff(u1692,axiom,
    sP1(s_Invertebrate,s_Animal,s_Animal)).

tff(u1691,axiom,
    sP1(s_Animal,s_Animal,s_Vertebrate)).

tff(u1690,axiom,
    sP1(s_Animal,s_Animal,s_Invertebrate)).

tff(u1689,axiom,
    sP1(s_Animal,s_Animal,s_Animal)).

% # SZS output end Saturation.
% ------------------------------
% Version: Vampire 4.3.0 (commit 83de4041 on 2019-05-17 12:56:57 +0200)
% Termination reason: Satisfiable

% Memory used [KB]: 5884
% Time elapsed: 0.012 s
% ------------------------------
% ------------------------------
% Success in time 0.026 s
apease commented 5 years ago

The SZS status options are given at - http://www.tptp.org/TPTP/TPTPTParty/2007/PositionStatements/GeoffSutcliffe_SZS.html

arademaker commented 5 years ago

Nice, see my comments in the CVC4 issue. I closed there and I believe we can close it here too. My mistake, I should have checked the TPTP website more carefully. The Vampire and CVC4 outputs are the same for the minimal.tptp file.

Now I need to scrutinize the minimal.tptp file to see what is there not in the current version of SUMO (its FOF or TFO translations actually). This is because the banana slug is proved using the minimal.tptp but not using the SUMO translations plus the necessary axioms from the problem.