The cow eats the lion. The cow is big. The cow is young. The lion is rough. The lion is young. The mouse chases the lion. The mouse eats the lion. The mouse is big. The mouse is rough. The mouse visits the cow. If something eats the cow and it visits the cow then it does not chase the mouse. If something chases the lion and the lion does not chase the cow then it is rough. If something visits the cow then it visits the lion. All round, rough things are red. If something is round then it eats the cow. If something visits the cow and it visits the mouse then it eats the cow. If something eats the lion and it is not young then it does not eat the cow. If something is big and it does not chase the lion then the lion does not visit the cow.
The cow eats the lion.
("cow" "eats" "lion" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is young.
("cow" "is" "young" "+")
The lion is rough.
("lion" "is" "rough" "+")
The lion is young.
("lion" "is" "young" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
If something eats the cow and it visits the cow then it does not chase the mouse.
((("something" "eats" "cow" "+") ("something" "visits" "cow" "+")) -> ("something" "chases" "mouse" "-"))
If something chases the lion and the lion does not chase the cow then it is rough.
((("something" "chases" "lion" "+") ("lion" "chases" "cow" "~")) -> ("something" "is" "rough" "+"))
If something visits the cow then it visits the lion.
((("something" "visits" "cow" "+")) -> ("something" "visits" "lion" "+"))
All round, rough things are red.
((("something" "is" "round" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If something is round then it eats the cow.
((("something" "is" "round" "+")) -> ("something" "eats" "cow" "+"))
If something visits the cow and it visits the mouse then it eats the cow.
((("something" "visits" "cow" "+") ("something" "visits" "mouse" "+")) -> ("something" "eats" "cow" "+"))
If something eats the lion and it is not young then it does not eat the cow.
((("something" "eats" "lion" "+") ("something" "is" "young" "~")) -> ("something" "eats" "cow" "-"))
If something is big and it does not chase the lion then the lion does not visit the cow.
((("something" "is" "big" "+") ("something" "chases" "lion" "~")) -> ("lion" "visits" "cow" "-"))
The cow is young.
True
1
proof
[(triple3)]
("cow" "is" "young" "+")
triple3
The lion is not young.
False
1
inv-proof
[(triple5)]
("lion" "is" "young" "-")
triple5
The mouse visits the lion.
True
2
proof
[(((triple10) -> rule3))]
("mouse" "visits" "lion" "+")
((triple10) -> (rule3 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
The mouse does not visit the lion.
False
2
inv-proof
[(((triple10) -> rule3))]
("mouse" "visits" "lion" "-")
((triple10) -> (rule3 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1
The cow does not visit the lion.
Unknown
inv-rconc
[@1: The cow visits the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "visits" "lion" "-")
The lion visits the lion.
Unknown
rconc
[@1: The lion visits the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "visits" "lion" "+")
The lion is not round.
Unknown
inv-random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "-")
The lion chases the cow.
Unknown
random
[@0: The lion chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "cow" "+")
@0: The cow eats the lion.[(triple1)] The cow is big.[(triple2)] The cow is young.[(triple3)] The lion is rough.[(triple4)] The lion is young.[(triple5)] The mouse chases the lion.[(triple6)] The mouse eats the lion.[(triple7)] The mouse is big.[(triple8)] The mouse is rough.[(triple9)] The mouse visits the cow.[(triple10)] @1: The mouse visits the lion.[(((triple10) -> rule3))]
The cow eats the lion.
("cow" "eats" "lion" "+")
triple1
The cow is big.
("cow" "is" "big" "+")
triple2
The cow is young.
("cow" "is" "young" "+")
triple3
The lion is rough.
("lion" "is" "rough" "+")
triple4
The lion is young.
("lion" "is" "young" "+")
triple5
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple6
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple7
The mouse is big.
("mouse" "is" "big" "+")
triple8
The mouse is rough.
("mouse" "is" "rough" "+")
triple9
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple10
The mouse visits the lion.
("mouse" "visits" "lion" "+")
((triple10) -> (rule3 % int1))
The mouse visits the lion.
("mouse" "visits" "lion" "+")
int1