The cow chases the rabbit. The rabbit is rough. The rabbit visits the cow. If someone is nice then they see the cow. If someone is red then they see the cow. If someone chases the rabbit then the rabbit chases the cow. If someone sees the cow and they visit the cow then the cow is green. If someone sees the rabbit and they chase the cow then the cow visits the rabbit. If the rabbit visits the cow then the rabbit is red.
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
If someone is nice then they see the cow.
((("someone" "is" "nice" "+")) -> ("someone" "sees" "cow" "+"))
If someone is red then they see the cow.
((("someone" "is" "red" "+")) -> ("someone" "sees" "cow" "+"))
If someone chases the rabbit then the rabbit chases the cow.
((("someone" "chases" "rabbit" "+")) -> ("rabbit" "chases" "cow" "+"))
If someone sees the cow and they visit the cow then the cow is green.
((("someone" "sees" "cow" "+") ("someone" "visits" "cow" "+")) -> ("cow" "is" "green" "+"))
If someone sees the rabbit and they chase the cow then the cow visits the rabbit.
((("someone" "sees" "rabbit" "+") ("someone" "chases" "cow" "+")) -> ("cow" "visits" "rabbit" "+"))
If the rabbit visits the cow then the rabbit is red.
((("rabbit" "visits" "cow" "+")) -> ("rabbit" "is" "red" "+"))
The rabbit visits the cow.
True
1
proof
[(triple3)]
("rabbit" "visits" "cow" "+")
triple3
The rabbit does not visit the cow.
False
1
inv-proof
[(triple3)]
("rabbit" "visits" "cow" "-")
triple3
The rabbit is red.
True
2
proof
[(((triple3) -> rule6))]
("rabbit" "is" "red" "+")
((triple3) -> (rule6 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit does not chase the cow.
False
2
inv-proof
[(((triple1) -> rule3))]
("rabbit" "chases" "cow" "-")
((triple1) -> (rule3 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The rabbit sees the cow.
True
3
proof
[(((((triple3) -> rule6)) -> rule2))]
("rabbit" "sees" "cow" "+")
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit does not see the cow.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule2))]
("rabbit" "sees" "cow" "-")
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The cow is green.
True
5
proof
[(((((((triple3) -> rule6)) -> rule2) triple3) -> rule4))]
("cow" "is" "green" "+")
((((((triple3) -> (rule6 % int3))) -> (rule2 % int2)) triple3) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The cow is not green.
False
5
inv-proof
[(((((((triple3) -> rule6)) -> rule2) triple3) -> rule4))]
("cow" "is" "green" "-")
((((((triple3) -> (rule6 % int3))) -> (rule2 % int2)) triple3) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The cow does not see the cow.
Unknown
inv-rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "sees" "cow" "-")
The cow visits the rabbit.
Unknown
rconc
[@1: The cow visits the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "visits" "rabbit" "+")
The cow is not cold.
Unknown
inv-random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
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 cow sees the rabbit.
Unknown
random
[@0: The cow sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "rabbit" "+")
The rabbit does not chase the rabbit.
Unknown
inv-random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
@0: The cow chases the rabbit.[(triple1)] The rabbit is rough.[(triple2)] The rabbit visits the cow.[(triple3)] @1: The rabbit chases the cow.[(((triple1) -> rule3))] The rabbit is red.[(((triple3) -> rule6))] @2: The rabbit sees the cow.[(((((triple3) -> rule6)) -> rule2))] @3: The cow is green.[(((((((triple3) -> rule6)) -> rule2) triple3) -> rule4))]
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple1
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple2
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple3
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
((triple1) -> (rule3 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
((triple3) -> (rule6 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The cow is green.
("cow" "is" "green" "+")
((((((triple3) -> (rule6 % int3))) -> (rule2 % int2)) triple3) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3