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