Anne is green. Anne is not red. Gary is furry. Gary is not nice. Harry is not cold. Harry is not furry. Harry is green. Harry is nice. Harry is not red. Harry is round. White people are not furry. All nice people are green. If someone is green then they are not white.
Anne is green.
("Anne" "is" "green" "+")
Anne is not red.
("Anne" "is" "red" "-")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is not nice.
("Gary" "is" "nice" "-")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is not furry.
("Harry" "is" "furry" "-")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is not red.
("Harry" "is" "red" "-")
Harry is round.
("Harry" "is" "round" "+")
White people are not furry.
((("someone" "is" "white" "+")) -> ("someone" "is" "furry" "-"))
All nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If someone is green then they are not white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "-"))
Anne is not red.
True
1
proof
[(triple2)]
("Anne" "is" "red" "-")
triple2
Anne is not green.
False
1
inv-proof
[(triple1)]
("Anne" "is" "green" "-")
triple1
Harry is not white.
True
2
proof
[(((triple7) -> rule3) OR ((((triple8) -> rule2)) -> rule3))]
("Harry" "is" "white" "-")
((triple7) -> (rule3 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
((((triple8) -> (rule2 % int2))) -> (rule3 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is white.
False
2
inv-proof
[(((triple7) -> rule3) OR ((((triple8) -> rule2)) -> rule3))]
("Harry" "is" "white" "+")
((triple7) -> (rule3 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
((((triple8) -> (rule2 % int2))) -> (rule3 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "green" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Anne is green.[(triple1)] Anne is not red.[(triple2)] Gary is furry.[(triple3)] Gary is not nice.[(triple4)] Harry is green.[(triple7 OR ((triple8) -> rule2))] Harry is nice.[(triple8)] Harry is not cold.[(triple5)] Harry is not furry.[(triple6)] Harry is not red.[(triple9)] Harry is round.[(triple10)] @1: Anne is not white.[(((triple1) -> rule3))] Harry is not white.[(((triple7) -> rule3) OR ((((triple8) -> rule2)) -> rule3))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is not red.
("Anne" "is" "red" "-")
triple2
Gary is furry.
("Gary" "is" "furry" "+")
triple3
Gary is not nice.
("Gary" "is" "nice" "-")
triple4
Harry is green.
("Harry" "is" "green" "+")
triple7
((triple8) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple8
Harry is not cold.
("Harry" "is" "cold" "-")
triple5
Harry is not furry.
("Harry" "is" "furry" "-")
triple6
Harry is not red.
("Harry" "is" "red" "-")
triple9
Harry is round.
("Harry" "is" "round" "+")
triple10
Anne is not white.
("Anne" "is" "white" "-")
((triple1) -> (rule3 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Harry is not white.
("Harry" "is" "white" "-")
((triple7) -> (rule3 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
((((triple8) -> (rule2 % int2))) -> (rule3 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2