The bear is red. The cat is nice. The dog eats the bear. If someone eats the bear then the bear is nice. If the dog is nice and the dog eats the cat then the dog needs the bear. If someone visits the dog then they are blue. If someone eats the cat and the cat needs the bear then the bear eats the cat. If someone is nice then they visit the dog. If the dog visits the cat and the dog needs the cat then the cat needs the bear. If someone visits the cat then the cat visits the dog. If the dog eats the cat then the cat needs the bear.
The bear is red.
("bear" "is" "red" "+")
The cat is nice.
("cat" "is" "nice" "+")
The dog eats the bear.
("dog" "eats" "bear" "+")
If someone eats the bear then the bear is nice.
((("someone" "eats" "bear" "+")) -> ("bear" "is" "nice" "+"))
If the dog is nice and the dog eats the cat then the dog needs the bear.
((("dog" "is" "nice" "+") ("dog" "eats" "cat" "+")) -> ("dog" "needs" "bear" "+"))
If someone visits the dog then they are blue.
((("someone" "visits" "dog" "+")) -> ("someone" "is" "blue" "+"))
If someone eats the cat and the cat needs the bear then the bear eats the cat.
((("someone" "eats" "cat" "+") ("cat" "needs" "bear" "+")) -> ("bear" "eats" "cat" "+"))
If someone is nice then they visit the dog.
((("someone" "is" "nice" "+")) -> ("someone" "visits" "dog" "+"))
If the dog visits the cat and the dog needs the cat then the cat needs the bear.
((("dog" "visits" "cat" "+") ("dog" "needs" "cat" "+")) -> ("cat" "needs" "bear" "+"))
If someone visits the cat then the cat visits the dog.
((("someone" "visits" "cat" "+")) -> ("cat" "visits" "dog" "+"))
If the dog eats the cat then the cat needs the bear.
((("dog" "eats" "cat" "+")) -> ("cat" "needs" "bear" "+"))
The cat is nice.
True
1
proof
[(triple2)]
("cat" "is" "nice" "+")
triple2
The cat is not nice.
False
1
inv-proof
[(triple2)]
("cat" "is" "nice" "-")
triple2
The cat visits the dog.
True
2
proof
[(((triple2) -> rule5))]
("cat" "visits" "dog" "+")
((triple2) -> (rule5 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The bear is not nice.
False
2
inv-proof
[(((triple3) -> rule1))]
("bear" "is" "nice" "-")
((triple3) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The bear visits the dog.
True
3
proof
[(((((triple3) -> rule1)) -> rule5))]
("bear" "visits" "dog" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The bear visits the dog.
("bear" "visits" "dog" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear does not visit the dog.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule5))]
("bear" "visits" "dog" "-")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The bear visits the dog.
("bear" "visits" "dog" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The bear is blue.
True
4
proof
[(((((((triple3) -> rule1)) -> rule5)) -> rule3))]
("bear" "is" "blue" "+")
((((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The bear is not blue.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule5)) -> rule3))]
("bear" "is" "blue" "-")
((((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3
The bear does not eat the cat.
Unknown
inv-rconc
[@1: The bear eats the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bear" "eats" "cat" "-")
The dog needs the bear.
Unknown
rconc
[@1: The dog needs the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "needs" "bear" "+")
The cat does not need the bear.
Unknown
inv-rconc
[@1: The cat needs the bear.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "needs" "bear" "-")
The dog is blue.
Unknown
rconc
[@2: The dog is blue.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("dog" "is" "blue" "+")
The cat does not eat the bear.
Unknown
inv-random
[@0: The cat eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "bear" "-")
The dog needs the cat.
Unknown
random
[@0: The dog needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "cat" "+")
The dog is not red.
Unknown
inv-random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "-")
The bear visits the cat.
Unknown
random
[@0: The bear visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "cat" "+")
@0: The bear is red.[(triple1)] The cat is nice.[(triple2)] The dog eats the bear.[(triple3)] @1: The bear is nice.[(((triple3) -> rule1))] The cat visits the dog.[(((triple2) -> rule5))] @2: The bear visits the dog.[(((((triple3) -> rule1)) -> rule5))] The cat is blue.[(((((triple2) -> rule5)) -> rule3))] @3: The bear is blue.[(((((((triple3) -> rule1)) -> rule5)) -> rule3))]
The bear is red.
("bear" "is" "red" "+")
triple1
The cat is nice.
("cat" "is" "nice" "+")
triple2
The dog eats the bear.
("dog" "eats" "bear" "+")
triple3
The bear is nice.
("bear" "is" "nice" "+")
((triple3) -> (rule1 % int1))
The bear is nice.
("bear" "is" "nice" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
((triple2) -> (rule5 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The bear visits the dog.
("bear" "visits" "dog" "+")
int1
The bear is nice.
("bear" "is" "nice" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The bear is blue.
("bear" "is" "blue" "+")
((((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The bear is blue.
("bear" "is" "blue" "+")
int1
The bear visits the dog.
("bear" "visits" "dog" "+")
int2
The bear is nice.
("bear" "is" "nice" "+")
int3