The rabbit is not blue. The rabbit is cold. The rabbit is kind. The rabbit is nice. The rabbit is red. All kind things are cold. All cold things are nice.
The rabbit is not blue.
("rabbit" "is" "blue" "-")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
All kind things are cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
All cold things are nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
The rabbit is nice.
True
1
proof
[(triple4 OR ((triple2) -> rule2) OR ((((triple3) -> rule1)) -> rule2))]
("rabbit" "is" "nice" "+")
triple4
((triple2) -> (rule2 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit is not cold.
False
1
inv-proof
[(triple2 OR ((triple3) -> rule1))]
("rabbit" "is" "cold" "-")
triple2
((triple3) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit does not see the rabbit.
Unknown
inv-random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "-")
The rabbit chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
@0: The rabbit is cold.[(triple2 OR ((triple3) -> rule1))] The rabbit is kind.[(triple3)] The rabbit is nice.[(triple4 OR ((triple2) -> rule2) OR ((((triple3) -> rule1)) -> rule2))] The rabbit is not blue.[(triple1)] The rabbit is red.[(triple5)]
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple2
((triple3) -> (rule1 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple3
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple4
((triple2) -> (rule2 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit is not blue.
("rabbit" "is" "blue" "-")
triple1
The rabbit is red.
("rabbit" "is" "red" "+")
triple5