The bear visits the tiger. The lion is big. The lion is blue. The lion likes the tiger. The lion visits the tiger. The squirrel is green. The tiger is big. If someone likes the tiger then they are not green. If someone chases the bear and they are not cold then they do not like the squirrel.
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion likes the tiger.
("lion" "likes" "tiger" "+")
The lion visits the tiger.
("lion" "visits" "tiger" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The tiger is big.
("tiger" "is" "big" "+")
If someone likes the tiger then they are not green.
((("someone" "likes" "tiger" "+")) -> ("someone" "is" "green" "-"))
If someone chases the bear and they are not cold then they do not like the squirrel.
((("someone" "chases" "bear" "+") ("someone" "is" "cold" "~")) -> ("someone" "likes" "squirrel" "-"))
The lion likes the tiger.
True
1
proof
[(triple4)]
("lion" "likes" "tiger" "+")
triple4
The lion does not like the tiger.
False
1
inv-proof
[(triple4)]
("lion" "likes" "tiger" "-")
triple4
The lion is not green.
True
2
proof
[(((triple4) -> rule1))]
("lion" "is" "green" "-")
((triple4) -> (rule1 % int1))
The lion is not green.
("lion" "is" "green" "-")
int1
The lion is green.
False
2
inv-proof
[(((triple4) -> rule1))]
("lion" "is" "green" "+")
((triple4) -> (rule1 % int1))
The lion is not green.
("lion" "is" "green" "-")
int1
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 squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The tiger likes the lion.
Unknown
random
[@0: The tiger likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "lion" "+")
@0: The bear visits the tiger.[(triple1)] The lion is big.[(triple2)] The lion is blue.[(triple3)] The lion likes the tiger.[(triple4)] The lion visits the tiger.[(triple5)] The squirrel is green.[(triple6)] The tiger is big.[(triple7)] @1: The lion is not green.[(((triple4) -> rule1))]
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple1
The lion is big.
("lion" "is" "big" "+")
triple2
The lion is blue.
("lion" "is" "blue" "+")
triple3
The lion likes the tiger.
("lion" "likes" "tiger" "+")
triple4
The lion visits the tiger.
("lion" "visits" "tiger" "+")
triple5
The squirrel is green.
("squirrel" "is" "green" "+")
triple6
The tiger is big.
("tiger" "is" "big" "+")
triple7
The lion is not green.
("lion" "is" "green" "-")
((triple4) -> (rule1 % int1))
The lion is not green.
("lion" "is" "green" "-")
int1