The cow is not nice. The rabbit is kind. If someone is kind then they visit the cow. If someone visits the cow then they are young. If the rabbit is young then the rabbit eats the cow. If the rabbit eats the cow and the rabbit is not nice then the cow is not young. If someone eats the cow then they chase the cow. If the rabbit visits the cow and the rabbit does not eat the cow then the cow does not visit the rabbit.
The cow is not nice.
("cow" "is" "nice" "-")
The rabbit is kind.
("rabbit" "is" "kind" "+")
If someone is kind then they visit the cow.
((("someone" "is" "kind" "+")) -> ("someone" "visits" "cow" "+"))
If someone visits the cow then they are young.
((("someone" "visits" "cow" "+")) -> ("someone" "is" "young" "+"))
If the rabbit is young then the rabbit eats the cow.
((("rabbit" "is" "young" "+")) -> ("rabbit" "eats" "cow" "+"))
If the rabbit eats the cow and the rabbit is not nice then the cow is not young.
((("rabbit" "eats" "cow" "+") ("rabbit" "is" "nice" "~")) -> ("cow" "is" "young" "-"))
If someone eats the cow then they chase the cow.
((("someone" "eats" "cow" "+")) -> ("someone" "chases" "cow" "+"))
If the rabbit visits the cow and the rabbit does not eat the cow then the cow does not visit the rabbit.
((("rabbit" "visits" "cow" "+") ("rabbit" "eats" "cow" "~")) -> ("cow" "visits" "rabbit" "-"))
The rabbit is kind.
True
1
proof
[(triple2)]
("rabbit" "is" "kind" "+")
triple2
The cow is nice.
False
1
inv-proof
[(triple1)]
("cow" "is" "nice" "+")
triple1
The rabbit visits the cow.
True
2
proof
[(((triple2) -> rule1))]
("rabbit" "visits" "cow" "+")
((triple2) -> (rule1 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The rabbit does not visit the cow.
False
2
inv-proof
[(((triple2) -> rule1))]
("rabbit" "visits" "cow" "-")
((triple2) -> (rule1 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The rabbit is young.
True
3
proof
[(((((triple2) -> rule1)) -> rule2))]
("rabbit" "is" "young" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int2
The rabbit is not young.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2))]
("rabbit" "is" "young" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int2
The rabbit eats the cow.
True
4
proof
[(((((((triple2) -> rule1)) -> rule2)) -> rule3))]
("rabbit" "eats" "cow" "+")
((((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int3
The rabbit does not eat the cow.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule2)) -> rule3))]
("rabbit" "eats" "cow" "-")
((((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int3
The cow is not young.
Unknown
inv-rconc
[@2: The cow is young.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("cow" "is" "young" "-")
The cow visits the cow.
Unknown
rconc
[@1: The cow visits the cow.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "visits" "cow" "+")
The cow does not chase the cow.
Unknown
inv-rconc
[@1: The cow chases the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "chases" "cow" "-")
The cow is kind.
Unknown
random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "+")
The rabbit is not red.
Unknown
inv-random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "-")
The cow visits the rabbit.
Unknown
random
[@0: The cow visits the rabbit.[CWA. Example of deepest failure = (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 eats the rabbit.
Unknown
random
[@0: The cow eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "rabbit" "+")
@0: The cow is not nice.[(triple1)] The rabbit is kind.[(triple2)] @1: The rabbit visits the cow.[(((triple2) -> rule1))] @2: The rabbit is young.[(((((triple2) -> rule1)) -> rule2))] @3: The rabbit eats the cow.[(((((((triple2) -> rule1)) -> rule2)) -> rule3))] @4: The rabbit chases the cow.[(((((((((triple2) -> rule1)) -> rule2)) -> rule3)) -> rule5))]
The cow is not nice.
("cow" "is" "nice" "-")
triple1
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple2
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
((triple2) -> (rule1 % int1))
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int2
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
((((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int3
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
((((((((triple2) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The rabbit eats the cow.
("rabbit" "eats" "cow" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
int3
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
int4