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