The rabbit is kind. The rabbit is round. The rabbit is young. If the rabbit is kind then the rabbit is young. Big, young people are cold. If someone is young then they are cold. All big people are not cold. If someone is round then they are young. If someone is kind and not big then they are round.
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
If the rabbit is kind then the rabbit is young.
((("rabbit" "is" "kind" "+")) -> ("rabbit" "is" "young" "+"))
Big, young people are cold.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
If someone is young then they are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
All big people are not cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "-"))
If someone is round then they are young.
((("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
If someone is kind and not big then they are round.
((("someone" "is" "kind" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "round" "+"))
The rabbit is round.
True
1
proof
[(triple2)]
("rabbit" "is" "round" "+")
triple2
The rabbit is not young.
False
1
inv-proof
[(triple3 OR ((triple1) -> rule1) OR ((triple2) -> rule5))]
("rabbit" "is" "young" "-")
triple3
((triple1) -> (rule1 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
((triple2) -> (rule5 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is cold.
True
2
proof
[(((triple3) -> rule3) OR ((((triple1) -> rule1)) -> rule3) OR ((((triple2) -> rule5)) -> rule3))]
("rabbit" "is" "cold" "+")
((triple3) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit is not cold.
False
2
inv-proof
[(((triple3) -> rule3) OR ((((triple1) -> rule1)) -> rule3) OR ((((triple2) -> rule5)) -> rule3))]
("rabbit" "is" "cold" "-")
((triple3) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
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 needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
The rabbit is not big.
Unknown
inv-random
[@0: The rabbit is big.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "big" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
@0: The rabbit is kind.[(triple1)] The rabbit is round.[(triple2)] The rabbit is young.[(triple3 OR ((triple1) -> rule1) OR ((triple2) -> rule5))] @1: The rabbit is cold.[(((triple3) -> rule3) OR ((((triple1) -> rule1)) -> rule3) OR ((((triple2) -> rule5)) -> rule3))]
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple1
The rabbit is round.
("rabbit" "is" "round" "+")
triple2
The rabbit is young.
("rabbit" "is" "young" "+")
triple3
((triple1) -> (rule1 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
((triple2) -> (rule5 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
((triple3) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2