Anne is not blue. Anne is quiet. Charlie is blue. Charlie is nice. Charlie is quiet. Dave is white. Dave is young. If Anne is quiet and Anne is not nice then Anne is furry. If Dave is cold then Dave is white. If someone is nice then they are quiet. If someone is furry then they are quiet. Furry people are not white. If someone is cold then they are not white. If Charlie is blue then Charlie is not furry. All blue, white people are not young.
Anne is not blue.
("Anne" "is" "blue" "-")
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
If Anne is quiet and Anne is not nice then Anne is furry.
((("Anne" "is" "quiet" "+") ("Anne" "is" "nice" "~")) -> ("Anne" "is" "furry" "+"))
If Dave is cold then Dave is white.
((("Dave" "is" "cold" "+")) -> ("Dave" "is" "white" "+"))
If someone is nice then they are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
If someone is furry then they are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
Furry people are not white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "-"))
If someone is cold then they are not white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "-"))
If Charlie is blue then Charlie is not furry.
((("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "furry" "-"))
All blue, white people are not young.
((("someone" "is" "blue" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "young" "-"))
Anne is not blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Charlie is not blue.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "blue" "-")
triple3
Charlie is not furry.
True
2
proof
[(((triple3) -> rule7))]
("Charlie" "is" "furry" "-")
((triple3) -> (rule7 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is furry.
False
2
inv-proof
[(((triple3) -> rule7))]
("Charlie" "is" "furry" "+")
((triple3) -> (rule7 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "quiet" "-")
Anne is furry.
Unknown
rconc
[@1: Anne is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "furry" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
@0: Anne is not blue.[(triple1)] Anne is quiet.[(triple2)] Charlie is blue.[(triple3)] Charlie is nice.[(triple4)] Charlie is quiet.[(triple5 OR ((triple4) -> rule3))] Dave is white.[(triple6)] Dave is young.[(triple7)] @1: Charlie is not furry.[(((triple3) -> rule7))]
Anne is not blue.
("Anne" "is" "blue" "-")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
((triple4) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Charlie is not furry.
("Charlie" "is" "furry" "-")
((triple3) -> (rule7 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1