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