The rabbit is young. All young things are round. If the rabbit is round and the rabbit is cold then the rabbit is not nice. Round things are cold. If something is round and nice then it is cold. If something is nice and not round then it is cold. If the rabbit is not nice and the rabbit is not young then the rabbit is not red.
The rabbit is young.
("rabbit" "is" "young" "+")
All young things are round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
If the rabbit is round and the rabbit is cold then the rabbit is not nice.
((("rabbit" "is" "round" "+") ("rabbit" "is" "cold" "+")) -> ("rabbit" "is" "nice" "-"))
Round things are cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "+"))
If something is round and nice then it is cold.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something is nice and not round then it is cold.
((("something" "is" "nice" "+") ("something" "is" "round" "~")) -> ("something" "is" "cold" "+"))
If the rabbit is not nice and the rabbit is not young then the rabbit is not red.
((("rabbit" "is" "nice" "~") ("rabbit" "is" "young" "~")) -> ("rabbit" "is" "red" "-"))
The rabbit is young.
True
1
proof
[(triple1)]
("rabbit" "is" "young" "+")
triple1
The rabbit is not young.
False
1
inv-proof
[(triple1)]
("rabbit" "is" "young" "-")
triple1
The rabbit is round.
True
2
proof
[(((triple1) -> rule1))]
("rabbit" "is" "round" "+")
((triple1) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is not round.
False
2
inv-proof
[(((triple1) -> rule1))]
("rabbit" "is" "round" "-")
((triple1) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is cold.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("rabbit" "is" "cold" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is not cold.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("rabbit" "is" "cold" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is not nice.
True
6
proof
[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule3)) -> rule2))]
("rabbit" "is" "nice" "-")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit is not nice.
("rabbit" "is" "nice" "-")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The rabbit is nice.
False
6
inv-proof
[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule3)) -> rule2))]
("rabbit" "is" "nice" "+")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit is not nice.
("rabbit" "is" "nice" "-")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
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 eats the rabbit.
Unknown
random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "+")
The rabbit is not red.
Unknown
inv-random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "-")
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 young.[(triple1)] @1: The rabbit is round.[(((triple1) -> rule1))] @2: The rabbit is cold.[(((((triple1) -> rule1)) -> rule3))] @3: The rabbit is not nice.[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule3)) -> rule2))]
The rabbit is young.
("rabbit" "is" "young" "+")
triple1
The rabbit is round.
("rabbit" "is" "round" "+")
((triple1) -> (rule1 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is not nice.
("rabbit" "is" "nice" "-")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The rabbit is not nice.
("rabbit" "is" "nice" "-")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3