The rabbit is rough. If the rabbit is rough then the rabbit is red. If something is blue and not rough then it is not round. If the rabbit is blue then the rabbit is round. Blue things are not big. Red, rough things are big. Red, round things are big. All red things are big. All round, red things are blue.
The rabbit is rough.
("rabbit" "is" "rough" "+")
If the rabbit is rough then the rabbit is red.
((("rabbit" "is" "rough" "+")) -> ("rabbit" "is" "red" "+"))
If something is blue and not rough then it is not round.
((("something" "is" "blue" "+") ("something" "is" "rough" "~")) -> ("something" "is" "round" "-"))
If the rabbit is blue then the rabbit is round.
((("rabbit" "is" "blue" "+")) -> ("rabbit" "is" "round" "+"))
Blue things are not big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "-"))
Red, rough things are big.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
Red, round things are big.
((("something" "is" "red" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
All red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
All round, red things are blue.
((("something" "is" "round" "+") ("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
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 red.
True
2
proof
[(((triple1) -> rule1))]
("rabbit" "is" "red" "+")
((triple1) -> (rule1 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is not red.
False
2
inv-proof
[(((triple1) -> rule1))]
("rabbit" "is" "red" "-")
((triple1) -> (rule1 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is big.
True
3
proof
[(((((triple1) -> rule1)) -> rule7) OR ((((triple1) -> rule1) triple1) -> rule5))]
("rabbit" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
((((triple1) -> (rule1 % int2)) triple1) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit is not big.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule7) OR ((((triple1) -> rule1) triple1) -> rule5))]
("rabbit" "is" "big" "-")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
((((triple1) -> (rule1 % int2)) triple1) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit is not blue.
Unknown
inv-rconc
[@2: The rabbit is blue.[CWA. Example of deepest failure = (rule8 <- rule3 <- FAIL)]]
("rabbit" "is" "blue" "-")
The rabbit is round.
Unknown
rconc
[@2: The rabbit is round.[CWA. Example of deepest failure = (rule3 <- rule8 <- FAIL)]]
("rabbit" "is" "round" "+")
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 likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
@0: The rabbit is rough.[(triple1)] @1: The rabbit is red.[(((triple1) -> rule1))] @2: The rabbit is big.[(((((triple1) -> rule1)) -> rule7) OR ((((triple1) -> rule1) triple1) -> rule5))]
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple1
The rabbit is red.
("rabbit" "is" "red" "+")
((triple1) -> (rule1 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit is big.
("rabbit" "is" "big" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
((((triple1) -> (rule1 % int2)) triple1) -> (rule5 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2