The lion eats the tiger. The lion is blue. The lion is cold. The lion is red. The lion is rough. The lion is young. The lion needs the tiger. The lion sees the tiger. The tiger eats the lion. The tiger is blue. The tiger is cold. The tiger is red. The tiger is rough. The tiger needs the lion. The tiger does not see the lion. If the tiger eats the lion and the lion is rough then the lion eats the tiger. If something is young then it needs the lion. If the tiger sees the lion and the lion does not see the tiger then the lion is not blue. If something needs the lion and the lion eats the tiger then it eats the lion. If something needs the tiger and the tiger does not eat the lion then the tiger is cold. If something sees the tiger and the tiger sees the lion then the tiger is cold.
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is young.
("lion" "is" "young" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
The tiger does not see the lion.
("tiger" "sees" "lion" "-")
If the tiger eats the lion and the lion is rough then the lion eats the tiger.
((("tiger" "eats" "lion" "+") ("lion" "is" "rough" "+")) -> ("lion" "eats" "tiger" "+"))
If something is young then it needs the lion.
((("something" "is" "young" "+")) -> ("something" "needs" "lion" "+"))
If the tiger sees the lion and the lion does not see the tiger then the lion is not blue.
((("tiger" "sees" "lion" "+") ("lion" "sees" "tiger" "~")) -> ("lion" "is" "blue" "-"))
If something needs the lion and the lion eats the tiger then it eats the lion.
((("something" "needs" "lion" "+") ("lion" "eats" "tiger" "+")) -> ("something" "eats" "lion" "+"))
If something needs the tiger and the tiger does not eat the lion then the tiger is cold.
((("something" "needs" "tiger" "+") ("tiger" "eats" "lion" "~")) -> ("tiger" "is" "cold" "+"))
If something sees the tiger and the tiger sees the lion then the tiger is cold.
((("something" "sees" "tiger" "+") ("tiger" "sees" "lion" "+")) -> ("tiger" "is" "cold" "+"))
The lion is cold.
True
1
proof
[(triple3)]
("lion" "is" "cold" "+")
triple3
The tiger does not eat the lion.
False
1
inv-proof
[(triple9 OR ((triple14 triple1) -> rule4))]
("tiger" "eats" "lion" "-")
triple9
((triple14 triple1) -> (rule4 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1
The lion needs the lion.
True
2
proof
[(((triple6) -> rule2))]
("lion" "needs" "lion" "+")
((triple6) -> (rule2 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion does not need the lion.
False
2
inv-proof
[(((triple6) -> rule2))]
("lion" "needs" "lion" "-")
((triple6) -> (rule2 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion eats the lion.
True
4
proof
[(((((triple6) -> rule2) triple1) -> rule4) OR ((((triple6) -> rule2) ((triple9 triple5) -> rule1)) -> rule4))]
("lion" "eats" "lion" "+")
((((triple6) -> (rule2 % int2)) triple1) -> (rule4 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
((((triple6) -> (rule2 % int3)) ((triple9 triple5) -> (rule1 % int2))) -> (rule4 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
int3
The lion does not eat the lion.
False
4
inv-proof
[(((((triple6) -> rule2) triple1) -> rule4) OR ((((triple6) -> rule2) ((triple9 triple5) -> rule1)) -> rule4))]
("lion" "eats" "lion" "-")
((((triple6) -> (rule2 % int2)) triple1) -> (rule4 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
((((triple6) -> (rule2 % int3)) ((triple9 triple5) -> (rule1 % int2))) -> (rule4 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
int3
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The tiger is young.
Unknown
random
[@0: The tiger is young.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "young" "+")
@0: The lion eats the tiger.[(triple1 OR ((triple9 triple5) -> rule1))] The lion is blue.[(triple2)] The lion is cold.[(triple3)] The lion is red.[(triple4)] The lion is rough.[(triple5)] The lion is young.[(triple6)] The lion needs the tiger.[(triple7)] The lion sees the tiger.[(triple8)] The tiger does not see the lion.[(triple15)] The tiger eats the lion.[(triple9 OR ((triple14 triple1) -> rule4))] The tiger is blue.[(triple10)] The tiger is cold.[(triple11)] The tiger is red.[(triple12)] The tiger is rough.[(triple13)] The tiger needs the lion.[(triple14)] @1: The lion needs the lion.[(((triple6) -> rule2))] @2: The lion eats the lion.[(((((triple6) -> rule2) triple1) -> rule4) OR ((((triple6) -> rule2) ((triple9 triple5) -> rule1)) -> rule4))]
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple1
((triple9 triple5) -> (rule1 % int1))
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int1
The lion is blue.
("lion" "is" "blue" "+")
triple2
The lion is cold.
("lion" "is" "cold" "+")
triple3
The lion is red.
("lion" "is" "red" "+")
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 sees the tiger.
("lion" "sees" "tiger" "+")
triple8
The tiger does not see the lion.
("tiger" "sees" "lion" "-")
triple15
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple9
((triple14 triple1) -> (rule4 % int1))
The tiger eats the lion.
("tiger" "eats" "lion" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
triple10
The tiger is cold.
("tiger" "is" "cold" "+")
triple11
The tiger is red.
("tiger" "is" "red" "+")
triple12
The tiger is rough.
("tiger" "is" "rough" "+")
triple13
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple14
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple6) -> (rule2 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
((((triple6) -> (rule2 % int2)) triple1) -> (rule4 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
((((triple6) -> (rule2 % int3)) ((triple9 triple5) -> (rule1 % int2))) -> (rule4 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
int3