Anne is blue. Bob is not furry. Charlie is blue. Dave is quiet. All white, smart things are kind. Blue things are not kind. If something is blue and not kind then it is furry.
Anne is blue.
("Anne" "is" "blue" "+")
Bob is not furry.
("Bob" "is" "furry" "-")
Charlie is blue.
("Charlie" "is" "blue" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
All white, smart things are kind.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
Blue things are not kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "-"))
If something is blue and not kind then it is furry.
((("something" "is" "blue" "+") ("something" "is" "kind" "~")) -> ("something" "is" "furry" "+"))
Charlie is blue.
True
1
proof
[(triple3)]
("Charlie" "is" "blue" "+")
triple3
Charlie is not blue.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "blue" "-")
triple3
Charlie is not kind.
True
2
proof
[(((triple3) -> rule2))]
("Charlie" "is" "kind" "-")
((triple3) -> (rule2 % int1))
Charlie is not kind.
("Charlie" "is" "kind" "-")
int1
Charlie is kind.
False
2
inv-proof
[(((triple3) -> rule2))]
("Charlie" "is" "kind" "+")
((triple3) -> (rule2 % int1))
Charlie is not kind.
("Charlie" "is" "kind" "-")
int1
Anne is furry.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule3))]
("Anne" "is" "furry" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not kind.
("Anne" "is" "kind" "-")
int2
Charlie is not furry.
False
4
inv-proof
[(((triple3 ((triple3) -> rule2)) -> rule3))]
("Charlie" "is" "furry" "-")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not kind.
("Charlie" "is" "kind" "-")
int2
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "furry" "-")
Dave is kind.
Unknown
rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "kind" "+")
Bob is not kind.
Unknown
inv-rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "kind" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Anne is blue.[(triple1)] Bob is not furry.[(triple2)] Charlie is blue.[(triple3)] Dave is quiet.[(triple4)] @1: Anne is not kind.[(((triple1) -> rule2))] Charlie is not kind.[(((triple3) -> rule2))] @2: Anne is furry.[(((triple1 ((triple1) -> rule2)) -> rule3))] Charlie is furry.[(((triple3 ((triple3) -> rule2)) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Bob is not furry.
("Bob" "is" "furry" "-")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple3
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Anne is not kind.
("Anne" "is" "kind" "-")
((triple1) -> (rule2 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Charlie is not kind.
("Charlie" "is" "kind" "-")
((triple3) -> (rule2 % int1))
Charlie is not kind.
("Charlie" "is" "kind" "-")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not kind.
("Anne" "is" "kind" "-")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple3 ((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not kind.
("Charlie" "is" "kind" "-")
int2