Anne is not big. Anne is not furry. Anne is quiet. Anne is young. Charlie is quiet. Gary is kind. Gary is young. If Gary is quiet then Gary is kind. Young things are quiet. Furry, young things are not big. If Anne is not quiet then Anne is blue. All blue things are not furry. All blue, quiet things are kind.
Anne is not big.
("Anne" "is" "big" "-")
Anne is not furry.
("Anne" "is" "furry" "-")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is young.
("Gary" "is" "young" "+")
If Gary is quiet then Gary is kind.
((("Gary" "is" "quiet" "+")) -> ("Gary" "is" "kind" "+"))
Young things are quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
Furry, young things are not big.
((("something" "is" "furry" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "-"))
If Anne is not quiet then Anne is blue.
((("Anne" "is" "quiet" "~")) -> ("Anne" "is" "blue" "+"))
All blue things are not furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "-"))
All blue, quiet things are kind.
((("something" "is" "blue" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
Anne is not big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Anne is big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Gary is quiet.
True
2
proof
[(((triple7) -> rule2))]
("Gary" "is" "quiet" "+")
((triple7) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not quiet.
False
2
inv-proof
[(((triple7) -> rule2))]
("Gary" "is" "quiet" "-")
((triple7) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "blue" "-")
Charlie is kind.
Unknown
rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "kind" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Anne is round.
Unknown
random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "+")
@0: Anne is not big.[(triple1)] Anne is not furry.[(triple2)] Anne is quiet.[(triple3 OR ((triple4) -> rule2))] Anne is young.[(triple4)] Charlie is quiet.[(triple5)] Gary is kind.[(triple6 OR ((((triple7) -> rule2)) -> rule1))] Gary is young.[(triple7)] @1: Gary is quiet.[(((triple7) -> rule2))]
Anne is not big.
("Anne" "is" "big" "-")
triple1
Anne is not furry.
("Anne" "is" "furry" "-")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
((triple4) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
Gary is kind.
("Gary" "is" "kind" "+")
triple6
((((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
triple7
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple7) -> (rule2 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1