The dog likes the lion. The lion needs the dog. The rabbit needs the dog. The squirrel is young. If something needs the dog then the dog is blue. If the rabbit is green then the rabbit is blue. If something chases the squirrel then it likes the dog. If something is blue then it needs the rabbit. If something needs the dog and it is rough then the dog likes the lion. Kind things are green. If the squirrel is blue and the squirrel chases the lion then the lion is green. If something chases the rabbit then the rabbit likes the dog.
The dog likes the lion.
("dog" "likes" "lion" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
If something needs the dog then the dog is blue.
((("something" "needs" "dog" "+")) -> ("dog" "is" "blue" "+"))
If the rabbit is green then the rabbit is blue.
((("rabbit" "is" "green" "+")) -> ("rabbit" "is" "blue" "+"))
If something chases the squirrel then it likes the dog.
((("something" "chases" "squirrel" "+")) -> ("something" "likes" "dog" "+"))
If something is blue then it needs the rabbit.
((("something" "is" "blue" "+")) -> ("something" "needs" "rabbit" "+"))
If something needs the dog and it is rough then the dog likes the lion.
((("something" "needs" "dog" "+") ("something" "is" "rough" "+")) -> ("dog" "likes" "lion" "+"))
Kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If the squirrel is blue and the squirrel chases the lion then the lion is green.
((("squirrel" "is" "blue" "+") ("squirrel" "chases" "lion" "+")) -> ("lion" "is" "green" "+"))
If something chases the rabbit then the rabbit likes the dog.
((("something" "chases" "rabbit" "+")) -> ("rabbit" "likes" "dog" "+"))
The squirrel is young.
True
1
proof
[(triple4)]
("squirrel" "is" "young" "+")
triple4
The rabbit does not need the dog.
False
1
inv-proof
[(triple3)]
("rabbit" "needs" "dog" "-")
triple3
The dog is blue.
True
2
proof
[(((triple2) -> rule1) OR ((triple3) -> rule1))]
("dog" "is" "blue" "+")
((triple2) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
((triple3) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog is not blue.
False
2
inv-proof
[(((triple2) -> rule1) OR ((triple3) -> rule1))]
("dog" "is" "blue" "-")
((triple2) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
((triple3) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog needs the rabbit.
True
3
proof
[(((((triple2) -> rule1)) -> rule4) OR ((((triple3) -> rule1)) -> rule4))]
("dog" "needs" "rabbit" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog does not need the rabbit.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule4) OR ((((triple3) -> rule1)) -> rule4))]
("dog" "needs" "rabbit" "-")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The rabbit is not green.
Unknown
inv-rconc
[@1: The rabbit is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "is" "green" "-")
The squirrel is green.
Unknown
rconc
[@1: The squirrel is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "is" "green" "+")
The lion does not like the dog.
Unknown
inv-rconc
[@1: The lion likes the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "likes" "dog" "-")
The squirrel needs the lion.
Unknown
random
[@0: The squirrel needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "lion" "+")
The dog does not need the squirrel.
Unknown
inv-random
[@0: The dog needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "squirrel" "-")
The dog needs the lion.
Unknown
random
[@0: The dog needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "lion" "+")
@0: The dog likes the lion.[(triple1)] The lion needs the dog.[(triple2)] The rabbit needs the dog.[(triple3)] The squirrel is young.[(triple4)] @1: The dog is blue.[(((triple2) -> rule1) OR ((triple3) -> rule1))] @2: The dog needs the rabbit.[(((((triple2) -> rule1)) -> rule4) OR ((((triple3) -> rule1)) -> rule4))]
The dog likes the lion.
("dog" "likes" "lion" "+")
triple1
The lion needs the dog.
("lion" "needs" "dog" "+")
triple2
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple3
The squirrel is young.
("squirrel" "is" "young" "+")
triple4
The dog is blue.
("dog" "is" "blue" "+")
((triple2) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
((triple3) -> (rule1 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2