The rabbit is red. If something is big then it is young. If something is big and nice then it is young. If something is red then it is young. If something is nice then it is big. If the rabbit is red and the rabbit is young then the rabbit is nice. If something is young and round then it is nice.
The rabbit is red.
("rabbit" "is" "red" "+")
If something is big then it is young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If something is big and nice then it is young.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If something is red then it is young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If something is nice then it is big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If the rabbit is red and the rabbit is young then the rabbit is nice.
((("rabbit" "is" "red" "+") ("rabbit" "is" "young" "+")) -> ("rabbit" "is" "nice" "+"))
If something is young and round then it is nice.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
The rabbit is red.
True
1
proof
[(triple1)]
("rabbit" "is" "red" "+")
triple1
The rabbit is not red.
False
1
inv-proof
[(triple1)]
("rabbit" "is" "red" "-")
triple1
The rabbit is young.
True
2
proof
[(((triple1) -> rule3))]
("rabbit" "is" "young" "+")
((triple1) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is not young.
False
2
inv-proof
[(((triple1) -> rule3))]
("rabbit" "is" "young" "-")
((triple1) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is nice.
True
4
proof
[(((triple1 ((triple1) -> rule3)) -> rule5))]
("rabbit" "is" "nice" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit is not nice.
False
4
inv-proof
[(((triple1 ((triple1) -> rule3)) -> rule5))]
("rabbit" "is" "nice" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit does not like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
The rabbit visits the rabbit.
Unknown
random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "+")
The rabbit is not round.
Unknown
inv-random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "-")
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 red.[(triple1)] @1: The rabbit is young.[(((triple1) -> rule3))] @2: The rabbit is nice.[(((triple1 ((triple1) -> rule3)) -> rule5))] @3: The rabbit is big.[(((((triple1 ((triple1) -> rule3)) -> rule5)) -> rule4))]
The rabbit is red.
("rabbit" "is" "red" "+")
triple1
The rabbit is young.
("rabbit" "is" "young" "+")
((triple1) -> (rule3 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
int3