The cat is round. The mouse eats the cat. The squirrel is nice. If something eats the cat then it likes the mouse. If something chases the cat then the cat is round. If something eats the mouse then the mouse likes the cat.
The cat is round.
("cat" "is" "round" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
If something eats the cat then it likes the mouse.
((("something" "eats" "cat" "+")) -> ("something" "likes" "mouse" "+"))
If something chases the cat then the cat is round.
((("something" "chases" "cat" "+")) -> ("cat" "is" "round" "+"))
If something eats the mouse then the mouse likes the cat.
((("something" "eats" "mouse" "+")) -> ("mouse" "likes" "cat" "+"))
The mouse eats the cat.
True
1
proof
[(triple2)]
("mouse" "eats" "cat" "+")
triple2
The mouse does not eat the cat.
False
1
inv-proof
[(triple2)]
("mouse" "eats" "cat" "-")
triple2
The mouse likes the mouse.
True
2
proof
[(((triple2) -> rule1))]
("mouse" "likes" "mouse" "+")
((triple2) -> (rule1 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse does not like the mouse.
False
2
inv-proof
[(((triple2) -> rule1))]
("mouse" "likes" "mouse" "-")
((triple2) -> (rule1 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The squirrel does not like the mouse.
Unknown
inv-rconc
[@1: The squirrel likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "likes" "mouse" "-")
The cat likes the mouse.
Unknown
rconc
[@1: The cat likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "mouse" "+")
The mouse does not like the squirrel.
Unknown
inv-random
[@0: The mouse likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "squirrel" "-")
The mouse eats the squirrel.
Unknown
random
[@0: The mouse eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "squirrel" "+")
@0: The cat is round.[(triple1)] The mouse eats the cat.[(triple2)] The squirrel is nice.[(triple3)] @1: The mouse likes the mouse.[(((triple2) -> rule1))]
The cat is round.
("cat" "is" "round" "+")
triple1
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple2
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple3
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((triple2) -> (rule1 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1