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