The lion is kind. The lion is red. The lion is rough. The lion is round. The lion is young. The lion likes the tiger. The lion needs the tiger. The lion sees the tiger. The tiger is kind. The tiger is red. The tiger is rough. The tiger is round. The tiger is young. The tiger likes the lion. The tiger needs the lion. The tiger sees the lion. If something sees the lion and the lion needs the tiger then the tiger sees the lion. If something is kind and round then it likes the tiger. If the lion likes the tiger and the lion needs the tiger then the tiger needs the lion.
The lion is kind.
("lion" "is" "kind" "+")
The lion is red.
("lion" "is" "red" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is round.
("lion" "is" "round" "+")
The lion is young.
("lion" "is" "young" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The lion needs the tiger.
("lion" "needs" "tiger" "+")
The lion sees the tiger.
("lion" "sees" "tiger" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
The tiger sees the lion.
("tiger" "sees" "lion" "+")
If something sees the lion and the lion needs the tiger then the tiger sees the lion.
((("something" "sees" "lion" "+") ("lion" "needs" "tiger" "+")) -> ("tiger" "sees" "lion" "+"))
If something is kind and round then it likes the tiger.
((("something" "is" "kind" "+") ("something" "is" "round" "+")) -> ("something" "likes" "tiger" "+"))
If the lion likes the tiger and the lion needs the tiger then the tiger needs the lion.
((("lion" "likes" "tiger" "+") ("lion" "needs" "tiger" "+")) -> ("tiger" "needs" "lion" "+"))
The tiger is young.
True
1
proof
[(triple13)]
("tiger" "is" "young" "+")
triple13
The lion does not need the tiger.
False
1
inv-proof
[(triple7)]
("lion" "needs" "tiger" "-")
triple7
The lion does not like the lion.
Unknown
inv-random
[@0: The lion likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "lion" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The lion is kind.[(triple1)] The lion is red.[(triple2)] The lion is rough.[(triple3)] The lion is round.[(triple4)] The lion is young.[(triple5)] The lion likes the tiger.[(triple6 OR ((triple1 triple4) -> rule2))] The lion needs the tiger.[(triple7)] The lion sees the tiger.[(triple8)] The tiger is kind.[(triple9)] The tiger is red.[(triple10)] The tiger is rough.[(triple11)] The tiger is round.[(triple12)] The tiger is young.[(triple13)] The tiger likes the lion.[(triple14)] The tiger needs the lion.[(triple15 OR ((triple6 triple7) -> rule3) OR ((((triple1 triple4) -> rule2) triple7) -> rule3))] The tiger sees the lion.[(triple16)] @1: The tiger likes the tiger.[(((triple9 triple12) -> rule2))]
The lion is kind.
("lion" "is" "kind" "+")
triple1
The lion is red.
("lion" "is" "red" "+")
triple2
The lion is rough.
("lion" "is" "rough" "+")
triple3
The lion is round.
("lion" "is" "round" "+")
triple4
The lion is young.
("lion" "is" "young" "+")
triple5
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple6
((triple1 triple4) -> (rule2 % int1))
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int1
The lion needs the tiger.
("lion" "needs" "tiger" "+")
triple7
The lion sees the tiger.
("lion" "sees" "tiger" "+")
triple8
The tiger is kind.
("tiger" "is" "kind" "+")
triple9
The tiger is red.
("tiger" "is" "red" "+")
triple10
The tiger is rough.
("tiger" "is" "rough" "+")
triple11
The tiger is round.
("tiger" "is" "round" "+")
triple12
The tiger is young.
("tiger" "is" "young" "+")
triple13
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple14
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple15
((triple6 triple7) -> (rule3 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
((((triple1 triple4) -> (rule2 % int2)) triple7) -> (rule3 % int1))
The tiger needs the lion.
("tiger" "needs" "lion" "+")
int1
The lion likes the tiger.
("lion" "likes" "tiger" "+")
int2
The tiger sees the lion.
("tiger" "sees" "lion" "+")
triple16
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((triple9 triple12) -> (rule2 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1