Anne is furry. Anne is not kind. Anne is red. Anne is white. Anne is young. Charlie is not kind. Charlie is not white. Gary is kind. Gary is red. Gary is white. Furry things are round. If Charlie is kind and Charlie is not big then Charlie is not young. White, red things are furry.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is not kind.
("Anne" "is" "kind" "-")
Anne is red.
("Anne" "is" "red" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is not kind.
("Charlie" "is" "kind" "-")
Charlie is not white.
("Charlie" "is" "white" "-")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is white.
("Gary" "is" "white" "+")
Furry things are round.
((("something" "is" "furry" "+")) -> ("something" "is" "round" "+"))
If Charlie is kind and Charlie is not big then Charlie is not young.
((("Charlie" "is" "kind" "+") ("Charlie" "is" "big" "~")) -> ("Charlie" "is" "young" "-"))
White, red things are furry.
((("something" "is" "white" "+") ("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
Anne is red.
True
1
proof
[(triple3)]
("Anne" "is" "red" "+")
triple3
Charlie is kind.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "kind" "+")
triple6
Anne is round.
True
2
proof
[(((triple1) -> rule1) OR ((((triple4 triple3) -> rule3)) -> rule1))]
("Anne" "is" "round" "+")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple4 triple3) -> (rule3 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not round.
False
2
inv-proof
[(((triple1) -> rule1) OR ((((triple4 triple3) -> rule3)) -> rule1))]
("Anne" "is" "round" "-")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple4 triple3) -> (rule3 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Gary is round.
True
4
proof
[(((((triple10 triple9) -> rule3)) -> rule1))]
("Gary" "is" "round" "+")
((((triple10 triple9) -> (rule3 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is not round.
False
4
inv-proof
[(((((triple10 triple9) -> rule3)) -> rule1))]
("Gary" "is" "round" "-")
((((triple10 triple9) -> (rule3 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is round.
Unknown
rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Charlie" "is" "round" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Anne is furry.[(triple1 OR ((triple4 triple3) -> rule3))] Anne is not kind.[(triple2)] Anne is red.[(triple3)] Anne is white.[(triple4)] Anne is young.[(triple5)] Charlie is not kind.[(triple6)] Charlie is not white.[(triple7)] Gary is kind.[(triple8)] Gary is red.[(triple9)] Gary is white.[(triple10)] @1: Anne is round.[(((triple1) -> rule1) OR ((((triple4 triple3) -> rule3)) -> rule1))] Gary is furry.[(((triple10 triple9) -> rule3))] @2: Gary is round.[(((((triple10 triple9) -> rule3)) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
((triple4 triple3) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not kind.
("Anne" "is" "kind" "-")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple5
Charlie is not kind.
("Charlie" "is" "kind" "-")
triple6
Charlie is not white.
("Charlie" "is" "white" "-")
triple7
Gary is kind.
("Gary" "is" "kind" "+")
triple8
Gary is red.
("Gary" "is" "red" "+")
triple9
Gary is white.
("Gary" "is" "white" "+")
triple10
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
((((triple4 triple3) -> (rule3 % int2))) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
((triple10 triple9) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((((triple10 triple9) -> (rule3 % int2))) -> (rule1 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2