The cow is blue. The rabbit visits the cow. If the rabbit is red and the rabbit is nice then the rabbit visits the cow. If something is blue then it needs the rabbit. If something needs the rabbit then the rabbit is blue.
The cow is blue.
("cow" "is" "blue" "+")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
If the rabbit is red and the rabbit is nice then the rabbit visits the cow.
((("rabbit" "is" "red" "+") ("rabbit" "is" "nice" "+")) -> ("rabbit" "visits" "cow" "+"))
If something is blue then it needs the rabbit.
((("something" "is" "blue" "+")) -> ("something" "needs" "rabbit" "+"))
If something needs the rabbit then the rabbit is blue.
((("something" "needs" "rabbit" "+")) -> ("rabbit" "is" "blue" "+"))
The cow is blue.
True
1
proof
[(triple1)]
("cow" "is" "blue" "+")
triple1
The cow is not blue.
False
1
inv-proof
[(triple1)]
("cow" "is" "blue" "-")
triple1
The cow needs the rabbit.
True
2
proof
[(((triple1) -> rule2))]
("cow" "needs" "rabbit" "+")
((triple1) -> (rule2 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The cow does not need the rabbit.
False
2
inv-proof
[(((triple1) -> rule2))]
("cow" "needs" "rabbit" "-")
((triple1) -> (rule2 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The rabbit is blue.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("rabbit" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int2
The rabbit is not blue.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("rabbit" "is" "blue" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int2
The rabbit needs the rabbit.
True
4
proof
[(((((((triple1) -> rule2)) -> rule3)) -> rule2))]
("rabbit" "needs" "rabbit" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int3
The rabbit does not need the rabbit.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule3)) -> rule2))]
("rabbit" "needs" "rabbit" "-")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int3
The cow does not visit the cow.
Unknown
inv-random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "-")
The rabbit likes the cow.
Unknown
random
[@0: The rabbit likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "cow" "+")
The cow is not red.
Unknown
inv-random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "-")
The cow likes the rabbit.
Unknown
random
[@0: The cow likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "rabbit" "+")
The rabbit is not rough.
Unknown
inv-random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
The rabbit is not round.
Unknown
inv-random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
@0: The cow is blue.[(triple1)] The rabbit visits the cow.[(triple2)] @1: The cow needs the rabbit.[(((triple1) -> rule2))] @2: The rabbit is blue.[(((((triple1) -> rule2)) -> rule3))] @3: The rabbit needs the rabbit.[(((((((triple1) -> rule2)) -> rule3)) -> rule2))]
The cow is blue.
("cow" "is" "blue" "+")
triple1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple2
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
((triple1) -> (rule2 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int3