The rabbit is round. If the rabbit is nice then the rabbit is blue. Green people are nice. Rough people are nice. If someone is blue and not rough then they are nice. If the rabbit is not rough then the rabbit is green. All green, nice people are blue. Round people are green. Nice people are round.
The rabbit is round.
("rabbit" "is" "round" "+")
If the rabbit is nice then the rabbit is blue.
((("rabbit" "is" "nice" "+")) -> ("rabbit" "is" "blue" "+"))
Green people are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If someone is blue and not rough then they are nice.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "nice" "+"))
If the rabbit is not rough then the rabbit is green.
((("rabbit" "is" "rough" "~")) -> ("rabbit" "is" "green" "+"))
All green, nice people are blue.
((("someone" "is" "green" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
Round people are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
Nice people are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
The rabbit is round.
True
1
proof
[(triple1)]
("rabbit" "is" "round" "+")
triple1
The rabbit is not round.
False
1
inv-proof
[(triple1)]
("rabbit" "is" "round" "-")
triple1
The rabbit is green.
True
2
proof
[(((triple1) -> rule7))]
("rabbit" "is" "green" "+")
((triple1) -> (rule7 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is not green.
False
2
inv-proof
[(((triple1) -> rule7))]
("rabbit" "is" "green" "-")
((triple1) -> (rule7 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is nice.
True
3
proof
[(((((triple1) -> rule7)) -> rule2))]
("rabbit" "is" "nice" "+")
((((triple1) -> (rule7 % int2))) -> (rule2 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit is not nice.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule2))]
("rabbit" "is" "nice" "-")
((((triple1) -> (rule7 % int2))) -> (rule2 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit is not rough.
Unknown
inv-random
[@0: The rabbit is rough.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "rough" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
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" "+")
@0: The rabbit is round.[(triple1)] @1: The rabbit is green.[(((triple1) -> rule7))] @2: The rabbit is nice.[(((((triple1) -> rule7)) -> rule2))] @3: The rabbit is blue.[(((((((triple1) -> rule7)) -> rule2)) -> rule1) OR ((((triple1) -> rule7) ((((triple1) -> rule7)) -> rule2)) -> rule6))]
The rabbit is round.
("rabbit" "is" "round" "+")
triple1
The rabbit is green.
("rabbit" "is" "green" "+")
((triple1) -> (rule7 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
((((triple1) -> (rule7 % int2))) -> (rule2 % int1))
The rabbit is nice.
("rabbit" "is" "nice" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
((((((triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3
((((triple1) -> (rule7 % int3)) ((((triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit is nice.
("rabbit" "is" "nice" "+")
int2
The rabbit is green.
("rabbit" "is" "green" "+")
int3