The cat does not chase the tiger. The cat is rough. The cat needs the lion. The cat needs the tiger. The cat visits the lion. The lion chases the cat. The lion chases the tiger. The lion is cold. The lion needs the cat. The lion needs the tiger. The lion visits the cat. The lion visits the tiger. The tiger chases the cat. The tiger is nice. The tiger needs the cat. The tiger visits the cat. If the lion needs the tiger then the lion is rough. If something visits the cat and the cat is young then it is not young. If something visits the cat and it is not kind then it is young. If something visits the lion and it does not need the tiger then the lion visits the cat. If something visits the tiger then it chases the tiger. If something visits the cat then it needs the cat.
The cat does not chase the tiger.
("cat" "chases" "tiger" "-")
The cat is rough.
("cat" "is" "rough" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The cat needs the tiger.
("cat" "needs" "tiger" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
The lion chases the tiger.
("lion" "chases" "tiger" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The tiger chases the cat.
("tiger" "chases" "cat" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger needs the cat.
("tiger" "needs" "cat" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
If the lion needs the tiger then the lion is rough.
((("lion" "needs" "tiger" "+")) -> ("lion" "is" "rough" "+"))
If something visits the cat and the cat is young then it is not young.
((("something" "visits" "cat" "+") ("cat" "is" "young" "+")) -> ("something" "is" "young" "-"))
If something visits the cat and it is not kind then it is young.
((("something" "visits" "cat" "+") ("something" "is" "kind" "~")) -> ("something" "is" "young" "+"))
If something visits the lion and it does not need the tiger then the lion visits the cat.
((("something" "visits" "lion" "+") ("something" "needs" "tiger" "~")) -> ("lion" "visits" "cat" "+"))
If something visits the tiger then it chases the tiger.
((("something" "visits" "tiger" "+")) -> ("something" "chases" "tiger" "+"))
If something visits the cat then it needs the cat.
((("something" "visits" "cat" "+")) -> ("something" "needs" "cat" "+"))
The tiger needs the cat.
True
1
proof
[(triple15 OR ((triple16) -> rule6))]
("tiger" "needs" "cat" "+")
triple15
((triple16) -> (rule6 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The lion does not chase the cat.
False
1
inv-proof
[(triple6)]
("lion" "chases" "cat" "-")
triple6
The lion is rough.
True
2
proof
[(((triple10) -> rule1))]
("lion" "is" "rough" "+")
((triple10) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The lion is not rough.
False
2
inv-proof
[(((triple10) -> rule1))]
("lion" "is" "rough" "-")
((triple10) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1
The tiger does not chase the tiger.
Unknown
inv-rconc
[@1: The tiger chases the tiger.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("tiger" "chases" "tiger" "-")
The lion is young.
Unknown
rconc
[@1: The lion is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "young" "+")
The tiger does not visit the lion.
Unknown
inv-random
[@0: The tiger visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "lion" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The cat does not chase the tiger.[(triple1)] The cat is rough.[(triple2)] The cat needs the lion.[(triple3)] The cat needs the tiger.[(triple4)] The cat visits the lion.[(triple5)] The lion chases the cat.[(triple6)] The lion chases the tiger.[(triple7 OR ((triple12) -> rule5))] The lion is cold.[(triple8)] The lion needs the cat.[(triple9 OR ((triple11) -> rule6))] The lion needs the tiger.[(triple10)] The lion visits the cat.[(triple11)] The lion visits the tiger.[(triple12)] The tiger chases the cat.[(triple13)] The tiger is nice.[(triple14)] The tiger needs the cat.[(triple15 OR ((triple16) -> rule6))] The tiger visits the cat.[(triple16)] @1: The lion is rough.[(((triple10) -> rule1))]
The cat does not chase the tiger.
("cat" "chases" "tiger" "-")
triple1
The cat is rough.
("cat" "is" "rough" "+")
triple2
The cat needs the lion.
("cat" "needs" "lion" "+")
triple3
The cat needs the tiger.
("cat" "needs" "tiger" "+")
triple4
The cat visits the lion.
("cat" "visits" "lion" "+")
triple5
The lion chases the cat.
("lion" "chases" "cat" "+")
triple6
The lion chases the tiger.
("lion" "chases" "tiger" "+")
triple7
((triple12) -> (rule5 % int1))
The lion chases the tiger.
("lion" "chases" "tiger" "+")
int1
The lion is cold.
("lion" "is" "cold" "+")
triple8
The lion needs the cat.
("lion" "needs" "cat" "+")
triple9
((triple11) -> (rule6 % int1))
The lion needs the cat.
("lion" "needs" "cat" "+")
int1
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple10
The lion visits the cat.
("lion" "visits" "cat" "+")
triple11
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple12
The tiger chases the cat.
("tiger" "chases" "cat" "+")
triple13
The tiger is nice.
("tiger" "is" "nice" "+")
triple14
The tiger needs the cat.
("tiger" "needs" "cat" "+")
triple15
((triple16) -> (rule6 % int1))
The tiger needs the cat.
("tiger" "needs" "cat" "+")
int1
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple16
The lion is rough.
("lion" "is" "rough" "+")
((triple10) -> (rule1 % int1))
The lion is rough.
("lion" "is" "rough" "+")
int1