The lion is big. The lion is kind. The lion is nice. The lion is round. The lion is young. The lion likes the tiger. The lion does not need the tiger. The lion visits the tiger. The tiger is big. The tiger is kind. The tiger is nice. The tiger is not young. The tiger likes the lion. The tiger needs the lion. The tiger visits the lion. If someone is young then they visit the lion.
The lion is big.
("lion" "is" "big" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is round.
("lion" "is" "round" "+")
The lion is young.
("lion" "is" "young" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The lion does not need the tiger.
("lion" "needs" "tiger" "-")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is not young.
("tiger" "is" "young" "-")
The tiger likes the lion.
("tiger" "likes" "lion" "+")
The tiger needs the lion.
("tiger" "needs" "lion" "+")
The tiger visits the lion.
("tiger" "visits" "lion" "+")
If someone is young then they visit the lion.
((("someone" "is" "young" "+")) -> ("someone" "visits" "lion" "+"))
The lion is big.
True
1
proof
[(triple1)]
("lion" "is" "big" "+")
triple1
The lion is not kind.
False
1
inv-proof
[(triple2)]
("lion" "is" "kind" "-")
triple2
The lion visits the lion.
True
2
proof
[(((triple5) -> rule1))]
("lion" "visits" "lion" "+")
((triple5) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The lion does not visit the lion.
False
2
inv-proof
[(((triple5) -> rule1))]
("lion" "visits" "lion" "-")
((triple5) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
@0: The lion does not need the tiger.[(triple7)] The lion is big.[(triple1)] The lion is kind.[(triple2)] The lion is nice.[(triple3)] The lion is round.[(triple4)] The lion is young.[(triple5)] The lion likes the tiger.[(triple6)] The lion visits the tiger.[(triple8)] The tiger is big.[(triple9)] The tiger is kind.[(triple10)] The tiger is nice.[(triple11)] The tiger is not young.[(triple12)] The tiger likes the lion.[(triple13)] The tiger needs the lion.[(triple14)] The tiger visits the lion.[(triple15)] @1: The lion visits the lion.[(((triple5) -> rule1))]
The lion does not need the tiger.
("lion" "needs" "tiger" "-")
triple7
The lion is big.
("lion" "is" "big" "+")
triple1
The lion is kind.
("lion" "is" "kind" "+")
triple2
The lion is nice.
("lion" "is" "nice" "+")
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
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple8
The tiger is big.
("tiger" "is" "big" "+")
triple9
The tiger is kind.
("tiger" "is" "kind" "+")
triple10
The tiger is nice.
("tiger" "is" "nice" "+")
triple11
The tiger is not young.
("tiger" "is" "young" "-")
triple12
The tiger likes the lion.
("tiger" "likes" "lion" "+")
triple13
The tiger needs the lion.
("tiger" "needs" "lion" "+")
triple14
The tiger visits the lion.
("tiger" "visits" "lion" "+")
triple15
The lion visits the lion.
("lion" "visits" "lion" "+")
((triple5) -> (rule1 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1