The lion chases the mouse. The lion chases the rabbit. The lion is big. The lion is nice. The lion is round. The lion likes the mouse. The lion needs the mouse. The lion needs the rabbit. The mouse chases the rabbit. The mouse is blue. The mouse is round. The rabbit chases the mouse. The rabbit is blue. The rabbit likes the mouse. The rabbit needs the lion. If someone is round and they chase the mouse then they are blue.
The lion chases the mouse.
("lion" "chases" "mouse" "+")
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is round.
("lion" "is" "round" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion needs the mouse.
("lion" "needs" "mouse" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is round.
("mouse" "is" "round" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
If someone is round and they chase the mouse then they are blue.
((("someone" "is" "round" "+") ("someone" "chases" "mouse" "+")) -> ("someone" "is" "blue" "+"))
The rabbit chases the mouse.
True
1
proof
[(triple12)]
("rabbit" "chases" "mouse" "+")
triple12
The lion does not chase the rabbit.
False
1
inv-proof
[(triple2)]
("lion" "chases" "rabbit" "-")
triple2
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
@0: The lion chases the mouse.[(triple1)] The lion chases the rabbit.[(triple2)] The lion is big.[(triple3)] The lion is nice.[(triple4)] The lion is round.[(triple5)] The lion likes the mouse.[(triple6)] The lion needs the mouse.[(triple7)] The lion needs the rabbit.[(triple8)] The mouse chases the rabbit.[(triple9)] The mouse is blue.[(triple10)] The mouse is round.[(triple11)] The rabbit chases the mouse.[(triple12)] The rabbit is blue.[(triple13)] The rabbit likes the mouse.[(triple14)] The rabbit needs the lion.[(triple15)] @1: The lion is blue.[(((triple5 triple1) -> rule1))]
The lion chases the mouse.
("lion" "chases" "mouse" "+")
triple1
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple2
The lion is big.
("lion" "is" "big" "+")
triple3
The lion is nice.
("lion" "is" "nice" "+")
triple4
The lion is round.
("lion" "is" "round" "+")
triple5
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple6
The lion needs the mouse.
("lion" "needs" "mouse" "+")
triple7
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple8
The mouse chases the rabbit.
("mouse" "chases" "rabbit" "+")
triple9
The mouse is blue.
("mouse" "is" "blue" "+")
triple10
The mouse is round.
("mouse" "is" "round" "+")
triple11
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple12
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple13
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple14
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple15
The lion is blue.
("lion" "is" "blue" "+")
((triple5 triple1) -> (rule1 % int1))
The lion is blue.
("lion" "is" "blue" "+")
int1