The cat eats the dog. The cat is kind. The cat is red. The dog is kind. The dog is young. The dog sees the cat. The dog visits the cat. If someone is kind and they eat the cat then they visit the cat. If someone sees the cat and the cat sees the dog then the dog eats the cat. If the dog sees the cat and the dog visits the cat then the dog eats the cat. If someone visits the cat and they eat the dog then they are green. If someone eats the cat and the cat is red then they are green. If someone eats the cat then they see the cat. If someone eats the dog and they eat the cat then they are rough. If the dog is green and the dog eats the cat then the cat does not see the dog.
The cat eats the dog.
("cat" "eats" "dog" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is red.
("cat" "is" "red" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is young.
("dog" "is" "young" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
If someone is kind and they eat the cat then they visit the cat.
((("someone" "is" "kind" "+") ("someone" "eats" "cat" "+")) -> ("someone" "visits" "cat" "+"))
If someone sees the cat and the cat sees the dog then the dog eats the cat.
((("someone" "sees" "cat" "+") ("cat" "sees" "dog" "+")) -> ("dog" "eats" "cat" "+"))
If the dog sees the cat and the dog visits the cat then the dog eats the cat.
((("dog" "sees" "cat" "+") ("dog" "visits" "cat" "+")) -> ("dog" "eats" "cat" "+"))
If someone visits the cat and they eat the dog then they are green.
((("someone" "visits" "cat" "+") ("someone" "eats" "dog" "+")) -> ("someone" "is" "green" "+"))
If someone eats the cat and the cat is red then they are green.
((("someone" "eats" "cat" "+") ("cat" "is" "red" "+")) -> ("someone" "is" "green" "+"))
If someone eats the cat then they see the cat.
((("someone" "eats" "cat" "+")) -> ("someone" "sees" "cat" "+"))
If someone eats the dog and they eat the cat then they are rough.
((("someone" "eats" "dog" "+") ("someone" "eats" "cat" "+")) -> ("someone" "is" "rough" "+"))
If the dog is green and the dog eats the cat then the cat does not see the dog.
((("dog" "is" "green" "+") ("dog" "eats" "cat" "+")) -> ("cat" "sees" "dog" "-"))
The cat eats the dog.
True
1
proof
[(triple1)]
("cat" "eats" "dog" "+")
triple1
The dog does not see the cat.
False
1
inv-proof
[(triple6)]
("dog" "sees" "cat" "-")
triple6
The dog eats the cat.
True
3
proof
[(((triple6 triple7) -> rule3))]
("dog" "eats" "cat" "+")
((triple6 triple7) -> (rule3 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
The dog does not eat the cat.
False
3
inv-proof
[(((triple6 triple7) -> rule3))]
("dog" "eats" "cat" "-")
((triple6 triple7) -> (rule3 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
The dog is green.
True
5
proof
[(((((triple6 triple7) -> rule3) triple3) -> rule5))]
("dog" "is" "green" "+")
((((triple6 triple7) -> (rule3 % int2)) triple3) -> (rule5 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog eats the cat.
("dog" "eats" "cat" "+")
int2
The dog is not green.
False
5
inv-proof
[(((((triple6 triple7) -> rule3) triple3) -> rule5))]
("dog" "is" "green" "-")
((((triple6 triple7) -> (rule3 % int2)) triple3) -> (rule5 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog eats the cat.
("dog" "eats" "cat" "+")
int2
The cat does not see the dog.
True
9
proof
[(((((((triple6 triple7) -> rule3) triple3) -> rule5) ((triple6 triple7) -> rule3)) -> rule8))]
("cat" "sees" "dog" "-")
((((((triple6 triple7) -> (rule3 % int3)) triple3) -> (rule5 % int2)) ((triple6 triple7) -> (rule3 % int3))) -> (rule8 % int1))
The cat does not see the dog.
("cat" "sees" "dog" "-")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The dog eats the cat.
("dog" "eats" "cat" "+")
int3
The cat sees the dog.
False
9
inv-proof
[(((((((triple6 triple7) -> rule3) triple3) -> rule5) ((triple6 triple7) -> rule3)) -> rule8))]
("cat" "sees" "dog" "+")
((((((triple6 triple7) -> (rule3 % int3)) triple3) -> (rule5 % int2)) ((triple6 triple7) -> (rule3 % int3))) -> (rule8 % int1))
The cat does not see the dog.
("cat" "sees" "dog" "-")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The dog eats the cat.
("dog" "eats" "cat" "+")
int3
The cat is not green.
Unknown
inv-rconc
[@2: The cat is green.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("cat" "is" "green" "-")
The cat sees the cat.
Unknown
rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "sees" "cat" "+")
The dog is not rough.
Unknown
inv-rconc
[@1: The dog is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "is" "rough" "-")
The cat visits the cat.
Unknown
rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "visits" "cat" "+")
The cat is not young.
Unknown
inv-random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "-")
The dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
The dog does not eat the dog.
Unknown
inv-random
[@0: The dog eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "dog" "-")
The cat visits the dog.
Unknown
random
[@0: The cat visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "dog" "+")
@0: The cat eats the dog.[(triple1)] The cat is kind.[(triple2)] The cat is red.[(triple3)] The dog is kind.[(triple4)] The dog is young.[(triple5)] The dog sees the cat.[(triple6)] The dog visits the cat.[(triple7)] @1: The dog eats the cat.[(((triple6 triple7) -> rule3))] @2: The dog is green.[(((((triple6 triple7) -> rule3) triple3) -> rule5))] @3: The cat does not see the dog.[(((((((triple6 triple7) -> rule3) triple3) -> rule5) ((triple6 triple7) -> rule3)) -> rule8))]
The cat eats the dog.
("cat" "eats" "dog" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple2
The cat is red.
("cat" "is" "red" "+")
triple3
The dog is kind.
("dog" "is" "kind" "+")
triple4
The dog is young.
("dog" "is" "young" "+")
triple5
The dog sees the cat.
("dog" "sees" "cat" "+")
triple6
The dog visits the cat.
("dog" "visits" "cat" "+")
triple7
The dog eats the cat.
("dog" "eats" "cat" "+")
((triple6 triple7) -> (rule3 % int1))
The dog eats the cat.
("dog" "eats" "cat" "+")
int1
The dog is green.
("dog" "is" "green" "+")
((((triple6 triple7) -> (rule3 % int2)) triple3) -> (rule5 % int1))
The dog is green.
("dog" "is" "green" "+")
int1
The dog eats the cat.
("dog" "eats" "cat" "+")
int2
The cat does not see the dog.
("cat" "sees" "dog" "-")
((((((triple6 triple7) -> (rule3 % int3)) triple3) -> (rule5 % int2)) ((triple6 triple7) -> (rule3 % int3))) -> (rule8 % int1))
The cat does not see the dog.
("cat" "sees" "dog" "-")
int1
The dog is green.
("dog" "is" "green" "+")
int2
The dog eats the cat.
("dog" "eats" "cat" "+")
int3