The rabbit is cold. The rabbit is nice. The rabbit is round. Cold, big people are round. Round, kind people are nice. Big people are kind. Cold, round people are kind. Nice, cold people are big. All nice people are round.
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
Cold, big people are round.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
Round, kind people are nice.
((("someone" "is" "round" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
Big people are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
Cold, round people are kind.
((("someone" "is" "cold" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
Nice, cold people are big.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
All nice people are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
The rabbit is cold.
True
1
proof
[(triple1)]
("rabbit" "is" "cold" "+")
triple1
The rabbit is not round.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule6) OR ((triple1 ((triple2 triple1) -> rule5)) -> rule1))]
("rabbit" "is" "round" "-")
triple3
((triple2) -> (rule6 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
((triple1 ((triple2 triple1) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is kind.
True
3
proof
[(((triple1 triple3) -> rule4) OR ((((triple2 triple1) -> rule5)) -> rule3) OR ((triple1 ((triple2) -> rule6)) -> rule4) OR ((triple1 ((triple1 ((triple2 triple1) -> rule5)) -> rule1)) -> rule4))]
("rabbit" "is" "kind" "+")
((triple1 triple3) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
((((triple2 triple1) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
((triple1 ((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
((triple1 ((triple1 ((triple2 triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
The rabbit is not kind.
False
3
inv-proof
[(((triple1 triple3) -> rule4) OR ((((triple2 triple1) -> rule5)) -> rule3) OR ((triple1 ((triple2) -> rule6)) -> rule4) OR ((triple1 ((triple1 ((triple2 triple1) -> rule5)) -> rule1)) -> rule4))]
("rabbit" "is" "kind" "-")
((triple1 triple3) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
((((triple2 triple1) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
((triple1 ((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
((triple1 ((triple1 ((triple2 triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
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 eats the rabbit.
Unknown
random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "+")
@0: The rabbit is cold.[(triple1)] The rabbit is nice.[(triple2 OR ((triple3 ((triple1 triple3) -> rule4)) -> rule2))] The rabbit is round.[(triple3 OR ((triple2) -> rule6) OR ((triple1 ((triple2 triple1) -> rule5)) -> rule1))] @1: The rabbit is big.[(((triple2 triple1) -> rule5) OR ((((triple3 ((triple1 triple3) -> rule4)) -> rule2) triple1) -> rule5))] The rabbit is kind.[(((triple1 triple3) -> rule4) OR ((((triple2 triple1) -> rule5)) -> rule3) OR ((triple1 ((triple2) -> rule6)) -> rule4) OR ((triple1 ((triple1 ((triple2 triple1) -> rule5)) -> rule1)) -> rule4))]
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple1
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple2
((triple3 ((triple1 triple3) -> (rule4 % int2))) -> (rule2 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
triple3
((triple2) -> (rule6 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
((triple1 ((triple2 triple1) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
((triple2 triple1) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
((((triple3 ((triple1 triple3) -> (rule4 % int3))) -> (rule2 % int2)) triple1) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is kind.
("rabbit" "is" "kind" "+")
int3
The rabbit is kind.
("rabbit" "is" "kind" "+")
((triple1 triple3) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
((((triple2 triple1) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
((triple1 ((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
((triple1 ((triple1 ((triple2 triple1) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The rabbit is kind.
("rabbit" "is" "kind" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3