The dog is young. The squirrel chases the dog. The squirrel is red. If something likes the squirrel then it likes the dog. If the squirrel needs the dog then the dog likes the squirrel. If something is cold then it is red. If something is cold then it needs the dog. If something chases the dog then it does not need the dog. Red things are not young. If something chases the dog and it does not need the dog then the dog does not chase the squirrel. If something likes the dog and the dog is not nice then the dog does not chase the squirrel.
The dog is young.
("dog" "is" "young" "+")
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
If something likes the squirrel then it likes the dog.
((("something" "likes" "squirrel" "+")) -> ("something" "likes" "dog" "+"))
If the squirrel needs the dog then the dog likes the squirrel.
((("squirrel" "needs" "dog" "+")) -> ("dog" "likes" "squirrel" "+"))
If something is cold then it is red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If something is cold then it needs the dog.
((("something" "is" "cold" "+")) -> ("something" "needs" "dog" "+"))
If something chases the dog then it does not need the dog.
((("something" "chases" "dog" "+")) -> ("something" "needs" "dog" "-"))
Red things are not young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "-"))
If something chases the dog and it does not need the dog then the dog does not chase the squirrel.
((("something" "chases" "dog" "+") ("something" "needs" "dog" "~")) -> ("dog" "chases" "squirrel" "-"))
If something likes the dog and the dog is not nice then the dog does not chase the squirrel.
((("something" "likes" "dog" "+") ("dog" "is" "nice" "~")) -> ("dog" "chases" "squirrel" "-"))
The dog is young.
True
1
proof
[(triple1)]
("dog" "is" "young" "+")
triple1
The squirrel is not red.
False
1
inv-proof
[(triple3)]
("squirrel" "is" "red" "-")
triple3
The squirrel does not need the dog.
True
2
proof
[(((triple2) -> rule5))]
("squirrel" "needs" "dog" "-")
((triple2) -> (rule5 % int1))
The squirrel does not need the dog.
("squirrel" "needs" "dog" "-")
int1
The squirrel needs the dog.
False
2
inv-proof
[(((triple2) -> rule5))]
("squirrel" "needs" "dog" "+")
((triple2) -> (rule5 % int1))
The squirrel does not need the dog.
("squirrel" "needs" "dog" "-")
int1
The dog is not red.
Unknown
inv-rconc
[@1: The dog is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "red" "-")
The dog needs the dog.
Unknown
rconc
[@1: The dog needs the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "needs" "dog" "+")
The dog is not nice.
Unknown
inv-random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
@0: The dog is young.[(triple1)] The squirrel chases the dog.[(triple2)] The squirrel is red.[(triple3)] @1: The squirrel does not need the dog.[(((triple2) -> rule5))] The squirrel is not young.[(((triple3) -> rule6))] @2: The dog does not chase the squirrel.[(((triple2 ((triple2) -> rule5)) -> rule7))]
The dog is young.
("dog" "is" "young" "+")
triple1
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
triple2
The squirrel is red.
("squirrel" "is" "red" "+")
triple3
The squirrel does not need the dog.
("squirrel" "needs" "dog" "-")
((triple2) -> (rule5 % int1))
The squirrel does not need the dog.
("squirrel" "needs" "dog" "-")
int1
The squirrel is not young.
("squirrel" "is" "young" "-")
((triple3) -> (rule6 % int1))
The squirrel is not young.
("squirrel" "is" "young" "-")
int1
The dog does not chase the squirrel.
("dog" "chases" "squirrel" "-")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule7 % int1))
The dog does not chase the squirrel.
("dog" "chases" "squirrel" "-")
int1
The squirrel does not need the dog.
("squirrel" "needs" "dog" "-")
int2