The cow chases the lion. The cow chases the squirrel. The cow likes the mouse. The cow visits the lion. The lion chases the cow. The lion chases the squirrel. The lion is nice. The lion likes the squirrel. The mouse chases the cow. The mouse is big. The mouse is green. The mouse likes the lion. The mouse visits the lion. The squirrel is green. The squirrel is nice. The squirrel is round. If someone likes the lion then the lion is round. If someone visits the squirrel and they are round then the squirrel is cold. If someone chases the cow and they like the cow then the cow chases the squirrel. If someone is round then they chase the mouse. If someone is nice then they visit the lion. If someone visits the cow then they like the mouse.
The cow chases the lion.
("cow" "chases" "lion" "+")
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
The cow likes the mouse.
("cow" "likes" "mouse" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The lion chases the cow.
("lion" "chases" "cow" "+")
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
The mouse chases the cow.
("mouse" "chases" "cow" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
If someone likes the lion then the lion is round.
((("someone" "likes" "lion" "+")) -> ("lion" "is" "round" "+"))
If someone visits the squirrel and they are round then the squirrel is cold.
((("someone" "visits" "squirrel" "+") ("someone" "is" "round" "+")) -> ("squirrel" "is" "cold" "+"))
If someone chases the cow and they like the cow then the cow chases the squirrel.
((("someone" "chases" "cow" "+") ("someone" "likes" "cow" "+")) -> ("cow" "chases" "squirrel" "+"))
If someone is round then they chase the mouse.
((("someone" "is" "round" "+")) -> ("someone" "chases" "mouse" "+"))
If someone is nice then they visit the lion.
((("someone" "is" "nice" "+")) -> ("someone" "visits" "lion" "+"))
If someone visits the cow then they like the mouse.
((("someone" "visits" "cow" "+")) -> ("someone" "likes" "mouse" "+"))
The mouse chases the cow.
True
1
proof
[(triple9)]
("mouse" "chases" "cow" "+")
triple9
The cow does not chase the squirrel.
False
1
inv-proof
[(triple2)]
("cow" "chases" "squirrel" "-")
triple2
The lion is round.
True
2
proof
[(((triple12) -> rule1))]
("lion" "is" "round" "+")
((triple12) -> (rule1 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The squirrel does not chase the mouse.
False
2
inv-proof
[(((triple16) -> rule4))]
("squirrel" "chases" "mouse" "-")
((triple16) -> (rule4 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The lion chases the mouse.
True
3
proof
[(((((triple12) -> rule1)) -> rule4))]
("lion" "chases" "mouse" "+")
((((triple12) -> (rule1 % int2))) -> (rule4 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The lion does not chase the mouse.
False
3
inv-proof
[(((((triple12) -> rule1)) -> rule4))]
("lion" "chases" "mouse" "-")
((((triple12) -> (rule1 % int2))) -> (rule4 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2
The squirrel does not like the mouse.
Unknown
inv-rconc
[@1: The squirrel likes the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "likes" "mouse" "-")
The mouse chases the mouse.
Unknown
rconc
[@1: The mouse chases the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "chases" "mouse" "+")
The lion does not like the mouse.
Unknown
inv-rconc
[@1: The lion likes the mouse.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "likes" "mouse" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
The lion is not green.
Unknown
inv-random
[@0: The lion is green.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "green" "-")
The cow is round.
Unknown
random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "+")
@0: The cow chases the lion.[(triple1)] The cow chases the squirrel.[(triple2)] The cow likes the mouse.[(triple3)] The cow visits the lion.[(triple4)] The lion chases the cow.[(triple5)] The lion chases the squirrel.[(triple6)] The lion is nice.[(triple7)] The lion likes the squirrel.[(triple8)] The mouse chases the cow.[(triple9)] The mouse is big.[(triple10)] The mouse is green.[(triple11)] The mouse likes the lion.[(triple12)] The mouse visits the lion.[(triple13)] The squirrel is green.[(triple14)] The squirrel is nice.[(triple15)] The squirrel is round.[(triple16)] @1: The lion is round.[(((triple12) -> rule1))] The lion visits the lion.[(((triple7) -> rule5))] The squirrel chases the mouse.[(((triple16) -> rule4))] The squirrel visits the lion.[(((triple15) -> rule5))] @2: The lion chases the mouse.[(((((triple12) -> rule1)) -> rule4))]
The cow chases the lion.
("cow" "chases" "lion" "+")
triple1
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
triple2
The cow likes the mouse.
("cow" "likes" "mouse" "+")
triple3
The cow visits the lion.
("cow" "visits" "lion" "+")
triple4
The lion chases the cow.
("lion" "chases" "cow" "+")
triple5
The lion chases the squirrel.
("lion" "chases" "squirrel" "+")
triple6
The lion is nice.
("lion" "is" "nice" "+")
triple7
The lion likes the squirrel.
("lion" "likes" "squirrel" "+")
triple8
The mouse chases the cow.
("mouse" "chases" "cow" "+")
triple9
The mouse is big.
("mouse" "is" "big" "+")
triple10
The mouse is green.
("mouse" "is" "green" "+")
triple11
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple12
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple13
The squirrel is green.
("squirrel" "is" "green" "+")
triple14
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple15
The squirrel is round.
("squirrel" "is" "round" "+")
triple16
The lion is round.
("lion" "is" "round" "+")
((triple12) -> (rule1 % int1))
The lion is round.
("lion" "is" "round" "+")
int1
The lion visits the lion.
("lion" "visits" "lion" "+")
((triple7) -> (rule5 % int1))
The lion visits the lion.
("lion" "visits" "lion" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
((triple16) -> (rule4 % int1))
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
int1
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
((triple15) -> (rule5 % int1))
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
int1
The lion chases the mouse.
("lion" "chases" "mouse" "+")
((((triple12) -> (rule1 % int2))) -> (rule4 % int1))
The lion chases the mouse.
("lion" "chases" "mouse" "+")
int1
The lion is round.
("lion" "is" "round" "+")
int2