The cat eats the dog. The dog eats the lion. The lion is red. If the cat likes the lion and the cat chases the lion then the lion likes the dog. If something is red then it eats the lion. If something eats the lion then it likes the lion. If something eats the lion then the lion likes the dog. All green things are nice. If something likes the lion then the lion is green.
The cat eats the dog.
("cat" "eats" "dog" "+")
The dog eats the lion.
("dog" "eats" "lion" "+")
The lion is red.
("lion" "is" "red" "+")
If the cat likes the lion and the cat chases the lion then the lion likes the dog.
((("cat" "likes" "lion" "+") ("cat" "chases" "lion" "+")) -> ("lion" "likes" "dog" "+"))
If something is red then it eats the lion.
((("something" "is" "red" "+")) -> ("something" "eats" "lion" "+"))
If something eats the lion then it likes the lion.
((("something" "eats" "lion" "+")) -> ("something" "likes" "lion" "+"))
If something eats the lion then the lion likes the dog.
((("something" "eats" "lion" "+")) -> ("lion" "likes" "dog" "+"))
All green things are nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If something likes the lion then the lion is green.
((("something" "likes" "lion" "+")) -> ("lion" "is" "green" "+"))
The cat eats the dog.
True
1
proof
[(triple1)]
("cat" "eats" "dog" "+")
triple1
The dog does not eat the lion.
False
1
inv-proof
[(triple2)]
("dog" "eats" "lion" "-")
triple2
The lion eats the lion.
True
2
proof
[(((triple3) -> rule2))]
("lion" "eats" "lion" "+")
((triple3) -> (rule2 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The dog does not like the lion.
False
2
inv-proof
[(((triple2) -> rule3))]
("dog" "likes" "lion" "-")
((triple2) -> (rule3 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The lion is green.
True
3
proof
[(((((triple2) -> rule3)) -> rule6) OR ((((((triple3) -> rule2)) -> rule3)) -> rule6))]
("lion" "is" "green" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
int2
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion eats the lion.
("lion" "eats" "lion" "+")
int3
The lion is not green.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule6) OR ((((((triple3) -> rule2)) -> rule3)) -> rule6))]
("lion" "is" "green" "-")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
int2
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion eats the lion.
("lion" "eats" "lion" "+")
int3
The lion is nice.
True
4
proof
[(((((((triple2) -> rule3)) -> rule6)) -> rule5) OR ((((((((triple3) -> rule2)) -> rule3)) -> rule6)) -> rule5))]
("lion" "is" "nice" "+")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The dog likes the lion.
("dog" "likes" "lion" "+")
int3
((((((((triple3) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
int3
The lion eats the lion.
("lion" "eats" "lion" "+")
int4
The lion is not nice.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule6)) -> rule5) OR ((((((((triple3) -> rule2)) -> rule3)) -> rule6)) -> rule5))]
("lion" "is" "nice" "-")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The dog likes the lion.
("dog" "likes" "lion" "+")
int3
((((((((triple3) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
int3
The lion eats the lion.
("lion" "eats" "lion" "+")
int4
The dog is not nice.
Unknown
inv-rconc
[@1: The dog is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "nice" "-")
The cat eats the lion.
Unknown
rconc
[@1: The cat eats the lion.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "eats" "lion" "+")
The cat does not like the lion.
Unknown
inv-rconc
[@2: The cat likes the lion.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("cat" "likes" "lion" "-")
The cat is nice.
Unknown
rconc
[@1: The cat is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "is" "nice" "+")
The dog does not eat the cat.
Unknown
inv-random
[@0: The dog eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "cat" "-")
The dog likes the cat.
Unknown
random
[@0: The dog likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "cat" "+")
The dog does not like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The dog chases the cat.
Unknown
random
[@0: The dog chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "cat" "+")
@0: The cat eats the dog.[(triple1)] The dog eats the lion.[(triple2)] The lion is red.[(triple3)] @1: The dog likes the lion.[(((triple2) -> rule3))] The lion eats the lion.[(((triple3) -> rule2))] The lion likes the dog.[(((triple2) -> rule4) OR ((((triple3) -> rule2)) -> rule4))] @2: The lion is green.[(((((triple2) -> rule3)) -> rule6) OR ((((((triple3) -> rule2)) -> rule3)) -> rule6))] The lion likes the lion.[(((((triple3) -> rule2)) -> rule3))] @3: The lion is nice.[(((((((triple2) -> rule3)) -> rule6)) -> rule5) OR ((((((((triple3) -> rule2)) -> rule3)) -> rule6)) -> rule5))]
The cat eats the dog.
("cat" "eats" "dog" "+")
triple1
The dog eats the lion.
("dog" "eats" "lion" "+")
triple2
The lion is red.
("lion" "is" "red" "+")
triple3
The dog likes the lion.
("dog" "likes" "lion" "+")
((triple2) -> (rule3 % int1))
The dog likes the lion.
("dog" "likes" "lion" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
((triple3) -> (rule2 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion likes the dog.
("lion" "likes" "dog" "+")
((triple2) -> (rule4 % int1))
The lion likes the dog.
("lion" "likes" "dog" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
The lion likes the dog.
("lion" "likes" "dog" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion is green.
("lion" "is" "green" "+")
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The dog likes the lion.
("dog" "likes" "lion" "+")
int2
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion likes the lion.
("lion" "likes" "lion" "+")
int2
The lion eats the lion.
("lion" "eats" "lion" "+")
int3
The lion likes the lion.
("lion" "likes" "lion" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The lion likes the lion.
("lion" "likes" "lion" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion is nice.
("lion" "is" "nice" "+")
((((((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The dog likes the lion.
("dog" "likes" "lion" "+")
int3
((((((((triple3) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The lion is nice.
("lion" "is" "nice" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion likes the lion.
("lion" "likes" "lion" "+")
int3
The lion eats the lion.
("lion" "eats" "lion" "+")
int4