The rabbit is blue. If the rabbit is big and the rabbit is red then the rabbit is round. All cold people are red. Blue people are red. If someone is blue then they are red. If someone is blue and not cold then they are not round. If someone is cold then they are round. If the rabbit is blue and the rabbit is red then the rabbit is big. Cold people are not big.
The rabbit is blue.
("rabbit" "is" "blue" "+")
If the rabbit is big and the rabbit is red then the rabbit is round.
((("rabbit" "is" "big" "+") ("rabbit" "is" "red" "+")) -> ("rabbit" "is" "round" "+"))
All cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
Blue people are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If someone is blue then they are red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "+"))
If someone is blue and not cold then they are not round.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "round" "-"))
If someone is cold then they are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If the rabbit is blue and the rabbit is red then the rabbit is big.
((("rabbit" "is" "blue" "+") ("rabbit" "is" "red" "+")) -> ("rabbit" "is" "big" "+"))
Cold people are not big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "-"))
The rabbit is blue.
True
1
proof
[(triple1)]
("rabbit" "is" "blue" "+")
triple1
The rabbit is not blue.
False
1
inv-proof
[(triple1)]
("rabbit" "is" "blue" "-")
triple1
The rabbit is red.
True
2
proof
[(((triple1) -> rule3) OR ((triple1) -> rule4))]
("rabbit" "is" "red" "+")
((triple1) -> (rule3 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
((triple1) -> (rule4 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is not red.
False
2
inv-proof
[(((triple1) -> rule3) OR ((triple1) -> rule4))]
("rabbit" "is" "red" "-")
((triple1) -> (rule3 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
((triple1) -> (rule4 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is big.
True
4
proof
[(((triple1 ((triple1) -> rule3)) -> rule7) OR ((triple1 ((triple1) -> rule4)) -> rule7))]
("rabbit" "is" "big" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
((triple1 ((triple1) -> (rule4 % int2))) -> (rule7 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit is not big.
False
4
inv-proof
[(((triple1 ((triple1) -> rule3)) -> rule7) OR ((triple1 ((triple1) -> rule4)) -> rule7))]
("rabbit" "is" "big" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
((triple1 ((triple1) -> (rule4 % int2))) -> (rule7 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit is round.
True
7
proof
[(((((triple1 ((triple1) -> rule3)) -> rule7) ((triple1) -> rule3)) -> rule1) OR ((((triple1 ((triple1) -> rule3)) -> rule7) ((triple1) -> rule4)) -> rule1) OR ((((triple1 ((triple1) -> rule4)) -> rule7) ((triple1) -> rule3)) -> rule1) OR ((((triple1 ((triple1) -> rule4)) -> rule7) ((triple1) -> rule4)) -> rule1))]
("rabbit" "is" "round" "+")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule7 % int2)) ((triple1) -> (rule3 % int3))) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule7 % int2)) ((triple1) -> (rule4 % int3))) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule7 % int2)) ((triple1) -> (rule3 % int3))) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule7 % int2)) ((triple1) -> (rule4 % int3))) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The rabbit is not round.
False
7
inv-proof
[(((((triple1 ((triple1) -> rule3)) -> rule7) ((triple1) -> rule3)) -> rule1) OR ((((triple1 ((triple1) -> rule3)) -> rule7) ((triple1) -> rule4)) -> rule1) OR ((((triple1 ((triple1) -> rule4)) -> rule7) ((triple1) -> rule3)) -> rule1) OR ((((triple1 ((triple1) -> rule4)) -> rule7) ((triple1) -> rule4)) -> rule1))]
("rabbit" "is" "round" "-")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule7 % int2)) ((triple1) -> (rule3 % int3))) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule7 % int2)) ((triple1) -> (rule4 % int3))) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule7 % int2)) ((triple1) -> (rule3 % int3))) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule7 % int2)) ((triple1) -> (rule4 % int3))) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
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 is cold.
Unknown
random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "+")
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 sees the rabbit.
Unknown
random
[@0: The rabbit sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "rabbit" "+")
@0: The rabbit is blue.[(triple1)] @1: The rabbit is red.[(((triple1) -> rule3) OR ((triple1) -> rule4))] @2: The rabbit is big.[(((triple1 ((triple1) -> rule3)) -> rule7) OR ((triple1 ((triple1) -> rule4)) -> rule7))] @3: The rabbit is round.[(((((triple1 ((triple1) -> rule3)) -> rule7) ((triple1) -> rule3)) -> rule1) OR ((((triple1 ((triple1) -> rule3)) -> rule7) ((triple1) -> rule4)) -> rule1) OR ((((triple1 ((triple1) -> rule4)) -> rule7) ((triple1) -> rule3)) -> rule1) OR ((((triple1 ((triple1) -> rule4)) -> rule7) ((triple1) -> rule4)) -> rule1))]
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple1
The rabbit is red.
("rabbit" "is" "red" "+")
((triple1) -> (rule3 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
((triple1) -> (rule4 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
((triple1 ((triple1) -> (rule4 % int2))) -> (rule7 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule7 % int2)) ((triple1) -> (rule3 % int3))) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule7 % int2)) ((triple1) -> (rule4 % int3))) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule7 % int2)) ((triple1) -> (rule3 % int3))) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule7 % int2)) ((triple1) -> (rule4 % int3))) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3