The cow is young. The dog is green. The rabbit needs the cow. The squirrel needs the cow. If someone needs the cow then they see the dog. If someone needs the dog and the dog sees the rabbit then they are green. If someone needs the cow then the cow is green. If someone sees the dog then they need the cow. If someone chases the dog then they see the rabbit. If someone needs the rabbit then they are young.
The cow is young.
("cow" "is" "young" "+")
The dog is green.
("dog" "is" "green" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
If someone needs the cow then they see the dog.
((("someone" "needs" "cow" "+")) -> ("someone" "sees" "dog" "+"))
If someone needs the dog and the dog sees the rabbit then they are green.
((("someone" "needs" "dog" "+") ("dog" "sees" "rabbit" "+")) -> ("someone" "is" "green" "+"))
If someone needs the cow then the cow is green.
((("someone" "needs" "cow" "+")) -> ("cow" "is" "green" "+"))
If someone sees the dog then they need the cow.
((("someone" "sees" "dog" "+")) -> ("someone" "needs" "cow" "+"))
If someone chases the dog then they see the rabbit.
((("someone" "chases" "dog" "+")) -> ("someone" "sees" "rabbit" "+"))
If someone needs the rabbit then they are young.
((("someone" "needs" "rabbit" "+")) -> ("someone" "is" "young" "+"))
The rabbit needs the cow.
True
1
proof
[(triple3)]
("rabbit" "needs" "cow" "+")
triple3
The cow is not young.
False
1
inv-proof
[(triple1)]
("cow" "is" "young" "-")
triple1
The cow is green.
True
2
proof
[(((triple3) -> rule3) OR ((triple4) -> rule3))]
("cow" "is" "green" "+")
((triple3) -> (rule3 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
((triple4) -> (rule3 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is not green.
False
2
inv-proof
[(((triple3) -> rule3) OR ((triple4) -> rule3))]
("cow" "is" "green" "-")
((triple3) -> (rule3 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
((triple4) -> (rule3 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow does not need the cow.
Unknown
inv-rconc
[@2: The cow needs the cow.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("cow" "needs" "cow" "-")
The rabbit is green.
Unknown
rconc
[@1: The rabbit is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "green" "+")
The cow does not chase the cow.
Unknown
inv-random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "-")
The rabbit is blue.
Unknown
random
[@0: The rabbit is blue.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "blue" "+")
@0: The cow is young.[(triple1)] The dog is green.[(triple2)] The rabbit needs the cow.[(triple3)] The squirrel needs the cow.[(triple4)] @1: The cow is green.[(((triple3) -> rule3) OR ((triple4) -> rule3))] The rabbit sees the dog.[(((triple3) -> rule1))] The squirrel sees the dog.[(((triple4) -> rule1))]
The cow is young.
("cow" "is" "young" "+")
triple1
The dog is green.
("dog" "is" "green" "+")
triple2
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple3
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple4
The cow is green.
("cow" "is" "green" "+")
((triple3) -> (rule3 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
((triple4) -> (rule3 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
((triple3) -> (rule1 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
((triple4) -> (rule1 % int1))
The squirrel sees the dog.
("squirrel" "sees" "dog" "+")
int1