The cow chases the rabbit. The cow is big. The cow is not blue. The cow is kind. The cow is red. The cow needs the rabbit. The cow sees the rabbit. The rabbit is blue. The rabbit needs the cow. The rabbit does not see the cow. If something is red then it needs the cow. If the cow is red then the cow needs the rabbit. If something is big and it needs the rabbit then it does not chase the cow. If something is young and it sees the rabbit then the rabbit needs the cow. If something sees the cow and it does not chase the cow then it is young. If something needs the cow and the cow sees the rabbit then it is young.
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is not blue.
("cow" "is" "blue" "-")
The cow is kind.
("cow" "is" "kind" "+")
The cow is red.
("cow" "is" "red" "+")
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
The rabbit does not see the cow.
("rabbit" "sees" "cow" "-")
If something is red then it needs the cow.
((("something" "is" "red" "+")) -> ("something" "needs" "cow" "+"))
If the cow is red then the cow needs the rabbit.
((("cow" "is" "red" "+")) -> ("cow" "needs" "rabbit" "+"))
If something is big and it needs the rabbit then it does not chase the cow.
((("something" "is" "big" "+") ("something" "needs" "rabbit" "+")) -> ("something" "chases" "cow" "-"))
If something is young and it sees the rabbit then the rabbit needs the cow.
((("something" "is" "young" "+") ("something" "sees" "rabbit" "+")) -> ("rabbit" "needs" "cow" "+"))
If something sees the cow and it does not chase the cow then it is young.
((("something" "sees" "cow" "+") ("something" "chases" "cow" "~")) -> ("something" "is" "young" "+"))
If something needs the cow and the cow sees the rabbit then it is young.
((("something" "needs" "cow" "+") ("cow" "sees" "rabbit" "+")) -> ("something" "is" "young" "+"))
The rabbit needs the cow.
True
1
proof
[(triple9 OR ((((((triple5) -> rule1) triple7) -> rule6) triple7) -> rule4))]
("rabbit" "needs" "cow" "+")
triple9
((((((triple5) -> (rule1 % int3)) triple7) -> (rule6 % int2)) triple7) -> (rule4 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
int3
The cow does not chase the rabbit.
False
1
inv-proof
[(triple1)]
("cow" "chases" "rabbit" "-")
triple1
The cow does not chase the cow.
True
3
proof
[(((triple2 triple6) -> rule3) OR ((triple2 ((triple5) -> rule2)) -> rule3))]
("cow" "chases" "cow" "-")
((triple2 triple6) -> (rule3 % int1))
The cow does not chase the cow.
("cow" "chases" "cow" "-")
int1
((triple2 ((triple5) -> (rule2 % int2))) -> (rule3 % int1))
The cow does not chase the cow.
("cow" "chases" "cow" "-")
int1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int2
The rabbit is not young.
False
3
inv-proof
[(((triple9 triple7) -> rule6) OR ((((((((triple5) -> rule1) triple7) -> rule6) triple7) -> rule4) triple7) -> rule6))]
("rabbit" "is" "young" "-")
((triple9 triple7) -> (rule6 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
((((((((triple5) -> (rule1 % int4)) triple7) -> (rule6 % int3)) triple7) -> (rule4 % int2)) triple7) -> (rule6 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The cow is young.
("cow" "is" "young" "+")
int3
The cow needs the cow.
("cow" "needs" "cow" "+")
int4
The cow is young.
True
4
proof
[(((((triple5) -> rule1) triple7) -> rule6))]
("cow" "is" "young" "+")
((((triple5) -> (rule1 % int2)) triple7) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The cow is not young.
False
4
inv-proof
[(((((triple5) -> rule1) triple7) -> rule6))]
("cow" "is" "young" "-")
((((triple5) -> (rule1 % int2)) triple7) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2
The rabbit is not red.
Unknown
inv-random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
The rabbit does not need the rabbit.
Unknown
inv-random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "-")
The rabbit chases the cow.
Unknown
random
[@0: The rabbit chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "cow" "+")
@0: The cow chases the rabbit.[(triple1)] The cow is big.[(triple2)] The cow is kind.[(triple4)] The cow is not blue.[(triple3)] The cow is red.[(triple5)] The cow needs the rabbit.[(triple6 OR ((triple5) -> rule2))] The cow sees the rabbit.[(triple7)] The rabbit does not see the cow.[(triple10)] The rabbit is blue.[(triple8)] The rabbit needs the cow.[(triple9 OR ((((((triple5) -> rule1) triple7) -> rule6) triple7) -> rule4))] @1: The cow does not chase the cow.[(((triple2 triple6) -> rule3) OR ((triple2 ((triple5) -> rule2)) -> rule3))] The cow needs the cow.[(((triple5) -> rule1))] The rabbit is young.[(((triple9 triple7) -> rule6) OR ((((((((triple5) -> rule1) triple7) -> rule6) triple7) -> rule4) triple7) -> rule6))] @2: The cow is young.[(((((triple5) -> rule1) triple7) -> rule6))]
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple1
The cow is big.
("cow" "is" "big" "+")
triple2
The cow is kind.
("cow" "is" "kind" "+")
triple4
The cow is not blue.
("cow" "is" "blue" "-")
triple3
The cow is red.
("cow" "is" "red" "+")
triple5
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
triple6
((triple5) -> (rule2 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple7
The rabbit does not see the cow.
("rabbit" "sees" "cow" "-")
triple10
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple8
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple9
((((((triple5) -> (rule1 % int3)) triple7) -> (rule6 % int2)) triple7) -> (rule4 % int1))
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int1
The cow is young.
("cow" "is" "young" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
int3
The cow does not chase the cow.
("cow" "chases" "cow" "-")
((triple2 triple6) -> (rule3 % int1))
The cow does not chase the cow.
("cow" "chases" "cow" "-")
int1
((triple2 ((triple5) -> (rule2 % int2))) -> (rule3 % int1))
The cow does not chase the cow.
("cow" "chases" "cow" "-")
int1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int2
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple5) -> (rule1 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
((triple9 triple7) -> (rule6 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
((((((((triple5) -> (rule1 % int4)) triple7) -> (rule6 % int3)) triple7) -> (rule4 % int2)) triple7) -> (rule6 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
int2
The cow is young.
("cow" "is" "young" "+")
int3
The cow needs the cow.
("cow" "needs" "cow" "+")
int4
The cow is young.
("cow" "is" "young" "+")
((((triple5) -> (rule1 % int2)) triple7) -> (rule6 % int1))
The cow is young.
("cow" "is" "young" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
int2