Anne is big. Anne is not furry. Anne is nice. All nice, green people are young. Furry, big people are young. If Anne is kind and Anne is not big then Anne is nice. If Anne is green and Anne is kind then Anne is young. If someone is nice then they are green. If someone is big and not kind then they are blue.
Anne is big.
("Anne" "is" "big" "+")
Anne is not furry.
("Anne" "is" "furry" "-")
Anne is nice.
("Anne" "is" "nice" "+")
All nice, green people are young.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "young" "+"))
Furry, big people are young.
((("someone" "is" "furry" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If Anne is kind and Anne is not big then Anne is nice.
((("Anne" "is" "kind" "+") ("Anne" "is" "big" "~")) -> ("Anne" "is" "nice" "+"))
If Anne is green and Anne is kind then Anne is young.
((("Anne" "is" "green" "+") ("Anne" "is" "kind" "+")) -> ("Anne" "is" "young" "+"))
If someone is nice then they are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If someone is big and not kind then they are blue.
((("someone" "is" "big" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "blue" "+"))
Anne is not furry.
True
1
proof
[(triple2)]
("Anne" "is" "furry" "-")
triple2
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Anne is green.
True
2
proof
[(((triple3) -> rule5))]
("Anne" "is" "green" "+")
((triple3) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not green.
False
2
inv-proof
[(((triple3) -> rule5))]
("Anne" "is" "green" "-")
((triple3) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
True
4
proof
[(((triple3 ((triple3) -> rule5)) -> rule1))]
("Anne" "is" "young" "+")
((triple3 ((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not young.
False
4
inv-proof
[(((triple3 ((triple3) -> rule5)) -> rule1))]
("Anne" "is" "young" "-")
((triple3 ((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "blue" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is big.[(triple1)] Anne is nice.[(triple3)] Anne is not furry.[(triple2)] @1: Anne is green.[(((triple3) -> rule5))] @2: Anne is young.[(((triple3 ((triple3) -> rule5)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is not furry.
("Anne" "is" "furry" "-")
triple2
Anne is green.
("Anne" "is" "green" "+")
((triple3) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple3 ((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2