The rabbit is nice. If something is blue and nice then it is not green. Red things are green. If something is green and nice then it is big. If something is green and nice then it is big. All nice things are big. Red, nice things are big. If the rabbit is green then the rabbit is nice. If something is big then it is blue.
The rabbit is nice.
("rabbit" "is" "nice" "+")
If something is blue and nice then it is not green.
((("something" "is" "blue" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "-"))
Red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If something is green and nice then it is big.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If something is green and nice then it is big.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
All nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Red, nice things are big.
((("something" "is" "red" "+") ("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If the rabbit is green then the rabbit is nice.
((("rabbit" "is" "green" "+")) -> ("rabbit" "is" "nice" "+"))
If something is big then it is blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
The rabbit is nice.
True
1
proof
[(triple1)]
("rabbit" "is" "nice" "+")
triple1
The rabbit is not nice.
False
1
inv-proof
[(triple1)]
("rabbit" "is" "nice" "-")
triple1
The rabbit is big.
True
2
proof
[(((triple1) -> rule5))]
("rabbit" "is" "big" "+")
((triple1) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is not big.
False
2
inv-proof
[(((triple1) -> rule5))]
("rabbit" "is" "big" "-")
((triple1) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is blue.
True
3
proof
[(((((triple1) -> rule5)) -> rule8))]
("rabbit" "is" "blue" "+")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is not blue.
False
3
inv-proof
[(((((triple1) -> rule5)) -> rule8))]
("rabbit" "is" "blue" "-")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is not green.
True
5
proof
[(((((((triple1) -> rule5)) -> rule8) triple1) -> rule1))]
("rabbit" "is" "green" "-")
((((((triple1) -> (rule5 % int3))) -> (rule8 % int2)) triple1) -> (rule1 % int1))
The rabbit is not green.
("rabbit" "is" "green" "-")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
The rabbit is green.
False
5
inv-proof
[(((((((triple1) -> rule5)) -> rule8) triple1) -> rule1))]
("rabbit" "is" "green" "+")
((((((triple1) -> (rule5 % int3))) -> (rule8 % int2)) triple1) -> (rule1 % int1))
The rabbit is not green.
("rabbit" "is" "green" "-")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
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 is red.
Unknown
random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "+")
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 nice.[(triple1)] @1: The rabbit is big.[(((triple1) -> rule5))] @2: The rabbit is blue.[(((((triple1) -> rule5)) -> rule8))] @3: The rabbit is not green.[(((((((triple1) -> rule5)) -> rule8) triple1) -> rule1))]
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple1
The rabbit is big.
("rabbit" "is" "big" "+")
((triple1) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is not green.
("rabbit" "is" "green" "-")
((((((triple1) -> (rule5 % int3))) -> (rule8 % int2)) triple1) -> (rule1 % int1))
The rabbit is not green.
("rabbit" "is" "green" "-")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3