The rabbit is cold. The rabbit is kind. The rabbit is nice. If the rabbit is rough and the rabbit is cold then the rabbit is red. If the rabbit is kind and the rabbit is cold then the rabbit is rough. Kind people are nice.
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
If the rabbit is rough and the rabbit is cold then the rabbit is red.
((("rabbit" "is" "rough" "+") ("rabbit" "is" "cold" "+")) -> ("rabbit" "is" "red" "+"))
If the rabbit is kind and the rabbit is cold then the rabbit is rough.
((("rabbit" "is" "kind" "+") ("rabbit" "is" "cold" "+")) -> ("rabbit" "is" "rough" "+"))
Kind people are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
The rabbit is cold.
True
1
proof
[(triple1)]
("rabbit" "is" "cold" "+")
triple1
The rabbit is not nice.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule3))]
("rabbit" "is" "nice" "-")
triple3
((triple2) -> (rule3 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is rough.
True
3
proof
[(((triple2 triple1) -> rule2))]
("rabbit" "is" "rough" "+")
((triple2 triple1) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is not rough.
False
3
inv-proof
[(((triple2 triple1) -> rule2))]
("rabbit" "is" "rough" "-")
((triple2 triple1) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is red.
True
5
proof
[(((((triple2 triple1) -> rule2) triple1) -> rule1))]
("rabbit" "is" "red" "+")
((((triple2 triple1) -> (rule2 % int2)) triple1) -> (rule1 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit is not red.
False
5
inv-proof
[(((((triple2 triple1) -> rule2) triple1) -> rule1))]
("rabbit" "is" "red" "-")
((((triple2 triple1) -> (rule2 % int2)) triple1) -> (rule1 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "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 rabbit is cold.[(triple1)] The rabbit is kind.[(triple2)] The rabbit is nice.[(triple3 OR ((triple2) -> rule3))] @1: The rabbit is rough.[(((triple2 triple1) -> rule2))] @2: The rabbit is red.[(((((triple2 triple1) -> rule2) triple1) -> rule1))]
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple1
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple2
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple3
((triple2) -> (rule3 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
((triple2 triple1) -> (rule2 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
((((triple2 triple1) -> (rule2 % int2)) triple1) -> (rule1 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is rough.
("rabbit" "is" "rough" "+")
int2