The cat is nice. The cat is rough. The cat needs the squirrel. The dog is not big. The dog is cold. The dog is kind. The dog is rough. The dog needs the cat. The dog does not need the squirrel. The dog visits the cat. The dog visits the squirrel. The squirrel chases the dog. The squirrel is cold. The squirrel is kind. The squirrel visits the cat. The squirrel visits the dog. If someone is nice and they do not chase the squirrel then they need the dog. If someone needs the squirrel then they do not need the dog. If someone visits the squirrel then they need the dog. If someone is cold then they chase the cat. If the squirrel chases the cat then the cat is kind. If someone chases the cat and they are not kind then they chase the dog.
The cat is nice.
("cat" "is" "nice" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The dog is not big.
("dog" "is" "big" "-")
The dog is cold.
("dog" "is" "cold" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The dog does not need the squirrel.
("dog" "needs" "squirrel" "-")
The dog visits the cat.
("dog" "visits" "cat" "+")
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
If someone is nice and they do not chase the squirrel then they need the dog.
((("someone" "is" "nice" "+") ("someone" "chases" "squirrel" "~")) -> ("someone" "needs" "dog" "+"))
If someone needs the squirrel then they do not need the dog.
((("someone" "needs" "squirrel" "+")) -> ("someone" "needs" "dog" "-"))
If someone visits the squirrel then they need the dog.
((("someone" "visits" "squirrel" "+")) -> ("someone" "needs" "dog" "+"))
If someone is cold then they chase the cat.
((("someone" "is" "cold" "+")) -> ("someone" "chases" "cat" "+"))
If the squirrel chases the cat then the cat is kind.
((("squirrel" "chases" "cat" "+")) -> ("cat" "is" "kind" "+"))
If someone chases the cat and they are not kind then they chase the dog.
((("someone" "chases" "cat" "+") ("someone" "is" "kind" "~")) -> ("someone" "chases" "dog" "+"))
The squirrel visits the dog.
True
1
proof
[(triple16)]
("squirrel" "visits" "dog" "+")
triple16
The dog is not kind.
False
1
inv-proof
[(triple6)]
("dog" "is" "kind" "-")
triple6
The squirrel chases the cat.
True
2
proof
[(((triple13) -> rule4))]
("squirrel" "chases" "cat" "+")
((triple13) -> (rule4 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
The dog does not need the dog.
False
2
inv-proof
[(((triple11) -> rule3))]
("dog" "needs" "dog" "-")
((triple11) -> (rule3 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The cat is kind.
True
3
proof
[(((((triple13) -> rule4)) -> rule5))]
("cat" "is" "kind" "+")
((((triple13) -> (rule4 % int2))) -> (rule5 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int2
The cat is not kind.
False
3
inv-proof
[(((((triple13) -> rule4)) -> rule5))]
("cat" "is" "kind" "-")
((((triple13) -> (rule4 % int2))) -> (rule5 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int2
The cat does not chase the cat.
Unknown
inv-rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "chases" "cat" "-")
The dog chases the dog.
Unknown
rconc
[@1: The dog chases the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "chases" "dog" "+")
The cat does not chase the dog.
Unknown
inv-rconc
[@1: The cat chases the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cat" "chases" "dog" "-")
The squirrel is nice.
Unknown
random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
@0: The cat is nice.[(triple1)] The cat is rough.[(triple2)] The cat needs the squirrel.[(triple3)] The dog does not need the squirrel.[(triple9)] The dog is cold.[(triple5)] The dog is kind.[(triple6)] The dog is not big.[(triple4)] The dog is rough.[(triple7)] The dog needs the cat.[(triple8)] The dog visits the cat.[(triple10)] The dog visits the squirrel.[(triple11)] The squirrel chases the dog.[(triple12)] The squirrel is cold.[(triple13)] The squirrel is kind.[(triple14)] The squirrel visits the cat.[(triple15)] The squirrel visits the dog.[(triple16)] @1: The cat does not need the dog.[(((triple3) -> rule2))] The dog chases the cat.[(((triple5) -> rule4))] The dog needs the dog.[(((triple11) -> rule3))] The squirrel chases the cat.[(((triple13) -> rule4))] @2: The cat is kind.[(((((triple13) -> rule4)) -> rule5))]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The cat is rough.
("cat" "is" "rough" "+")
triple2
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple3
The dog does not need the squirrel.
("dog" "needs" "squirrel" "-")
triple9
The dog is cold.
("dog" "is" "cold" "+")
triple5
The dog is kind.
("dog" "is" "kind" "+")
triple6
The dog is not big.
("dog" "is" "big" "-")
triple4
The dog is rough.
("dog" "is" "rough" "+")
triple7
The dog needs the cat.
("dog" "needs" "cat" "+")
triple8
The dog visits the cat.
("dog" "visits" "cat" "+")
triple10
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
triple11
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
triple12
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple13
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple14
The squirrel visits the cat.
("squirrel" "visits" "cat" "+")
triple15
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple16
The cat does not need the dog.
("cat" "needs" "dog" "-")
((triple3) -> (rule2 % int1))
The cat does not need the dog.
("cat" "needs" "dog" "-")
int1
The dog chases the cat.
("dog" "chases" "cat" "+")
((triple5) -> (rule4 % int1))
The dog chases the cat.
("dog" "chases" "cat" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
((triple11) -> (rule3 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
((triple13) -> (rule4 % int1))
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
((((triple13) -> (rule4 % int2))) -> (rule5 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The squirrel chases the cat.
("squirrel" "chases" "cat" "+")
int2