The cow needs the mouse. The dog is not green. The dog likes the lion. The dog likes the mouse. The dog needs the cow. The dog needs the mouse. The lion is not green. The lion does not like the dog. The lion likes the mouse. The lion needs the dog. The lion visits the cow. The lion does not visit the dog. The mouse likes the dog. The mouse needs the lion. The mouse visits the dog. The mouse does not visit the lion. If something needs the lion and it is not round then it likes the cow. If something is red then it likes the cow. Green, nice things are not young. If something needs the dog then the dog is red. If something is young and it does not like the mouse then it is green. If the dog visits the mouse and the mouse does not visit the cow then the mouse needs the cow.
The cow needs the mouse.
("cow" "needs" "mouse" "+")
The dog is not green.
("dog" "is" "green" "-")
The dog likes the lion.
("dog" "likes" "lion" "+")
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The lion is not green.
("lion" "is" "green" "-")
The lion does not like the dog.
("lion" "likes" "dog" "-")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
The lion does not visit the dog.
("lion" "visits" "dog" "-")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The mouse needs the lion.
("mouse" "needs" "lion" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
The mouse does not visit the lion.
("mouse" "visits" "lion" "-")
If something needs the lion and it is not round then it likes the cow.
((("something" "needs" "lion" "+") ("something" "is" "round" "~")) -> ("something" "likes" "cow" "+"))
If something is red then it likes the cow.
((("something" "is" "red" "+")) -> ("something" "likes" "cow" "+"))
Green, nice things are not young.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "-"))
If something needs the dog then the dog is red.
((("something" "needs" "dog" "+")) -> ("dog" "is" "red" "+"))
If something is young and it does not like the mouse then it is green.
((("something" "is" "young" "+") ("something" "likes" "mouse" "~")) -> ("something" "is" "green" "+"))
If the dog visits the mouse and the mouse does not visit the cow then the mouse needs the cow.
((("dog" "visits" "mouse" "+") ("mouse" "visits" "cow" "~")) -> ("mouse" "needs" "cow" "+"))
The mouse does not visit the lion.
True
1
proof
[(triple16)]
("mouse" "visits" "lion" "-")
triple16
The dog does not like the lion.
False
1
inv-proof
[(triple3)]
("dog" "likes" "lion" "-")
triple3
The dog is red.
True
2
proof
[(((triple10) -> rule4))]
("dog" "is" "red" "+")
((triple10) -> (rule4 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog is not red.
False
2
inv-proof
[(((triple10) -> rule4))]
("dog" "is" "red" "-")
((triple10) -> (rule4 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog likes the cow.
True
3
proof
[(((((triple10) -> rule4)) -> rule2))]
("dog" "likes" "cow" "+")
((((triple10) -> (rule4 % int2))) -> (rule2 % int1))
The dog likes the cow.
("dog" "likes" "cow" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog does not like the cow.
False
3
inv-proof
[(((((triple10) -> rule4)) -> rule2))]
("dog" "likes" "cow" "-")
((((triple10) -> (rule4 % int2))) -> (rule2 % int1))
The dog likes the cow.
("dog" "likes" "cow" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The mouse does not like the cow.
Unknown
inv-rconc
[@1: The mouse likes the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "likes" "cow" "-")
The cow likes the cow.
Unknown
rconc
[@1: The cow likes the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "likes" "cow" "+")
The cow is not green.
Unknown
inv-rconc
[@1: The cow is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "is" "green" "-")
The lion visits the mouse.
Unknown
random
[@0: The lion visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "mouse" "+")
The lion is not red.
Unknown
inv-random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "-")
The lion is round.
Unknown
random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "+")
@0: The cow needs the mouse.[(triple1)] The dog is not green.[(triple2)] The dog likes the lion.[(triple3)] The dog likes the mouse.[(triple4)] The dog needs the cow.[(triple5)] The dog needs the mouse.[(triple6)] The lion does not like the dog.[(triple8)] The lion does not visit the dog.[(triple12)] The lion is not green.[(triple7)] The lion likes the mouse.[(triple9)] The lion needs the dog.[(triple10)] The lion visits the cow.[(triple11)] The mouse does not visit the lion.[(triple16)] The mouse likes the dog.[(triple13)] The mouse needs the lion.[(triple14)] The mouse visits the dog.[(triple15)] @1: The dog is red.[(((triple10) -> rule4))] @2: The dog likes the cow.[(((((triple10) -> rule4)) -> rule2))]
The cow needs the mouse.
("cow" "needs" "mouse" "+")
triple1
The dog is not green.
("dog" "is" "green" "-")
triple2
The dog likes the lion.
("dog" "likes" "lion" "+")
triple3
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple4
The dog needs the cow.
("dog" "needs" "cow" "+")
triple5
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple6
The lion does not like the dog.
("lion" "likes" "dog" "-")
triple8
The lion does not visit the dog.
("lion" "visits" "dog" "-")
triple12
The lion is not green.
("lion" "is" "green" "-")
triple7
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple9
The lion needs the dog.
("lion" "needs" "dog" "+")
triple10
The lion visits the cow.
("lion" "visits" "cow" "+")
triple11
The mouse does not visit the lion.
("mouse" "visits" "lion" "-")
triple16
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple13
The mouse needs the lion.
("mouse" "needs" "lion" "+")
triple14
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple15
The dog is red.
("dog" "is" "red" "+")
((triple10) -> (rule4 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog likes the cow.
("dog" "likes" "cow" "+")
((((triple10) -> (rule4 % int2))) -> (rule2 % int1))
The dog likes the cow.
("dog" "likes" "cow" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2