The mouse is not big. The mouse is cold. The mouse is kind. The mouse is not red. The mouse likes the rabbit. The mouse sees the rabbit. The mouse visits the rabbit. The rabbit is big. The rabbit is not cold. The rabbit is kind. The rabbit is nice. The rabbit is red. The rabbit does not like the mouse. The rabbit sees the mouse. The rabbit visits the mouse. If something is cold and nice then it visits the mouse. If something sees the mouse then it visits the mouse. If something visits the rabbit and it is not red then it is nice. If something likes the rabbit and the rabbit visits the mouse then the mouse sees the rabbit. If something is red and it sees the rabbit then the rabbit is not cold. If the rabbit does not see the mouse then the rabbit visits the mouse.
The mouse is not big.
("mouse" "is" "big" "-")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is not red.
("mouse" "is" "red" "-")
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is not cold.
("rabbit" "is" "cold" "-")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit does not like the mouse.
("rabbit" "likes" "mouse" "-")
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
If something is cold and nice then it visits the mouse.
((("something" "is" "cold" "+") ("something" "is" "nice" "+")) -> ("something" "visits" "mouse" "+"))
If something sees the mouse then it visits the mouse.
((("something" "sees" "mouse" "+")) -> ("something" "visits" "mouse" "+"))
If something visits the rabbit and it is not red then it is nice.
((("something" "visits" "rabbit" "+") ("something" "is" "red" "~")) -> ("something" "is" "nice" "+"))
If something likes the rabbit and the rabbit visits the mouse then the mouse sees the rabbit.
((("something" "likes" "rabbit" "+") ("rabbit" "visits" "mouse" "+")) -> ("mouse" "sees" "rabbit" "+"))
If something is red and it sees the rabbit then the rabbit is not cold.
((("something" "is" "red" "+") ("something" "sees" "rabbit" "+")) -> ("rabbit" "is" "cold" "-"))
If the rabbit does not see the mouse then the rabbit visits the mouse.
((("rabbit" "sees" "mouse" "~")) -> ("rabbit" "visits" "mouse" "+"))
The rabbit is red.
True
1
proof
[(triple12)]
("rabbit" "is" "red" "+")
triple12
The rabbit is not red.
False
1
inv-proof
[(triple12)]
("rabbit" "is" "red" "-")
triple12
The mouse is nice.
True
3
proof
[(((triple7 triple4) -> rule3))]
("mouse" "is" "nice" "+")
((triple7 triple4) -> (rule3 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse is not nice.
False
3
inv-proof
[(((triple7 triple4) -> rule3))]
("mouse" "is" "nice" "-")
((triple7 triple4) -> (rule3 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse visits the mouse.
True
5
proof
[(((triple2 ((triple7 triple4) -> rule3)) -> rule1))]
("mouse" "visits" "mouse" "+")
((triple2 ((triple7 triple4) -> (rule3 % int2))) -> (rule1 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The mouse does not visit the mouse.
False
5
inv-proof
[(((triple2 ((triple7 triple4) -> rule3)) -> rule1))]
("mouse" "visits" "mouse" "-")
((triple2 ((triple7 triple4) -> (rule3 % int2))) -> (rule1 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2
The rabbit does not like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
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 mouse likes the mouse.
Unknown
random
[@0: The mouse likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "mouse" "+")
@0: The mouse is cold.[(triple2)] The mouse is kind.[(triple3)] The mouse is not big.[(triple1)] The mouse is not red.[(triple4)] The mouse likes the rabbit.[(triple5)] The mouse sees the rabbit.[(triple6 OR ((triple5 triple15) -> rule4) OR ((triple5 ((triple14) -> rule2)) -> rule4))] The mouse visits the rabbit.[(triple7)] The rabbit does not like the mouse.[(triple13)] The rabbit is big.[(triple8)] The rabbit is kind.[(triple10)] The rabbit is nice.[(triple11)] The rabbit is not cold.[(triple9)] The rabbit is red.[(triple12)] The rabbit sees the mouse.[(triple14)] The rabbit visits the mouse.[(triple15 OR ((triple14) -> rule2))] @1: The mouse is nice.[(((triple7 triple4) -> rule3))] @2: The mouse visits the mouse.[(((triple2 ((triple7 triple4) -> rule3)) -> rule1))]
The mouse is cold.
("mouse" "is" "cold" "+")
triple2
The mouse is kind.
("mouse" "is" "kind" "+")
triple3
The mouse is not big.
("mouse" "is" "big" "-")
triple1
The mouse is not red.
("mouse" "is" "red" "-")
triple4
The mouse likes the rabbit.
("mouse" "likes" "rabbit" "+")
triple5
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple6
((triple5 triple15) -> (rule4 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
((triple5 ((triple14) -> (rule2 % int2))) -> (rule4 % int1))
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
int1
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int2
The mouse visits the rabbit.
("mouse" "visits" "rabbit" "+")
triple7
The rabbit does not like the mouse.
("rabbit" "likes" "mouse" "-")
triple13
The rabbit is big.
("rabbit" "is" "big" "+")
triple8
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple10
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple11
The rabbit is not cold.
("rabbit" "is" "cold" "-")
triple9
The rabbit is red.
("rabbit" "is" "red" "+")
triple12
The rabbit sees the mouse.
("rabbit" "sees" "mouse" "+")
triple14
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
triple15
((triple14) -> (rule2 % int1))
The rabbit visits the mouse.
("rabbit" "visits" "mouse" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
((triple7 triple4) -> (rule3 % int1))
The mouse is nice.
("mouse" "is" "nice" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((triple2 ((triple7 triple4) -> (rule3 % int2))) -> (rule1 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The mouse is nice.
("mouse" "is" "nice" "+")
int2