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