The cow is kind. The rabbit is red. If something sees the cow then the cow does not need the rabbit. If something is kind and it visits the rabbit then the rabbit visits the cow. If something needs the cow and the cow visits the rabbit then the rabbit visits the cow. If something is red then it sees the cow. If something visits the rabbit then it is not nice. If something visits the rabbit and it is not red then it sees the rabbit. If the cow is kind and the cow does not need the rabbit then the cow is green. If something needs the rabbit and the rabbit needs the cow then the cow is not green.
The cow is kind.
("cow" "is" "kind" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
If something sees the cow then the cow does not need the rabbit.
((("something" "sees" "cow" "+")) -> ("cow" "needs" "rabbit" "-"))
If something is kind and it visits the rabbit then the rabbit visits the cow.
((("something" "is" "kind" "+") ("something" "visits" "rabbit" "+")) -> ("rabbit" "visits" "cow" "+"))
If something needs the cow and the cow visits the rabbit then the rabbit visits the cow.
((("something" "needs" "cow" "+") ("cow" "visits" "rabbit" "+")) -> ("rabbit" "visits" "cow" "+"))
If something is red then it sees the cow.
((("something" "is" "red" "+")) -> ("something" "sees" "cow" "+"))
If something visits the rabbit then it is not nice.
((("something" "visits" "rabbit" "+")) -> ("something" "is" "nice" "-"))
If something visits the rabbit and it is not red then it sees the rabbit.
((("something" "visits" "rabbit" "+") ("something" "is" "red" "~")) -> ("something" "sees" "rabbit" "+"))
If the cow is kind and the cow does not need the rabbit then the cow is green.
((("cow" "is" "kind" "+") ("cow" "needs" "rabbit" "~")) -> ("cow" "is" "green" "+"))
If something needs the rabbit and the rabbit needs the cow then the cow is not green.
((("something" "needs" "rabbit" "+") ("rabbit" "needs" "cow" "+")) -> ("cow" "is" "green" "-"))
The cow is kind.
True
1
proof
[(triple1)]
("cow" "is" "kind" "+")
triple1
The rabbit is not red.
False
1
inv-proof
[(triple2)]
("rabbit" "is" "red" "-")
triple2
The rabbit sees the cow.
True
2
proof
[(((triple2) -> rule4))]
("rabbit" "sees" "cow" "+")
((triple2) -> (rule4 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The rabbit does not see the cow.
False
2
inv-proof
[(((triple2) -> rule4))]
("rabbit" "sees" "cow" "-")
((triple2) -> (rule4 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The cow does not need the rabbit.
True
3
proof
[(((((triple2) -> rule4)) -> rule1))]
("cow" "needs" "rabbit" "-")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
The cow does not need the rabbit.
("cow" "needs" "rabbit" "-")
int1
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int2
The cow needs the rabbit.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule1))]
("cow" "needs" "rabbit" "+")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
The cow does not need the rabbit.
("cow" "needs" "rabbit" "-")
int1
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int2
The cow is green.
True
5
proof
[(((triple1 ((((triple2) -> rule4)) -> rule1)) -> rule7))]
("cow" "is" "green" "+")
((triple1 ((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow does not need the rabbit.
("cow" "needs" "rabbit" "-")
int2
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int3
The cow is not green.
False
5
inv-proof
[(((triple1 ((((triple2) -> rule4)) -> rule1)) -> rule7))]
("cow" "is" "green" "-")
((triple1 ((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow does not need the rabbit.
("cow" "needs" "rabbit" "-")
int2
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int3
The rabbit does not visit the cow.
Unknown
inv-rconc
[@1: The rabbit visits the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "visits" "cow" "-")
The cow sees the rabbit.
Unknown
rconc
[@1: The cow sees the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "sees" "rabbit" "+")
The rabbit does not see the rabbit.
Unknown
inv-rconc
[@1: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "sees" "rabbit" "-")
The cow sees the cow.
Unknown
rconc
[@1: The cow sees the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "sees" "cow" "+")
The rabbit is not cold.
Unknown
inv-random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
The rabbit is not kind.
Unknown
inv-random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
@0: The cow is kind.[(triple1)] The rabbit is red.[(triple2)] @1: The rabbit sees the cow.[(((triple2) -> rule4))] @2: The cow does not need the rabbit.[(((((triple2) -> rule4)) -> rule1))] @3: The cow is green.[(((triple1 ((((triple2) -> rule4)) -> rule1)) -> rule7))]
The cow is kind.
("cow" "is" "kind" "+")
triple1
The rabbit is red.
("rabbit" "is" "red" "+")
triple2
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
((triple2) -> (rule4 % int1))
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int1
The cow does not need the rabbit.
("cow" "needs" "rabbit" "-")
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
The cow does not need the rabbit.
("cow" "needs" "rabbit" "-")
int1
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int2
The cow is green.
("cow" "is" "green" "+")
((triple1 ((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow does not need the rabbit.
("cow" "needs" "rabbit" "-")
int2
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
int3