The rabbit is young. If something is blue and young then it is not cold. All round, young things are blue. All big things are blue. All round things are young. If the rabbit is blue then the rabbit is not cold. All young things are big.
The rabbit is young.
("rabbit" "is" "young" "+")
If something is blue and young then it is not cold.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "cold" "-"))
All round, young things are blue.
((("something" "is" "round" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
All big things are blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
All round things are young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
If the rabbit is blue then the rabbit is not cold.
((("rabbit" "is" "blue" "+")) -> ("rabbit" "is" "cold" "-"))
All young things are big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
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 big.
True
2
proof
[(((triple1) -> rule6))]
("rabbit" "is" "big" "+")
((triple1) -> (rule6 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is not big.
False
2
inv-proof
[(((triple1) -> rule6))]
("rabbit" "is" "big" "-")
((triple1) -> (rule6 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is blue.
True
3
proof
[(((((triple1) -> rule6)) -> rule3))]
("rabbit" "is" "blue" "+")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is not blue.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule3))]
("rabbit" "is" "blue" "-")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is not cold.
True
4
proof
[(((((((triple1) -> rule6)) -> rule3)) -> rule5) OR ((((((triple1) -> rule6)) -> rule3) triple1) -> rule1))]
("rabbit" "is" "cold" "-")
((((((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit is not cold.
("rabbit" "is" "cold" "-")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
((((((triple1) -> (rule6 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The rabbit is not cold.
("rabbit" "is" "cold" "-")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
The rabbit is cold.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule3)) -> rule5) OR ((((((triple1) -> rule6)) -> rule3) triple1) -> rule1))]
("rabbit" "is" "cold" "+")
((((((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit is not cold.
("rabbit" "is" "cold" "-")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
((((((triple1) -> (rule6 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The rabbit is not cold.
("rabbit" "is" "cold" "-")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
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 chases the rabbit.
Unknown
random
[@0: The rabbit chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "rabbit" "+")
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 is round.
Unknown
random
[@0: The rabbit is round.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "round" "+")
@0: The rabbit is young.[(triple1)] @1: The rabbit is big.[(((triple1) -> rule6))] @2: The rabbit is blue.[(((((triple1) -> rule6)) -> rule3))] @3: The rabbit is not cold.[(((((((triple1) -> rule6)) -> rule3)) -> rule5) OR ((((((triple1) -> rule6)) -> rule3) triple1) -> rule1))]
The rabbit is young.
("rabbit" "is" "young" "+")
triple1
The rabbit is big.
("rabbit" "is" "big" "+")
((triple1) -> (rule6 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
int2
The rabbit is not cold.
("rabbit" "is" "cold" "-")
((((((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit is not cold.
("rabbit" "is" "cold" "-")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
((((((triple1) -> (rule6 % int3))) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The rabbit is not cold.
("rabbit" "is" "cold" "-")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3