The rabbit is young. If something is young and cold then it is blue. If the rabbit is young then the rabbit is blue. Blue things are cold. Cold, blue things are rough. If the rabbit is not rough then the rabbit is not green. Cold, blue things are green. If something is young and not blue then it is not green. If something is blue and not cold then it is green.
The rabbit is young.
("rabbit" "is" "young" "+")
If something is young and cold then it is blue.
((("something" "is" "young" "+") ("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
If the rabbit is young then the rabbit is blue.
((("rabbit" "is" "young" "+")) -> ("rabbit" "is" "blue" "+"))
Blue things are cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
Cold, blue things are rough.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If the rabbit is not rough then the rabbit is not green.
((("rabbit" "is" "rough" "~")) -> ("rabbit" "is" "green" "-"))
Cold, blue things are green.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If something is young and not blue then it is not green.
((("something" "is" "young" "+") ("something" "is" "blue" "~")) -> ("something" "is" "green" "-"))
If something is blue and not cold then it is green.
((("something" "is" "blue" "+") ("something" "is" "cold" "~")) -> ("something" "is" "green" "+"))
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 blue.
True
2
proof
[(((triple1) -> rule2))]
("rabbit" "is" "blue" "+")
((triple1) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is not blue.
False
2
inv-proof
[(((triple1) -> rule2))]
("rabbit" "is" "blue" "-")
((triple1) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is cold.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("rabbit" "is" "cold" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is not cold.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("rabbit" "is" "cold" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is green.
True
6
proof
[(((((((triple1) -> rule2)) -> rule3) ((triple1) -> rule2)) -> rule6))]
("rabbit" "is" "green" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2)) ((triple1) -> (rule2 % int3))) -> (rule6 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3
The rabbit is not rough.
False
6
inv-proof
[(((((((triple1) -> rule2)) -> rule3) ((triple1) -> rule2)) -> rule4))]
("rabbit" "is" "rough" "-")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2)) ((triple1) -> (rule2 % int3))) -> (rule4 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3
The rabbit does not eat the rabbit.
Unknown
inv-random
[@0: The rabbit eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "rabbit" "-")
The rabbit needs the rabbit.
Unknown
random
[@0: The rabbit needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "rabbit" "+")
@0: The rabbit is young.[(triple1)] @1: The rabbit is blue.[(((triple1) -> rule2))] @2: The rabbit is cold.[(((((triple1) -> rule2)) -> rule3))] @3: The rabbit is green.[(((((((triple1) -> rule2)) -> rule3) ((triple1) -> rule2)) -> rule6))] The rabbit is rough.[(((((((triple1) -> rule2)) -> rule3) ((triple1) -> rule2)) -> rule4))]
The rabbit is young.
("rabbit" "is" "young" "+")
triple1
The rabbit is blue.
("rabbit" "is" "blue" "+")
((triple1) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2)) ((triple1) -> (rule2 % int3))) -> (rule6 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3
The rabbit is rough.
("rabbit" "is" "rough" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2)) ((triple1) -> (rule2 % int3))) -> (rule4 % int1))
The rabbit is rough.
("rabbit" "is" "rough" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3