The dog visits the lion. The lion does not visit the dog. The squirrel visits the dog. If something is blue then it visits the dog. If something visits the dog then the dog likes the squirrel. If something likes the lion and it visits the dog then it is green. If the dog eats the lion and the lion does not eat the dog then the dog is blue. If something likes the squirrel then it is blue. If something eats the squirrel and it likes the squirrel then it does not visit the squirrel.
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion does not visit the dog.
("lion" "visits" "dog" "-")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
If something is blue then it visits the dog.
((("something" "is" "blue" "+")) -> ("something" "visits" "dog" "+"))
If something visits the dog then the dog likes the squirrel.
((("something" "visits" "dog" "+")) -> ("dog" "likes" "squirrel" "+"))
If something likes the lion and it visits the dog then it is green.
((("something" "likes" "lion" "+") ("something" "visits" "dog" "+")) -> ("something" "is" "green" "+"))
If the dog eats the lion and the lion does not eat the dog then the dog is blue.
((("dog" "eats" "lion" "+") ("lion" "eats" "dog" "~")) -> ("dog" "is" "blue" "+"))
If something likes the squirrel then it is blue.
((("something" "likes" "squirrel" "+")) -> ("something" "is" "blue" "+"))
If something eats the squirrel and it likes the squirrel then it does not visit the squirrel.
((("something" "eats" "squirrel" "+") ("something" "likes" "squirrel" "+")) -> ("something" "visits" "squirrel" "-"))
The dog visits the lion.
True
1
proof
[(triple1)]
("dog" "visits" "lion" "+")
triple1
The dog does not visit the lion.
False
1
inv-proof
[(triple1)]
("dog" "visits" "lion" "-")
triple1
The dog likes the squirrel.
True
2
proof
[(((triple3) -> rule2))]
("dog" "likes" "squirrel" "+")
((triple3) -> (rule2 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The dog does not like the squirrel.
False
2
inv-proof
[(((triple3) -> rule2))]
("dog" "likes" "squirrel" "-")
((triple3) -> (rule2 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The dog is blue.
True
3
proof
[(((((triple3) -> rule2)) -> rule5))]
("dog" "is" "blue" "+")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int2
The dog is not blue.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule5))]
("dog" "is" "blue" "-")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int2
The dog visits the dog.
True
4
proof
[(((((((triple3) -> rule2)) -> rule5)) -> rule1))]
("dog" "visits" "dog" "+")
((((((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int3
The dog does not visit the dog.
False
4
inv-proof
[(((((((triple3) -> rule2)) -> rule5)) -> rule1))]
("dog" "visits" "dog" "-")
((((((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int3
The dog is not green.
Unknown
inv-rconc
[@1: The dog is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "green" "-")
The lion is blue.
Unknown
rconc
[@1: The lion is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "is" "blue" "+")
The squirrel is not green.
Unknown
inv-rconc
[@1: The squirrel is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "green" "-")
The squirrel is blue.
Unknown
rconc
[@1: The squirrel is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "is" "blue" "+")
The squirrel does not like the dog.
Unknown
inv-random
[@0: The squirrel likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "dog" "-")
The squirrel eats the dog.
Unknown
random
[@0: The squirrel eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "dog" "+")
The lion does not eat the dog.
Unknown
inv-random
[@0: The lion eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "dog" "-")
The dog likes the lion.
Unknown
random
[@0: The dog likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "lion" "+")
@0: The dog visits the lion.[(triple1)] The lion does not visit the dog.[(triple2)] The squirrel visits the dog.[(triple3)] @1: The dog likes the squirrel.[(((triple3) -> rule2))] @2: The dog is blue.[(((((triple3) -> rule2)) -> rule5))] @3: The dog visits the dog.[(((((((triple3) -> rule2)) -> rule5)) -> rule1))]
The dog visits the lion.
("dog" "visits" "lion" "+")
triple1
The lion does not visit the dog.
("lion" "visits" "dog" "-")
triple2
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple3
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
((triple3) -> (rule2 % int1))
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
((((((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog likes the squirrel.
("dog" "likes" "squirrel" "+")
int3