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