The bear eats the dog. The cat is cold. The cat likes the squirrel. The dog eats the squirrel. The dog is blue. The dog is round. The squirrel likes the cat. If something is cold then it visits the squirrel. If something visits the cat and the cat likes the bear then the cat likes the dog. If something visits the dog then the dog is blue. If something visits the squirrel then it likes the dog. If something likes the dog and it is red then the dog is round. If something eats the dog then the dog is cold.
The bear eats the dog.
("bear" "eats" "dog" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is round.
("dog" "is" "round" "+")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
If something is cold then it visits the squirrel.
((("something" "is" "cold" "+")) -> ("something" "visits" "squirrel" "+"))
If something visits the cat and the cat likes the bear then the cat likes the dog.
((("something" "visits" "cat" "+") ("cat" "likes" "bear" "+")) -> ("cat" "likes" "dog" "+"))
If something visits the dog then the dog is blue.
((("something" "visits" "dog" "+")) -> ("dog" "is" "blue" "+"))
If something visits the squirrel then it likes the dog.
((("something" "visits" "squirrel" "+")) -> ("something" "likes" "dog" "+"))
If something likes the dog and it is red then the dog is round.
((("something" "likes" "dog" "+") ("something" "is" "red" "+")) -> ("dog" "is" "round" "+"))
If something eats the dog then the dog is cold.
((("something" "eats" "dog" "+")) -> ("dog" "is" "cold" "+"))
The dog is round.
True
1
proof
[(triple6)]
("dog" "is" "round" "+")
triple6
The dog is not blue.
False
1
inv-proof
[(triple5)]
("dog" "is" "blue" "-")
triple5
The dog is cold.
True
2
proof
[(((triple1) -> rule6))]
("dog" "is" "cold" "+")
((triple1) -> (rule6 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog is not cold.
False
2
inv-proof
[(((triple1) -> rule6))]
("dog" "is" "cold" "-")
((triple1) -> (rule6 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The cat likes the dog.
True
3
proof
[(((((triple2) -> rule1)) -> rule4))]
("cat" "likes" "dog" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The cat likes the dog.
("cat" "likes" "dog" "+")
int1
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int2
The cat does not like the dog.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule4))]
("cat" "likes" "dog" "-")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The cat likes the dog.
("cat" "likes" "dog" "+")
int1
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int2
The dog likes the dog.
True
4
proof
[(((((((triple1) -> rule6)) -> rule1)) -> rule4))]
("dog" "likes" "dog" "+")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
int3
The dog does not like the dog.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule1)) -> rule4))]
("dog" "likes" "dog" "-")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
int3
The squirrel does not like the dog.
Unknown
inv-rconc
[@2: The squirrel likes the dog.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("squirrel" "likes" "dog" "-")
The squirrel visits the squirrel.
Unknown
rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "visits" "squirrel" "+")
The bear does not visit the squirrel.
Unknown
inv-rconc
[@1: The bear visits the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "visits" "squirrel" "-")
The bear likes the dog.
Unknown
rconc
[@2: The bear likes the dog.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("bear" "likes" "dog" "+")
The squirrel is not big.
Unknown
inv-random
[@0: The squirrel is big.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "big" "-")
The bear is blue.
Unknown
random
[@0: The bear is blue.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "blue" "+")
The dog does not like the cat.
Unknown
inv-random
[@0: The dog likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "cat" "-")
The dog likes the squirrel.
Unknown
random
[@0: The dog likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "squirrel" "+")
@0: The bear eats the dog.[(triple1)] The cat is cold.[(triple2)] The cat likes the squirrel.[(triple3)] The dog eats the squirrel.[(triple4)] The dog is blue.[(triple5)] The dog is round.[(triple6)] The squirrel likes the cat.[(triple7)] @1: The cat visits the squirrel.[(((triple2) -> rule1))] The dog is cold.[(((triple1) -> rule6))] @2: The cat likes the dog.[(((((triple2) -> rule1)) -> rule4))] The dog visits the squirrel.[(((((triple1) -> rule6)) -> rule1))] @3: The dog likes the dog.[(((((((triple1) -> rule6)) -> rule1)) -> rule4))]
The bear eats the dog.
("bear" "eats" "dog" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple3
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
triple4
The dog is blue.
("dog" "is" "blue" "+")
triple5
The dog is round.
("dog" "is" "round" "+")
triple6
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple7
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
((triple2) -> (rule1 % int1))
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
((triple1) -> (rule6 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The cat likes the dog.
("cat" "likes" "dog" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The cat likes the dog.
("cat" "likes" "dog" "+")
int1
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
int2
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The dog likes the dog.
("dog" "likes" "dog" "+")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int2
The dog is cold.
("dog" "is" "cold" "+")
int3