The mouse chases the rabbit. The mouse is blue. The mouse is nice. The mouse is round. The mouse sees the rabbit. The mouse visits the rabbit. The rabbit is kind. The rabbit is nice. The rabbit is round. The rabbit visits the mouse. If something chases the rabbit then it chases the mouse.
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If something chases the rabbit then it chases the mouse.
((("something" "chases" "rabbit" "+")) -> ("something" "chases" "mouse" "+"))
The mouse is nice.
True
1
proof
[(triple3)]
("mouse" "is" "nice" "+")
triple3
The mouse does not visit the rabbit.
False
1
inv-proof
[(triple6)]
("mouse" "visits" "rabbit" "-")
triple6
The mouse chases the mouse.
True
2
proof
[(((triple1) -> rule1))]
("mouse" "chases" "mouse" "+")
((triple1) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse does not chase the mouse.
False
2
inv-proof
[(((triple1) -> rule1))]
("mouse" "chases" "mouse" "-")
((triple1) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
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 rabbit is rough.
Unknown
random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "+")
The rabbit does not see the mouse.
Unknown
inv-random
[@0: The rabbit sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "mouse" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
@0: The mouse chases the rabbit.[(triple1)] The mouse is blue.[(triple2)] The mouse is nice.[(triple3)] The mouse is round.[(triple4)] The mouse sees the rabbit.[(triple5)] The mouse visits the rabbit.[(triple6)] The rabbit is kind.[(triple7)] The rabbit is nice.[(triple8)] The rabbit is round.[(triple9)] The rabbit visits the mouse.[(triple10)] @1: The mouse chases the mouse.[(((triple1) -> rule1))]
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple1
The mouse is blue.
("mouse" "is" "blue" "+")
triple2
The mouse is nice.
("mouse" "is" "nice" "+")
triple3
The mouse is round.
("mouse" "is" "round" "+")
triple4
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple5
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple6
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple7
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple8
The rabbit is round.
("rabbit" "is" "round" "+")
triple9
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple10
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((triple1) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1