The rabbit is rough. If the rabbit is cold then the rabbit is not big. If someone is cold then they are round. If someone is rough then they are cold. If the rabbit is red then the rabbit is round. Round, rough people are red. If someone is rough and not cold then they are red. If someone is rough and not red then they are not big. Red, round people are not big.
The rabbit is rough.
("rabbit" "is" "rough" "+")
If the rabbit is cold then the rabbit is not big.
((("rabbit" "is" "cold" "+")) -> ("rabbit" "is" "big" "-"))
If someone is cold then they are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If someone is rough then they are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If the rabbit is red then the rabbit is round.
((("rabbit" "is" "red" "+")) -> ("rabbit" "is" "round" "+"))
Round, rough people are red.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If someone is rough and not cold then they are red.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "red" "+"))
If someone is rough and not red then they are not big.
((("someone" "is" "rough" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "big" "-"))
Red, round people are not big.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "big" "-"))
The rabbit is rough.
True
1
proof
[(triple1)]
("rabbit" "is" "rough" "+")
triple1
The rabbit is not rough.
False
1
inv-proof
[(triple1)]
("rabbit" "is" "rough" "-")
triple1
The rabbit is cold.
True
2
proof
[(((triple1) -> rule3))]
("rabbit" "is" "cold" "+")
((triple1) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is not cold.
False
2
inv-proof
[(((triple1) -> rule3))]
("rabbit" "is" "cold" "-")
((triple1) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is round.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("rabbit" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit is not round.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("rabbit" "is" "round" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit is red.
True
5
proof
[(((((((triple1) -> rule3)) -> rule2) triple1) -> rule5))]
("rabbit" "is" "red" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) triple1) -> (rule5 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3
The rabbit is not red.
False
5
inv-proof
[(((((((triple1) -> rule3)) -> rule2) triple1) -> rule5))]
("rabbit" "is" "red" "-")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) triple1) -> (rule5 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3
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 eats the rabbit.
Unknown
random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "+")
@0: The rabbit is rough.[(triple1)] @1: The rabbit is cold.[(((triple1) -> rule3))] @2: The rabbit is not big.[(((((triple1) -> rule3)) -> rule1) OR ((((((((triple1) -> rule3)) -> rule2) triple1) -> rule5) ((((triple1) -> rule3)) -> rule2)) -> rule8))] The rabbit is round.[(((((triple1) -> rule3)) -> rule2))] @3: The rabbit is red.[(((((((triple1) -> rule3)) -> rule2) triple1) -> rule5))]
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple1
The rabbit is cold.
("rabbit" "is" "cold" "+")
((triple1) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is not big.
("rabbit" "is" "big" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The rabbit is not big.
("rabbit" "is" "big" "-")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
((((((((triple1) -> (rule3 % int4))) -> (rule2 % int3)) triple1) -> (rule5 % int2)) ((((triple1) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule8 % int1))
The rabbit is not big.
("rabbit" "is" "big" "-")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The rabbit is cold.
("rabbit" "is" "cold" "+")
int4
The rabbit is round.
("rabbit" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) triple1) -> (rule5 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is cold.
("rabbit" "is" "cold" "+")
int3