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