The cow likes the lion. The dog is not green. The lion visits the dog. If something is red then it does not need the lion. If the lion likes the cow and the cow does not like the lion then the lion does not like the dog. If something visits the cow then the cow needs the lion. All red things are green. If something likes the lion then it visits the cow. If something needs the cow and it does not visit the cow then the cow visits the dog. If something visits the dog then the dog visits the lion. If the cow does not visit the dog then the cow does not like the dog.
The cow likes the lion.
("cow" "likes" "lion" "+")
The dog is not green.
("dog" "is" "green" "-")
The lion visits the dog.
("lion" "visits" "dog" "+")
If something is red then it does not need the lion.
((("something" "is" "red" "+")) -> ("something" "needs" "lion" "-"))
If the lion likes the cow and the cow does not like the lion then the lion does not like the dog.
((("lion" "likes" "cow" "+") ("cow" "likes" "lion" "~")) -> ("lion" "likes" "dog" "-"))
If something visits the cow then the cow needs the lion.
((("something" "visits" "cow" "+")) -> ("cow" "needs" "lion" "+"))
All red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If something likes the lion then it visits the cow.
((("something" "likes" "lion" "+")) -> ("something" "visits" "cow" "+"))
If something needs the cow and it does not visit the cow then the cow visits the dog.
((("something" "needs" "cow" "+") ("something" "visits" "cow" "~")) -> ("cow" "visits" "dog" "+"))
If something visits the dog then the dog visits the lion.
((("something" "visits" "dog" "+")) -> ("dog" "visits" "lion" "+"))
If the cow does not visit the dog then the cow does not like the dog.
((("cow" "visits" "dog" "~")) -> ("cow" "likes" "dog" "-"))
The dog is not green.
True
1
proof
[(triple2)]
("dog" "is" "green" "-")
triple2
The cow does not like the lion.
False
1
inv-proof
[(triple1)]
("cow" "likes" "lion" "-")
triple1
The dog visits the lion.
True
2
proof
[(((triple3) -> rule7))]
("dog" "visits" "lion" "+")
((triple3) -> (rule7 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The dog does not visit the lion.
False
2
inv-proof
[(((triple3) -> rule7))]
("dog" "visits" "lion" "-")
((triple3) -> (rule7 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The cow needs the lion.
True
3
proof
[(((((triple1) -> rule5)) -> rule3))]
("cow" "needs" "lion" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The cow needs the lion.
("cow" "needs" "lion" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow does not need the lion.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule3))]
("cow" "needs" "lion" "-")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The cow needs the lion.
("cow" "needs" "lion" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow is not green.
Unknown
inv-rconc
[@1: The cow is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "is" "green" "-")
The cow visits the dog.
Unknown
rconc
[@1: The cow visits the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "visits" "dog" "+")
The lion is not green.
Unknown
inv-rconc
[@1: The lion is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "green" "-")
The cow needs the dog.
Unknown
random
[@0: The cow needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "dog" "+")
The cow is not red.
Unknown
inv-random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "-")
The lion needs the cow.
Unknown
random
[@0: The lion needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "cow" "+")
@0: The cow likes the lion.[(triple1)] The dog is not green.[(triple2)] The lion visits the dog.[(triple3)] @1: The cow visits the cow.[(((triple1) -> rule5))] The dog visits the lion.[(((triple3) -> rule7))] @2: The cow needs the lion.[(((((triple1) -> rule5)) -> rule3))]
The cow likes the lion.
("cow" "likes" "lion" "+")
triple1
The dog is not green.
("dog" "is" "green" "-")
triple2
The lion visits the dog.
("lion" "visits" "dog" "+")
triple3
The cow visits the cow.
("cow" "visits" "cow" "+")
((triple1) -> (rule5 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The dog visits the lion.
("dog" "visits" "lion" "+")
((triple3) -> (rule7 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The cow needs the lion.
("cow" "needs" "lion" "+")
((((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The cow needs the lion.
("cow" "needs" "lion" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2