The rabbit is big. The rabbit is blue. The rabbit is green. The rabbit is not nice. The rabbit is red. If the rabbit is green and the rabbit is not nice then the rabbit is red. If someone is big then they are red. All nice people are green. Green people are blue. If someone is red and green then they are blue. If someone is blue then they are big.
The rabbit is big.
("rabbit" "is" "big" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is not nice.
("rabbit" "is" "nice" "-")
The rabbit is red.
("rabbit" "is" "red" "+")
If the rabbit is green and the rabbit is not nice then the rabbit is red.
((("rabbit" "is" "green" "+") ("rabbit" "is" "nice" "~")) -> ("rabbit" "is" "red" "+"))
If someone is big then they are red.
((("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
All nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
Green people are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If someone is red and green then they are blue.
((("someone" "is" "red" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue then they are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
The rabbit is not nice.
True
1
proof
[(triple4)]
("rabbit" "is" "nice" "-")
triple4
The rabbit is not big.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule6) OR ((((triple3) -> rule4)) -> rule6) OR ((((triple5 triple3) -> rule5)) -> rule6) OR ((((((triple3 triple4) -> rule1) triple3) -> rule5)) -> rule6))]
("rabbit" "is" "big" "-")
triple1
((triple2) -> (rule6 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
((((triple5 triple3) -> (rule5 % int2))) -> (rule6 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
((((((triple3 triple4) -> (rule1 % int3)) triple3) -> (rule5 % int2))) -> (rule6 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The rabbit does not visit the rabbit.
Unknown
inv-random
[@0: The rabbit visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "rabbit" "-")
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 big.[(triple1 OR ((triple2) -> rule6) OR ((((triple3) -> rule4)) -> rule6) OR ((((triple5 triple3) -> rule5)) -> rule6) OR ((((((triple3 triple4) -> rule1) triple3) -> rule5)) -> rule6))] The rabbit is blue.[(triple2 OR ((triple3) -> rule4) OR ((triple5 triple3) -> rule5) OR ((((triple1) -> rule2) triple3) -> rule5) OR ((((triple3 triple4) -> rule1) triple3) -> rule5))] The rabbit is green.[(triple3)] The rabbit is not nice.[(triple4)] The rabbit is red.[(triple5 OR ((triple1) -> rule2) OR ((triple3 triple4) -> rule1) OR ((((triple2) -> rule6)) -> rule2) OR ((((((triple3) -> rule4)) -> rule6)) -> rule2))]
The rabbit is big.
("rabbit" "is" "big" "+")
triple1
((triple2) -> (rule6 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
((((triple5 triple3) -> (rule5 % int2))) -> (rule6 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
((((((triple3 triple4) -> (rule1 % int3)) triple3) -> (rule5 % int2))) -> (rule6 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple2
((triple3) -> (rule4 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
((triple5 triple3) -> (rule5 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
((((triple1) -> (rule2 % int2)) triple3) -> (rule5 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
((((triple3 triple4) -> (rule1 % int2)) triple3) -> (rule5 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
triple3
The rabbit is not nice.
("rabbit" "is" "nice" "-")
triple4
The rabbit is red.
("rabbit" "is" "red" "+")
triple5
((triple1) -> (rule2 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
((triple3 triple4) -> (rule1 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
((((((triple3) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3