The rabbit is blue. The rabbit is nice. The rabbit is red. The rabbit is round. The rabbit is young. If something is young and blue then it is nice. If something is nice and young then it is round. If the rabbit is round then the rabbit is nice. If the rabbit is red and the rabbit is blue then the rabbit is round. If the rabbit is young then the rabbit is nice. If the rabbit is blue and the rabbit is round then the rabbit is young.
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit is red.
("rabbit" "is" "red" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
If something is young and blue then it is nice.
((("something" "is" "young" "+") ("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
If something is nice and young then it is round.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
If the rabbit is round then the rabbit is nice.
((("rabbit" "is" "round" "+")) -> ("rabbit" "is" "nice" "+"))
If the rabbit is red and the rabbit is blue then the rabbit is round.
((("rabbit" "is" "red" "+") ("rabbit" "is" "blue" "+")) -> ("rabbit" "is" "round" "+"))
If the rabbit is young then the rabbit is nice.
((("rabbit" "is" "young" "+")) -> ("rabbit" "is" "nice" "+"))
If the rabbit is blue and the rabbit is round then the rabbit is young.
((("rabbit" "is" "blue" "+") ("rabbit" "is" "round" "+")) -> ("rabbit" "is" "young" "+"))
The rabbit is round.
True
1
proof
[(triple4 OR ((triple2 triple5) -> rule2) OR ((triple3 triple1) -> rule4) OR ((((triple5) -> rule5) triple5) -> rule2) OR ((((triple5 triple1) -> rule1) triple5) -> rule2))]
("rabbit" "is" "round" "+")
triple4
((triple2 triple5) -> (rule2 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
((triple3 triple1) -> (rule4 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
((((triple5) -> (rule5 % int2)) triple5) -> (rule2 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
((((triple5 triple1) -> (rule1 % int2)) triple5) -> (rule2 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is not red.
False
1
inv-proof
[(triple3)]
("rabbit" "is" "red" "-")
triple3
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" "+")
@0: The rabbit is blue.[(triple1)] The rabbit is nice.[(triple2 OR ((triple4) -> rule3) OR ((triple5) -> rule5) OR ((triple5 triple1) -> rule1) OR ((((triple1 triple4) -> rule6)) -> rule5) OR ((((triple3 triple1) -> rule4)) -> rule3) OR ((((triple1 triple4) -> rule6) triple1) -> rule1) OR ((((triple1 ((triple3 triple1) -> rule4)) -> rule6)) -> rule5) OR ((((triple1 ((triple3 triple1) -> rule4)) -> rule6) triple1) -> rule1))] The rabbit is red.[(triple3)] The rabbit is round.[(triple4 OR ((triple2 triple5) -> rule2) OR ((triple3 triple1) -> rule4) OR ((((triple5) -> rule5) triple5) -> rule2) OR ((((triple5 triple1) -> rule1) triple5) -> rule2))] The rabbit is young.[(triple5 OR ((triple1 triple4) -> rule6) OR ((triple1 ((triple3 triple1) -> rule4)) -> rule6))]
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple1
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple2
((triple4) -> (rule3 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
((triple5) -> (rule5 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
((triple5 triple1) -> (rule1 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
((((triple1 triple4) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
((((triple3 triple1) -> (rule4 % int2))) -> (rule3 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
((((triple1 triple4) -> (rule6 % int2)) triple1) -> (rule1 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
((((triple1 ((triple3 triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
((((triple1 ((triple3 triple1) -> (rule4 % int3))) -> (rule6 % int2)) triple1) -> (rule1 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is young.
("rabbit" "is" "young" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The rabbit is red.
("rabbit" "is" "red" "+")
triple3
The rabbit is round.
("rabbit" "is" "round" "+")
triple4
((triple2 triple5) -> (rule2 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
((triple3 triple1) -> (rule4 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
((((triple5) -> (rule5 % int2)) triple5) -> (rule2 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
((((triple5 triple1) -> (rule1 % int2)) triple5) -> (rule2 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is young.
("rabbit" "is" "young" "+")
triple5
((triple1 triple4) -> (rule6 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
((triple1 ((triple3 triple1) -> (rule4 % int2))) -> (rule6 % int1))
The rabbit is young.
("rabbit" "is" "young" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2