The mouse visits the rabbit. The rabbit visits the mouse. If something chases the rabbit and it sees the mouse then the mouse is cold. If something chases the mouse then it visits the rabbit. If the rabbit visits the mouse then the rabbit sees the mouse. If something is young and cold then it is red. If something visits the mouse and it chases the mouse then it chases the rabbit. If something is red then it sees the rabbit. If the rabbit sees the mouse then the rabbit is red. If something chases the mouse and the mouse visits the rabbit then the mouse sees the rabbit.
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If something chases the rabbit and it sees the mouse then the mouse is cold.
((("something" "chases" "rabbit" "+") ("something" "sees" "mouse" "+")) -> ("mouse" "is" "cold" "+"))
If something chases the mouse then it visits the rabbit.
((("something" "chases" "mouse" "+")) -> ("something" "visits" "rabbit" "+"))
If the rabbit visits the mouse then the rabbit sees the mouse.
((("rabbit" "visits" "mouse" "+")) -> ("rabbit" "sees" "mouse" "+"))
If something is young and cold then it is red.
((("something" "is" "young" "+") ("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If something visits the mouse and it chases the mouse then it chases the rabbit.
((("something" "visits" "mouse" "+") ("something" "chases" "mouse" "+")) -> ("something" "chases" "rabbit" "+"))
If something is red then it sees the rabbit.
((("something" "is" "red" "+")) -> ("something" "sees" "rabbit" "+"))
If the rabbit sees the mouse then the rabbit is red.
((("rabbit" "sees" "mouse" "+")) -> ("rabbit" "is" "red" "+"))
If something chases the mouse and the mouse visits the rabbit then the mouse sees the rabbit.
((("something" "chases" "mouse" "+") ("mouse" "visits" "rabbit" "+")) -> ("mouse" "sees" "rabbit" "+"))
The mouse visits the rabbit.
True
1
proof
[(triple1)]
("mouse" "visits" "rabbit" "+")
triple1
The mouse does not visit the rabbit.
False
1
inv-proof
[(triple1)]
("mouse" "visits" "rabbit" "-")
triple1
The rabbit sees the mouse.
True
2
proof
[(((triple2) -> rule3))]
("rabbit" "sees" "mouse" "+")
((triple2) -> (rule3 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit does not see the mouse.
False
2
inv-proof
[(((triple2) -> rule3))]
("rabbit" "sees" "mouse" "-")
((triple2) -> (rule3 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit is red.
True
3
proof
[(((((triple2) -> rule3)) -> rule7))]
("rabbit" "is" "red" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int2
The rabbit is not red.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule7))]
("rabbit" "is" "red" "-")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int2
The mouse is not cold.
Unknown
inv-rconc
[@2: The mouse is cold.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("mouse" "is" "cold" "-")
The rabbit visits the rabbit.
Unknown
rconc
[@1: The rabbit visits the rabbit.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "visits" "rabbit" "+")
The mouse does not chase the rabbit.
Unknown
inv-rconc
[@1: The mouse chases the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "chases" "rabbit" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The mouse is blue.
Unknown
random
[@0: The mouse is blue.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "blue" "+")
@0: The mouse visits the rabbit.[(triple1)] The rabbit visits the mouse.[(triple2)] @1: The rabbit sees the mouse.[(((triple2) -> rule3))] @2: The rabbit is red.[(((((triple2) -> rule3)) -> rule7))] @3: The rabbit sees the rabbit.[(((((((triple2) -> rule3)) -> rule7)) -> rule6))]
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple1
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple2
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
((triple2) -> (rule3 % int1))
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int2
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((((((triple2) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
int3