The mouse chases the rabbit. The mouse is big. The mouse is kind. The mouse is nice. The mouse is round. The mouse is young. The mouse needs the rabbit. The mouse sees the rabbit. The rabbit chases the mouse. The rabbit is big. The rabbit is kind. The rabbit is nice. The rabbit is round. The rabbit is young. The rabbit needs the mouse. The rabbit does not see the mouse. If something is round then it chases the mouse. If something is kind then it does not see the mouse. If something is nice then it does not see the mouse. If something is round and it needs the rabbit then it does not need the mouse. If something is kind and it sees the rabbit then the rabbit chases the mouse. If something needs the rabbit then the rabbit is young. If something needs the mouse and it chases the rabbit then the rabbit sees the mouse. If something chases the rabbit and it is not young then the rabbit sees the mouse.
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
The rabbit does not see the mouse.
("rabbit" "sees" "mouse" "-")
If something is round then it chases the mouse.
((("something" "is" "round" "+")) -> ("something" "chases" "mouse" "+"))
If something is kind then it does not see the mouse.
((("something" "is" "kind" "+")) -> ("something" "sees" "mouse" "-"))
If something is nice then it does not see the mouse.
((("something" "is" "nice" "+")) -> ("something" "sees" "mouse" "-"))
If something is round and it needs the rabbit then it does not need the mouse.
((("something" "is" "round" "+") ("something" "needs" "rabbit" "+")) -> ("something" "needs" "mouse" "-"))
If something is kind and it sees the rabbit then the rabbit chases the mouse.
((("something" "is" "kind" "+") ("something" "sees" "rabbit" "+")) -> ("rabbit" "chases" "mouse" "+"))
If something needs the rabbit then the rabbit is young.
((("something" "needs" "rabbit" "+")) -> ("rabbit" "is" "young" "+"))
If something needs the mouse and it chases the rabbit then the rabbit sees the mouse.
((("something" "needs" "mouse" "+") ("something" "chases" "rabbit" "+")) -> ("rabbit" "sees" "mouse" "+"))
If something chases the rabbit and it is not young then the rabbit sees the mouse.
((("something" "chases" "rabbit" "+") ("something" "is" "young" "~")) -> ("rabbit" "sees" "mouse" "+"))
The mouse sees the rabbit.
True
1
proof
[(triple8)]
("mouse" "sees" "rabbit" "+")
triple8
The mouse is not nice.
False
1
inv-proof
[(triple4)]
("mouse" "is" "nice" "-")
triple4
The rabbit does not chase the rabbit.
Unknown
inv-random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
@0: The mouse chases the rabbit.[(triple1)] The mouse is big.[(triple2)] The mouse is kind.[(triple3)] The mouse is nice.[(triple4)] The mouse is round.[(triple5)] The mouse is young.[(triple6)] The mouse needs the rabbit.[(triple7)] The mouse sees the rabbit.[(triple8)] The rabbit chases the mouse.[(triple9 OR ((triple13) -> rule1) OR ((triple3 triple8) -> rule5))] The rabbit does not see the mouse.[(triple16 OR ((triple11) -> rule2) OR ((triple12) -> rule3))] The rabbit is big.[(triple10)] The rabbit is kind.[(triple11)] The rabbit is nice.[(triple12)] The rabbit is round.[(triple13)] The rabbit is young.[(triple14 OR ((triple7) -> rule6))] The rabbit needs the mouse.[(triple15)] @1: The mouse chases the mouse.[(((triple5) -> rule1))] The mouse does not need the mouse.[(((triple5 triple7) -> rule4))] The mouse does not see the mouse.[(((triple3) -> rule2) OR ((triple4) -> rule3))]
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple1
The mouse is big.
("mouse" "is" "big" "+")
triple2
The mouse is kind.
("mouse" "is" "kind" "+")
triple3
The mouse is nice.
("mouse" "is" "nice" "+")
triple4
The mouse is round.
("mouse" "is" "round" "+")
triple5
The mouse is young.
("mouse" "is" "young" "+")
triple6
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple7
The mouse sees the rabbit.
("mouse" "sees" "rabbit" "+")
triple8
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple9
((triple13) -> (rule1 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
((triple3 triple8) -> (rule5 % int1))
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
int1
The rabbit does not see the mouse.
("rabbit" "sees" "mouse" "-")
triple16
((triple11) -> (rule2 % int1))
The rabbit does not see the mouse.
("rabbit" "sees" "mouse" "-")
int1
((triple12) -> (rule3 % int1))
The rabbit does not see the mouse.
("rabbit" "sees" "mouse" "-")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
triple10
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple11
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple12
The rabbit is round.
("rabbit" "is" "round" "+")
triple13
The rabbit is young.
("rabbit" "is" "young" "+")
triple14
((triple7) -> (rule6 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit needs the mouse.
("rabbit" "needs" "mouse" "+")
triple15
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((triple5) -> (rule1 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse does not need the mouse.
("mouse" "needs" "mouse" "-")
((triple5 triple7) -> (rule4 % int1))
The mouse does not need the mouse.
("mouse" "needs" "mouse" "-")
int1
The mouse does not see the mouse.
("mouse" "sees" "mouse" "-")
((triple3) -> (rule2 % int1))
The mouse does not see the mouse.
("mouse" "sees" "mouse" "-")
int1
((triple4) -> (rule3 % int1))
The mouse does not see the mouse.
("mouse" "sees" "mouse" "-")
int1