The cat is big. The lion likes the squirrel. The mouse likes the lion. The squirrel does not chase the mouse. If someone visits the lion then they are nice. If someone visits the squirrel and they are not rough then they are nice. If someone likes the squirrel then they visit the cat. If someone visits the lion and the lion visits the cat then the cat does not like the lion. If someone likes the squirrel then the squirrel visits the mouse. If someone visits the cat then the cat does not visit the lion.
The cat is big.
("cat" "is" "big" "+")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
The squirrel does not chase the mouse.
("squirrel" "chases" "mouse" "-")
If someone visits the lion then they are nice.
((("someone" "visits" "lion" "+")) -> ("someone" "is" "nice" "+"))
If someone visits the squirrel and they are not rough then they are nice.
((("someone" "visits" "squirrel" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "nice" "+"))
If someone likes the squirrel then they visit the cat.
((("someone" "likes" "squirrel" "+")) -> ("someone" "visits" "cat" "+"))
If someone visits the lion and the lion visits the cat then the cat does not like the lion.
((("someone" "visits" "lion" "+") ("lion" "visits" "cat" "+")) -> ("cat" "likes" "lion" "-"))
If someone likes the squirrel then the squirrel visits the mouse.
((("someone" "likes" "squirrel" "+")) -> ("squirrel" "visits" "mouse" "+"))
If someone visits the cat then the cat does not visit the lion.
((("someone" "visits" "cat" "+")) -> ("cat" "visits" "lion" "-"))
The lion likes the squirrel.
True
1
proof
[(triple2)]
("lion" "likes" "squirrel" "+")
triple2
The squirrel chases the mouse.
False
1
inv-proof
[(triple4)]
("squirrel" "chases" "mouse" "+")
triple4
The lion visits the cat.
True
2
proof
[(((triple2) -> rule3))]
("lion" "visits" "cat" "+")
((triple2) -> (rule3 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The squirrel does not visit the mouse.
False
2
inv-proof
[(((triple2) -> rule5))]
("squirrel" "visits" "mouse" "-")
((triple2) -> (rule5 % int1))
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int1
The cat does not visit the lion.
True
3
proof
[(((((triple2) -> rule3)) -> rule6))]
("cat" "visits" "lion" "-")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The cat does not visit the lion.
("cat" "visits" "lion" "-")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The cat visits the lion.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule6))]
("cat" "visits" "lion" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The cat does not visit the lion.
("cat" "visits" "lion" "-")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The cat is not nice.
Unknown
inv-rconc
[@1: The cat is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "nice" "-")
The mouse is nice.
Unknown
rconc
[@1: The mouse is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "nice" "+")
The lion is not nice.
Unknown
inv-rconc
[@1: The lion is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "nice" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
The squirrel is not rough.
Unknown
inv-random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "-")
The lion likes the cat.
Unknown
random
[@0: The lion likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "cat" "+")
@0: The cat is big.[(triple1)] The lion likes the squirrel.[(triple2)] The mouse likes the lion.[(triple3)] The squirrel does not chase the mouse.[(triple4)] @1: The lion visits the cat.[(((triple2) -> rule3))] The squirrel visits the mouse.[(((triple2) -> rule5))] @2: The cat does not visit the lion.[(((((triple2) -> rule3)) -> rule6))]
The cat is big.
("cat" "is" "big" "+")
triple1
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple2
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple3
The squirrel does not chase the mouse.
("squirrel" "chases" "mouse" "-")
triple4
The lion visits the cat.
("lion" "visits" "cat" "+")
((triple2) -> (rule3 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
((triple2) -> (rule5 % int1))
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
int1
The cat does not visit the lion.
("cat" "visits" "lion" "-")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The cat does not visit the lion.
("cat" "visits" "lion" "-")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2