The cat eats the dog. The cat eats the squirrel. The cat is green. The cat is kind. The cat is red. The cat is rough. The cat sees the dog. The cat sees the squirrel. The cat visits the dog. The dog eats the cat. The dog eats the squirrel. The dog sees the cat. The dog sees the squirrel. The dog visits the cat. The dog visits the squirrel. The squirrel sees the cat. If someone sees the dog then the dog eats the squirrel. If the cat is big then the cat is rough. If someone sees the dog then they are big.
The cat eats the dog.
("cat" "eats" "dog" "+")
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The cat is green.
("cat" "is" "green" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat sees the dog.
("cat" "sees" "dog" "+")
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
The cat visits the dog.
("cat" "visits" "dog" "+")
The dog eats the cat.
("dog" "eats" "cat" "+")
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
If someone sees the dog then the dog eats the squirrel.
((("someone" "sees" "dog" "+")) -> ("dog" "eats" "squirrel" "+"))
If the cat is big then the cat is rough.
((("cat" "is" "big" "+")) -> ("cat" "is" "rough" "+"))
If someone sees the dog then they are big.
((("someone" "sees" "dog" "+")) -> ("someone" "is" "big" "+"))
The dog sees the cat.
True
1
proof
[(triple12)]
("dog" "sees" "cat" "+")
triple12
The cat does not eat the squirrel.
False
1
inv-proof
[(triple2)]
("cat" "eats" "squirrel" "-")
triple2
The cat is big.
True
2
proof
[(((triple7) -> rule3))]
("cat" "is" "big" "+")
((triple7) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is not big.
False
2
inv-proof
[(((triple7) -> rule3))]
("cat" "is" "big" "-")
((triple7) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The squirrel is not big.
Unknown
inv-rconc
[@1: The squirrel is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "big" "-")
The dog is big.
Unknown
rconc
[@1: The dog is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "big" "+")
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 dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
@0: The cat eats the dog.[(triple1)] The cat eats the squirrel.[(triple2)] The cat is green.[(triple3)] The cat is kind.[(triple4)] The cat is red.[(triple5)] The cat is rough.[(triple6 OR ((((triple7) -> rule3)) -> rule2))] The cat sees the dog.[(triple7)] The cat sees the squirrel.[(triple8)] The cat visits the dog.[(triple9)] The dog eats the cat.[(triple10)] The dog eats the squirrel.[(triple11 OR ((triple7) -> rule1))] The dog sees the cat.[(triple12)] The dog sees the squirrel.[(triple13)] The dog visits the cat.[(triple14)] The dog visits the squirrel.[(triple15)] The squirrel sees the cat.[(triple16)] @1: The cat is big.[(((triple7) -> rule3))]
The cat eats the dog.
("cat" "eats" "dog" "+")
triple1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple2
The cat is green.
("cat" "is" "green" "+")
triple3
The cat is kind.
("cat" "is" "kind" "+")
triple4
The cat is red.
("cat" "is" "red" "+")
triple5
The cat is rough.
("cat" "is" "rough" "+")
triple6
((((triple7) -> (rule3 % int2))) -> (rule2 % int1))
The cat is rough.
("cat" "is" "rough" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The cat sees the dog.
("cat" "sees" "dog" "+")
triple7
The cat sees the squirrel.
("cat" "sees" "squirrel" "+")
triple8
The cat visits the dog.
("cat" "visits" "dog" "+")
triple9
The dog eats the cat.
("dog" "eats" "cat" "+")
triple10
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
triple11
((triple7) -> (rule1 % int1))
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
triple12
The dog sees the squirrel.
("dog" "sees" "squirrel" "+")
triple13
The dog visits the cat.
("dog" "visits" "cat" "+")
triple14
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
triple15
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple16
The cat is big.
("cat" "is" "big" "+")
((triple7) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1