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