The rabbit is big. The rabbit is blue. The rabbit is green. The rabbit is nice. The rabbit is round. If the rabbit is not nice then the rabbit is big. All nice things are blue. Nice things are blue. Round things are blue. Nice, round things are big. If something is big then it is round.
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
If the rabbit is not nice then the rabbit is big.
((("rabbit" "is" "nice" "~")) -> ("rabbit" "is" "big" "+"))
All nice things are blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
Nice things are blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
Round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Nice, round things are big.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If something is big then it is round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
The rabbit is big.
True
1
proof
[(triple1 OR ((triple4 triple5) -> rule5))]
("rabbit" "is" "big" "+")
triple1
((triple4 triple5) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is not blue.
False
1
inv-proof
[(triple2 OR ((triple4) -> rule2) OR ((triple4) -> rule3) OR ((triple5) -> rule4) OR ((((triple1) -> rule6)) -> rule4))]
("rabbit" "is" "blue" "-")
triple2
((triple4) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
((triple4) -> (rule3 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
((triple5) -> (rule4 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
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 sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
@0: The rabbit is big.[(triple1 OR ((triple4 triple5) -> rule5))] The rabbit is blue.[(triple2 OR ((triple4) -> rule2) OR ((triple4) -> rule3) OR ((triple5) -> rule4) OR ((((triple1) -> rule6)) -> rule4))] The rabbit is green.[(triple3)] The rabbit is nice.[(triple4)] The rabbit is round.[(triple5 OR ((triple1) -> rule6))]
The rabbit is big.
("rabbit" "is" "big" "+")
triple1
((triple4 triple5) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple2
((triple4) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
((triple4) -> (rule3 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
((triple5) -> (rule4 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
triple3
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple4
The rabbit is round.
("rabbit" "is" "round" "+")
triple5
((triple1) -> (rule6 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1