The cat is not kind. The cat is not nice. The cat likes the dog. The cat likes the squirrel. The dog eats the cat. The dog eats the squirrel. The dog is cold. The dog does not like the squirrel. The squirrel eats the cat. The squirrel likes the cat. If someone eats the dog then they eat the squirrel. If the cat visits the dog and the cat likes the squirrel then the dog is kind. If the dog is not big then the dog does not visit the cat. If someone is big then they visit the cat. If the squirrel eats the cat then the cat visits the dog. If someone is kind then they do not visit the squirrel.
The cat is not kind.
("cat" "is" "kind" "-")
The cat is not nice.
("cat" "is" "nice" "-")
The cat likes the dog.
("cat" "likes" "dog" "+")
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The dog eats the cat.
("dog" "eats" "cat" "+")
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog does not like the squirrel.
("dog" "likes" "squirrel" "-")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
If someone eats the dog then they eat the squirrel.
((("someone" "eats" "dog" "+")) -> ("someone" "eats" "squirrel" "+"))
If the cat visits the dog and the cat likes the squirrel then the dog is kind.
((("cat" "visits" "dog" "+") ("cat" "likes" "squirrel" "+")) -> ("dog" "is" "kind" "+"))
If the dog is not big then the dog does not visit the cat.
((("dog" "is" "big" "~")) -> ("dog" "visits" "cat" "-"))
If someone is big then they visit the cat.
((("someone" "is" "big" "+")) -> ("someone" "visits" "cat" "+"))
If the squirrel eats the cat then the cat visits the dog.
((("squirrel" "eats" "cat" "+")) -> ("cat" "visits" "dog" "+"))
If someone is kind then they do not visit the squirrel.
((("someone" "is" "kind" "+")) -> ("someone" "visits" "squirrel" "-"))
The cat is not kind.
True
1
proof
[(triple1)]
("cat" "is" "kind" "-")
triple1
The cat does not like the dog.
False
1
inv-proof
[(triple3)]
("cat" "likes" "dog" "-")
triple3
The cat visits the dog.
True
2
proof
[(((triple9) -> rule5))]
("cat" "visits" "dog" "+")
((triple9) -> (rule5 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat does not visit the dog.
False
2
inv-proof
[(((triple9) -> rule5))]
("cat" "visits" "dog" "-")
((triple9) -> (rule5 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The dog is kind.
True
4
proof
[(((((triple9) -> rule5) triple4) -> rule2))]
("dog" "is" "kind" "+")
((((triple9) -> (rule5 % int2)) triple4) -> (rule2 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The dog is not kind.
False
4
inv-proof
[(((((triple9) -> rule5) triple4) -> rule2))]
("dog" "is" "kind" "-")
((((triple9) -> (rule5 % int2)) triple4) -> (rule2 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The dog does not visit the squirrel.
True
5
proof
[(((((((triple9) -> rule5) triple4) -> rule2)) -> rule6))]
("dog" "visits" "squirrel" "-")
((((((triple9) -> (rule5 % int3)) triple4) -> (rule2 % int2))) -> (rule6 % int1))
The dog does not visit the squirrel.
("dog" "visits" "squirrel" "-")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
The dog visits the squirrel.
False
5
inv-proof
[(((((((triple9) -> rule5) triple4) -> rule2)) -> rule6))]
("dog" "visits" "squirrel" "+")
((((((triple9) -> (rule5 % int3)) triple4) -> (rule2 % int2))) -> (rule6 % int1))
The dog does not visit the squirrel.
("dog" "visits" "squirrel" "-")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
The cat does not eat the squirrel.
Unknown
inv-rconc
[@1: The cat eats the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "eats" "squirrel" "-")
The cat visits the cat.
Unknown
rconc
[@1: The cat visits the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "visits" "cat" "+")
The squirrel does not eat the squirrel.
Unknown
inv-rconc
[@1: The squirrel eats the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "eats" "squirrel" "-")
The squirrel visits the cat.
Unknown
rconc
[@1: The squirrel visits the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "visits" "cat" "+")
The dog is not round.
Unknown
inv-random
[@0: The dog is round.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "round" "-")
The squirrel is round.
Unknown
random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "+")
The dog does not visit the dog.
Unknown
inv-random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
@0: The cat is not kind.[(triple1)] The cat is not nice.[(triple2)] The cat likes the dog.[(triple3)] The cat likes the squirrel.[(triple4)] The dog does not like the squirrel.[(triple8)] The dog eats the cat.[(triple5)] The dog eats the squirrel.[(triple6)] The dog is cold.[(triple7)] The squirrel eats the cat.[(triple9)] The squirrel likes the cat.[(triple10)] @1: The cat visits the dog.[(((triple9) -> rule5))] @2: The dog is kind.[(((((triple9) -> rule5) triple4) -> rule2))] @3: The dog does not visit the squirrel.[(((((((triple9) -> rule5) triple4) -> rule2)) -> rule6))]
The cat is not kind.
("cat" "is" "kind" "-")
triple1
The cat is not nice.
("cat" "is" "nice" "-")
triple2
The cat likes the dog.
("cat" "likes" "dog" "+")
triple3
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple4
The dog does not like the squirrel.
("dog" "likes" "squirrel" "-")
triple8
The dog eats the cat.
("dog" "eats" "cat" "+")
triple5
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
triple6
The dog is cold.
("dog" "is" "cold" "+")
triple7
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple9
The squirrel likes the cat.
("squirrel" "likes" "cat" "+")
triple10
The cat visits the dog.
("cat" "visits" "dog" "+")
((triple9) -> (rule5 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
((((triple9) -> (rule5 % int2)) triple4) -> (rule2 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The dog does not visit the squirrel.
("dog" "visits" "squirrel" "-")
((((((triple9) -> (rule5 % int3)) triple4) -> (rule2 % int2))) -> (rule6 % int1))
The dog does not visit the squirrel.
("dog" "visits" "squirrel" "-")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3