The cow eats the mouse. The cow is red. The cow likes the lion. The cow visits the mouse. The lion eats the mouse. The lion is young. The lion visits the cow. The mouse eats the cow. The mouse eats the lion. The mouse is cold. The mouse is green. The mouse is rough. The mouse is young. The mouse likes the cow. The mouse likes the lion. The mouse visits the lion. If something visits the lion then it visits the mouse. If something is rough then it is young. If the lion likes the cow and the lion is rough then the lion visits the cow. If something is green and it likes the mouse then it likes the lion. If something visits the mouse and it eats the mouse then the mouse eats the cow. If the lion is young then the lion visits the mouse.
The cow eats the mouse.
("cow" "eats" "mouse" "+")
The cow is red.
("cow" "is" "red" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The lion eats the mouse.
("lion" "eats" "mouse" "+")
The lion is young.
("lion" "is" "young" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
The mouse eats the cow.
("mouse" "eats" "cow" "+")
The mouse eats the lion.
("mouse" "eats" "lion" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse likes the cow.
("mouse" "likes" "cow" "+")
The mouse likes the lion.
("mouse" "likes" "lion" "+")
The mouse visits the lion.
("mouse" "visits" "lion" "+")
If something visits the lion then it visits the mouse.
((("something" "visits" "lion" "+")) -> ("something" "visits" "mouse" "+"))
If something is rough then it is young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If the lion likes the cow and the lion is rough then the lion visits the cow.
((("lion" "likes" "cow" "+") ("lion" "is" "rough" "+")) -> ("lion" "visits" "cow" "+"))
If something is green and it likes the mouse then it likes the lion.
((("something" "is" "green" "+") ("something" "likes" "mouse" "+")) -> ("something" "likes" "lion" "+"))
If something visits the mouse and it eats the mouse then the mouse eats the cow.
((("something" "visits" "mouse" "+") ("something" "eats" "mouse" "+")) -> ("mouse" "eats" "cow" "+"))
If the lion is young then the lion visits the mouse.
((("lion" "is" "young" "+")) -> ("lion" "visits" "mouse" "+"))
The cow eats the mouse.
True
1
proof
[(triple1)]
("cow" "eats" "mouse" "+")
triple1
The mouse does not eat the cow.
False
1
inv-proof
[(triple8 OR ((triple4 triple1) -> rule5) OR ((((triple6) -> rule6) triple5) -> rule5))]
("mouse" "eats" "cow" "-")
triple8
((triple4 triple1) -> (rule5 % int1))
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int1
((((triple6) -> (rule6 % int2)) triple5) -> (rule5 % int1))
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int1
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int2
The lion visits the mouse.
True
2
proof
[(((triple6) -> rule6))]
("lion" "visits" "mouse" "+")
((triple6) -> (rule6 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The mouse does not visit the mouse.
False
2
inv-proof
[(((triple16) -> rule1))]
("mouse" "visits" "mouse" "-")
((triple16) -> (rule1 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1
The lion does not like the lion.
Unknown
inv-rconc
[@1: The lion likes the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "likes" "lion" "-")
The cow is young.
Unknown
rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "young" "+")
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 rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
@0: The cow eats the mouse.[(triple1)] The cow is red.[(triple2)] The cow likes the lion.[(triple3)] The cow visits the mouse.[(triple4)] The lion eats the mouse.[(triple5)] The lion is young.[(triple6)] The lion visits the cow.[(triple7)] The mouse eats the cow.[(triple8 OR ((triple4 triple1) -> rule5) OR ((((triple6) -> rule6) triple5) -> rule5))] The mouse eats the lion.[(triple9)] The mouse is cold.[(triple10)] The mouse is green.[(triple11)] The mouse is rough.[(triple12)] The mouse is young.[(triple13 OR ((triple12) -> rule2))] The mouse likes the cow.[(triple14)] The mouse likes the lion.[(triple15)] The mouse visits the lion.[(triple16)] @1: The lion visits the mouse.[(((triple6) -> rule6))] The mouse visits the mouse.[(((triple16) -> rule1))]
The cow eats the mouse.
("cow" "eats" "mouse" "+")
triple1
The cow is red.
("cow" "is" "red" "+")
triple2
The cow likes the lion.
("cow" "likes" "lion" "+")
triple3
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple4
The lion eats the mouse.
("lion" "eats" "mouse" "+")
triple5
The lion is young.
("lion" "is" "young" "+")
triple6
The lion visits the cow.
("lion" "visits" "cow" "+")
triple7
The mouse eats the cow.
("mouse" "eats" "cow" "+")
triple8
((triple4 triple1) -> (rule5 % int1))
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int1
((((triple6) -> (rule6 % int2)) triple5) -> (rule5 % int1))
The mouse eats the cow.
("mouse" "eats" "cow" "+")
int1
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int2
The mouse eats the lion.
("mouse" "eats" "lion" "+")
triple9
The mouse is cold.
("mouse" "is" "cold" "+")
triple10
The mouse is green.
("mouse" "is" "green" "+")
triple11
The mouse is rough.
("mouse" "is" "rough" "+")
triple12
The mouse is young.
("mouse" "is" "young" "+")
triple13
((triple12) -> (rule2 % int1))
The mouse is young.
("mouse" "is" "young" "+")
int1
The mouse likes the cow.
("mouse" "likes" "cow" "+")
triple14
The mouse likes the lion.
("mouse" "likes" "lion" "+")
triple15
The mouse visits the lion.
("mouse" "visits" "lion" "+")
triple16
The lion visits the mouse.
("lion" "visits" "mouse" "+")
((triple6) -> (rule6 % int1))
The lion visits the mouse.
("lion" "visits" "mouse" "+")
int1
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
((triple16) -> (rule1 % int1))
The mouse visits the mouse.
("mouse" "visits" "mouse" "+")
int1