The dog eats the squirrel. The dog is kind. The squirrel is big. If something chases the dog and the dog sees the squirrel then the squirrel is big. If something is big and kind then it eats the squirrel. If something sees the squirrel and the squirrel is young then the squirrel chases the dog. If something sees the squirrel then the squirrel sees the dog. If something is big then it eats the squirrel. If something eats the dog and it sees the squirrel then the dog is kind. If something sees the squirrel and it is big then the squirrel sees the dog. If something chases the squirrel then the squirrel eats the dog.
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
The dog is kind.
("dog" "is" "kind" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
If something chases the dog and the dog sees the squirrel then the squirrel is big.
((("something" "chases" "dog" "+") ("dog" "sees" "squirrel" "+")) -> ("squirrel" "is" "big" "+"))
If something is big and kind then it eats the squirrel.
((("something" "is" "big" "+") ("something" "is" "kind" "+")) -> ("something" "eats" "squirrel" "+"))
If something sees the squirrel and the squirrel is young then the squirrel chases the dog.
((("something" "sees" "squirrel" "+") ("squirrel" "is" "young" "+")) -> ("squirrel" "chases" "dog" "+"))
If something sees the squirrel then the squirrel sees the dog.
((("something" "sees" "squirrel" "+")) -> ("squirrel" "sees" "dog" "+"))
If something is big then it eats the squirrel.
((("something" "is" "big" "+")) -> ("something" "eats" "squirrel" "+"))
If something eats the dog and it sees the squirrel then the dog is kind.
((("something" "eats" "dog" "+") ("something" "sees" "squirrel" "+")) -> ("dog" "is" "kind" "+"))
If something sees the squirrel and it is big then the squirrel sees the dog.
((("something" "sees" "squirrel" "+") ("something" "is" "big" "+")) -> ("squirrel" "sees" "dog" "+"))
If something chases the squirrel then the squirrel eats the dog.
((("something" "chases" "squirrel" "+")) -> ("squirrel" "eats" "dog" "+"))
The dog eats the squirrel.
True
1
proof
[(triple1)]
("dog" "eats" "squirrel" "+")
triple1
The dog is not kind.
False
1
inv-proof
[(triple2)]
("dog" "is" "kind" "-")
triple2
The squirrel eats the squirrel.
True
2
proof
[(((triple3) -> rule5))]
("squirrel" "eats" "squirrel" "+")
((triple3) -> (rule5 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel does not eat the squirrel.
False
2
inv-proof
[(((triple3) -> rule5))]
("squirrel" "eats" "squirrel" "-")
((triple3) -> (rule5 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1
The squirrel does not chase the dog.
Unknown
inv-rconc
[@1: The squirrel chases the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "chases" "dog" "-")
The squirrel eats the dog.
Unknown
rconc
[@1: The squirrel eats the dog.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("squirrel" "eats" "dog" "+")
The dog does not see the squirrel.
Unknown
inv-random
[@0: The dog sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "squirrel" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
@0: The dog eats the squirrel.[(triple1)] The dog is kind.[(triple2)] The squirrel is big.[(triple3)] @1: The squirrel eats the squirrel.[(((triple3) -> rule5))]
The dog eats the squirrel.
("dog" "eats" "squirrel" "+")
triple1
The dog is kind.
("dog" "is" "kind" "+")
triple2
The squirrel is big.
("squirrel" "is" "big" "+")
triple3
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
((triple3) -> (rule5 % int1))
The squirrel eats the squirrel.
("squirrel" "eats" "squirrel" "+")
int1