The cow chases the rabbit. The cow eats the rabbit. The cow is blue. The cow sees the rabbit. The rabbit does not eat the cow. The rabbit is cold. The rabbit sees the cow. Nice things are cold. If something is blue then it is nice.
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The rabbit does not eat the cow.
("rabbit" "eats" "cow" "-")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
Nice things are cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something is blue then it is nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
The cow eats the rabbit.
True
1
proof
[(triple2)]
("cow" "eats" "rabbit" "+")
triple2
The rabbit is not cold.
False
1
inv-proof
[(triple6)]
("rabbit" "is" "cold" "-")
triple6
The cow is nice.
True
2
proof
[(((triple3) -> rule2))]
("cow" "is" "nice" "+")
((triple3) -> (rule2 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is not nice.
False
2
inv-proof
[(((triple3) -> rule2))]
("cow" "is" "nice" "-")
((triple3) -> (rule2 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is cold.
True
3
proof
[(((((triple3) -> rule2)) -> rule1))]
("cow" "is" "cold" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The cow is not cold.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule1))]
("cow" "is" "cold" "-")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2
The rabbit is not nice.
Unknown
inv-rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "nice" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
The cow is not rough.
Unknown
inv-random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
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 rabbit sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
@0: The cow chases the rabbit.[(triple1)] The cow eats the rabbit.[(triple2)] The cow is blue.[(triple3)] The cow sees the rabbit.[(triple4)] The rabbit does not eat the cow.[(triple5)] The rabbit is cold.[(triple6)] The rabbit sees the cow.[(triple7)] @1: The cow is nice.[(((triple3) -> rule2))] @2: The cow is cold.[(((((triple3) -> rule2)) -> rule1))]
The cow chases the rabbit.
("cow" "chases" "rabbit" "+")
triple1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
triple2
The cow is blue.
("cow" "is" "blue" "+")
triple3
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple4
The rabbit does not eat the cow.
("rabbit" "eats" "cow" "-")
triple5
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple6
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple7
The cow is nice.
("cow" "is" "nice" "+")
((triple3) -> (rule2 % int1))
The cow is nice.
("cow" "is" "nice" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is nice.
("cow" "is" "nice" "+")
int2