The cat is green. The cat is kind. The cat likes the dog. The cat likes the lion. The cat likes the squirrel. The dog eats the lion. The dog is red. The dog visits the lion. The lion is nice. The lion is red. The squirrel does not like the lion. If something is green and not nice then it likes the squirrel. If something eats the cat then the cat is red. If something likes the squirrel and it visits the lion then it is not red. If something is green and it visits the cat then the cat is kind. If something visits the squirrel and it eats the dog then the dog visits the lion. If something eats the squirrel then it eats the cat. If something is red then it eats the squirrel.
The cat is green.
("cat" "is" "green" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat likes the dog.
("cat" "likes" "dog" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The dog eats the lion.
("dog" "eats" "lion" "+")
The dog is red.
("dog" "is" "red" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion is nice.
("lion" "is" "nice" "+")
The lion is red.
("lion" "is" "red" "+")
The squirrel does not like the lion.
("squirrel" "likes" "lion" "-")
If something is green and not nice then it likes the squirrel.
((("something" "is" "green" "+") ("something" "is" "nice" "~")) -> ("something" "likes" "squirrel" "+"))
If something eats the cat then the cat is red.
((("something" "eats" "cat" "+")) -> ("cat" "is" "red" "+"))
If something likes the squirrel and it visits the lion then it is not red.
((("something" "likes" "squirrel" "+") ("something" "visits" "lion" "+")) -> ("something" "is" "red" "-"))
If something is green and it visits the cat then the cat is kind.
((("something" "is" "green" "+") ("something" "visits" "cat" "+")) -> ("cat" "is" "kind" "+"))
If something visits the squirrel and it eats the dog then the dog visits the lion.
((("something" "visits" "squirrel" "+") ("something" "eats" "dog" "+")) -> ("dog" "visits" "lion" "+"))
If something eats the squirrel then it eats the cat.
((("something" "eats" "squirrel" "+")) -> ("something" "eats" "cat" "+"))
If something is red then it eats the squirrel.
((("something" "is" "red" "+")) -> ("something" "eats" "squirrel" "+"))
The lion is red.
True
1
proof
[(triple10)]
("lion" "is" "red" "+")
triple10
The cat does not like the lion.
False
1
inv-proof
[(triple4)]
("cat" "likes" "lion" "-")
triple4
The lion eats the squirrel.
True
2
proof
[(((triple10) -> rule7))]
("lion" "eats" "squirrel" "+")
((triple10) -> (rule7 % int1))
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int1
The dog does not eat the squirrel.
False
2
inv-proof
[(((triple7) -> rule7))]
("dog" "eats" "squirrel" "-")
((triple7) -> (rule7 % int1))
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int1
The lion eats the cat.
True
3
proof
[(((((triple10) -> rule7)) -> rule6))]
("lion" "eats" "cat" "+")
((((triple10) -> (rule7 % int2))) -> (rule6 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int2
The lion does not eat the cat.
False
3
inv-proof
[(((((triple10) -> rule7)) -> rule6))]
("lion" "eats" "cat" "-")
((((triple10) -> (rule7 % int2))) -> (rule6 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int2
The cat is red.
True
4
proof
[(((((((triple10) -> rule7)) -> rule6)) -> rule2) OR ((((((triple7) -> rule7)) -> rule6)) -> rule2))]
("cat" "is" "red" "+")
((((((triple10) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int3
((((((triple7) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The dog eats the cat.
("dog" "eats" "cat" "+")
int2
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int3
The cat is not red.
False
4
inv-proof
[(((((((triple10) -> rule7)) -> rule6)) -> rule2) OR ((((((triple7) -> rule7)) -> rule6)) -> rule2))]
("cat" "is" "red" "-")
((((((triple10) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int3
((((((triple7) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The dog eats the cat.
("dog" "eats" "cat" "+")
int2
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int3
The cat eats the squirrel.
True
5
proof
[(((((((((triple10) -> rule7)) -> rule6)) -> rule2)) -> rule7) OR ((((((((triple7) -> rule7)) -> rule6)) -> rule2)) -> rule7))]
("cat" "eats" "squirrel" "+")
((((((((triple10) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The lion eats the cat.
("lion" "eats" "cat" "+")
int3
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int4
((((((((triple7) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The dog eats the cat.
("dog" "eats" "cat" "+")
int3
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int4
The cat does not eat the squirrel.
False
5
inv-proof
[(((((((((triple10) -> rule7)) -> rule6)) -> rule2)) -> rule7) OR ((((((((triple7) -> rule7)) -> rule6)) -> rule2)) -> rule7))]
("cat" "eats" "squirrel" "-")
((((((((triple10) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The lion eats the cat.
("lion" "eats" "cat" "+")
int3
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int4
((((((((triple7) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The dog eats the cat.
("dog" "eats" "cat" "+")
int3
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int4
The cat eats the cat.
True
6
proof
[(((((((((((triple10) -> rule7)) -> rule6)) -> rule2)) -> rule7)) -> rule6) OR ((((((((((triple7) -> rule7)) -> rule6)) -> rule2)) -> rule7)) -> rule6))]
("cat" "eats" "cat" "+")
((((((((((triple10) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The lion eats the cat.
("lion" "eats" "cat" "+")
int4
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int5
((((((((((triple7) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The dog eats the cat.
("dog" "eats" "cat" "+")
int4
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int5
The cat does not eat the cat.
False
6
inv-proof
[(((((((((((triple10) -> rule7)) -> rule6)) -> rule2)) -> rule7)) -> rule6) OR ((((((((((triple7) -> rule7)) -> rule6)) -> rule2)) -> rule7)) -> rule6))]
("cat" "eats" "cat" "-")
((((((((((triple10) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The lion eats the cat.
("lion" "eats" "cat" "+")
int4
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int5
((((((((((triple7) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The dog eats the cat.
("dog" "eats" "cat" "+")
int4
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int5
The squirrel does not eat the cat.
Unknown
inv-rconc
[@2: The squirrel eats the cat.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("squirrel" "eats" "cat" "-")
The dog likes the squirrel.
Unknown
rconc
[@1: The dog likes the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "likes" "squirrel" "+")
The squirrel does not eat the squirrel.
Unknown
inv-rconc
[@1: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "eats" "squirrel" "-")
The squirrel likes the squirrel.
Unknown
rconc
[@1: The squirrel likes the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "likes" "squirrel" "+")
The lion does not like the squirrel.
Unknown
inv-rconc
[@1: The lion likes the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "likes" "squirrel" "-")
The lion visits the dog.
Unknown
random
[@0: The lion visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "dog" "+")
The cat does not visit the dog.
Unknown
inv-random
[@0: The cat visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "dog" "-")
The dog is nice.
Unknown
random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "+")
The dog is not round.
Unknown
inv-random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
The cat does not eat the dog.
Unknown
inv-random
[@0: The cat eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "dog" "-")
The lion likes the cat.
Unknown
random
[@0: The lion likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "cat" "+")
@0: The cat is green.[(triple1)] The cat is kind.[(triple2)] The cat likes the dog.[(triple3)] The cat likes the lion.[(triple4)] The cat likes the squirrel.[(triple5)] The dog eats the lion.[(triple6)] The dog is red.[(triple7)] The dog visits the lion.[(triple8)] The lion is nice.[(triple9)] The lion is red.[(triple10)] The squirrel does not like the lion.[(triple11)] @1: The dog eats the squirrel.[(((triple7) -> rule7))] The lion eats the squirrel.[(((triple10) -> rule7))] @2: The dog eats the cat.[(((((triple7) -> rule7)) -> rule6))] The lion eats the cat.[(((((triple10) -> rule7)) -> rule6))] @3: The cat is red.[(((((((triple10) -> rule7)) -> rule6)) -> rule2) OR ((((((triple7) -> rule7)) -> rule6)) -> rule2))] @4: The cat eats the squirrel.[(((((((((triple10) -> rule7)) -> rule6)) -> rule2)) -> rule7) OR ((((((((triple7) -> rule7)) -> rule6)) -> rule2)) -> rule7))] @5: The cat eats the cat.[(((((((((((triple10) -> rule7)) -> rule6)) -> rule2)) -> rule7)) -> rule6) OR ((((((((((triple7) -> rule7)) -> rule6)) -> rule2)) -> rule7)) -> rule6))]
The cat is green.
("cat" "is" "green" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat likes the dog.
("cat" "likes" "dog" "+")
triple3
The cat likes the lion.
("cat" "likes" "lion" "+")
triple4
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple5
The dog eats the lion.
("dog" "eats" "lion" "+")
triple6
The dog is red.
("dog" "is" "red" "+")
triple7
The dog visits the lion.
("dog" "visits" "lion" "+")
triple8
The lion is nice.
("lion" "is" "nice" "+")
triple9
The lion is red.
("lion" "is" "red" "+")
triple10
The squirrel does not like the lion.
("squirrel" "likes" "lion" "-")
triple11
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
((triple7) -> (rule7 % int1))
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
((triple10) -> (rule7 % int1))
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int1
The dog eats the cat.
("dog" "eats" "cat" "+")
((((triple7) -> (rule7 % int2))) -> (rule6 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int2
The lion eats the cat.
("lion" "eats" "cat" "+")
((((triple10) -> (rule7 % int2))) -> (rule6 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int2
The cat is red.
("cat" "is" "red" "+")
((((((triple10) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int3
((((((triple7) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The dog eats the cat.
("dog" "eats" "cat" "+")
int2
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int3
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
((((((((triple10) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The lion eats the cat.
("lion" "eats" "cat" "+")
int3
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int4
((((((((triple7) -> (rule7 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The dog eats the cat.
("dog" "eats" "cat" "+")
int3
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int4
The cat eats the cat.
("cat" "eats" "cat" "+")
((((((((((triple10) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The lion eats the cat.
("lion" "eats" "cat" "+")
int4
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
int5
((((((((((triple7) -> (rule7 % int5))) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The dog eats the cat.
("dog" "eats" "cat" "+")
int4
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int5