The rabbit is blue. The rabbit is cold. The rabbit is kind. The rabbit is nice. The rabbit is red. If the rabbit is kind then the rabbit is nice. All red people are blue. All cold people are kind. If someone is blue then they are kind. Red, kind people are cold. All blue, kind people are red.
The rabbit is 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" "+")
If the rabbit is kind then the rabbit is nice.
((("rabbit" "is" "kind" "+")) -> ("rabbit" "is" "nice" "+"))
All red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
All cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If someone is blue then they are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
Red, kind people are cold.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
All blue, kind people are red.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "red" "+"))
The rabbit is kind.
True
1
proof
[(triple3 OR ((triple1) -> rule4) OR ((triple2) -> rule3) OR ((((triple5) -> rule2)) -> rule4))]
("rabbit" "is" "kind" "+")
triple3
((triple1) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
((triple2) -> (rule3 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is not kind.
False
1
inv-proof
[(triple3 OR ((triple1) -> rule4) OR ((triple2) -> rule3) OR ((((triple5) -> rule2)) -> rule4))]
("rabbit" "is" "kind" "-")
triple3
((triple1) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
((triple2) -> (rule3 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit does not eat the rabbit.
Unknown
inv-random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
@0: The rabbit is blue.[(triple1 OR ((triple5) -> rule2))] The rabbit is cold.[(triple2 OR ((triple5 triple3) -> rule5) OR ((triple5 ((triple1) -> rule4)) -> rule5) OR ((((triple1 triple3) -> rule6) triple3) -> rule5) OR ((((triple1 triple3) -> rule6) ((triple1) -> rule4)) -> rule5) OR ((triple5 ((((triple5) -> rule2)) -> rule4)) -> rule5) OR ((((triple1 ((triple1) -> rule4)) -> rule6) triple3) -> rule5) OR ((((triple1 triple3) -> rule6) ((((triple5) -> rule2)) -> rule4)) -> rule5) OR ((((triple1 ((triple1) -> rule4)) -> rule6) ((triple1) -> rule4)) -> rule5) OR ((((triple1 ((triple1) -> rule4)) -> rule6) ((((triple5) -> rule2)) -> rule4)) -> rule5))] The rabbit is kind.[(triple3 OR ((triple1) -> rule4) OR ((triple2) -> rule3) OR ((((triple5) -> rule2)) -> rule4))] The rabbit is nice.[(triple4 OR ((triple3) -> rule1) OR ((((triple1) -> rule4)) -> rule1) OR ((((triple2) -> rule3)) -> rule1) OR ((((((triple5) -> rule2)) -> rule4)) -> rule1))] The rabbit is red.[(triple5 OR ((triple1 triple3) -> rule6) OR ((triple1 ((triple1) -> rule4)) -> rule6) OR ((triple1 ((triple2) -> rule3)) -> rule6))]
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple1
((triple5) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple2
((triple5 triple3) -> (rule5 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
((triple5 ((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
((((triple1 triple3) -> (rule6 % int2)) triple3) -> (rule5 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
((((triple1 triple3) -> (rule6 % int3)) ((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
((triple5 ((((triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule6 % int2)) triple3) -> (rule5 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit is kind.
("rabbit" "is" "kind" "+")
int3
((((triple1 triple3) -> (rule6 % int4)) ((((triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3
The rabbit is red.
("rabbit" "is" "red" "+")
int4
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule6 % int2)) ((triple1) -> (rule4 % int3))) -> (rule5 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit is kind.
("rabbit" "is" "kind" "+")
int3
((((triple1 ((triple1) -> (rule4 % int4))) -> (rule6 % int3)) ((((triple5) -> (rule2 % int2))) -> (rule4 % int4))) -> (rule5 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The rabbit is kind.
("rabbit" "is" "kind" "+")
int4
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple3
((triple1) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
((triple2) -> (rule3 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple4
((triple3) -> (rule1 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
((((((triple5) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3
The rabbit is red.
("rabbit" "is" "red" "+")
triple5
((triple1 triple3) -> (rule6 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
((triple1 ((triple1) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
((triple1 ((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2