Anne is blue. Anne is quiet. Bob is quiet. Bob is not white. Bob is young. Dave is blue. Fiona is not nice. If Anne is white then Anne is not quiet. If something is quiet then it is blue.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is not white.
("Bob" "is" "white" "-")
Bob is young.
("Bob" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Fiona is not nice.
("Fiona" "is" "nice" "-")
If Anne is white then Anne is not quiet.
((("Anne" "is" "white" "+")) -> ("Anne" "is" "quiet" "-"))
If something is quiet then it is blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
Anne is blue.
True
1
proof
[(triple1 OR ((triple2) -> rule2))]
("Anne" "is" "blue" "+")
triple1
((triple2) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Bob is white.
False
1
inv-proof
[(triple4)]
("Bob" "is" "white" "+")
triple4
Fiona is not blue.
Unknown
inv-rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "blue" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is blue.[(triple1 OR ((triple2) -> rule2))] Anne is quiet.[(triple2)] Bob is not white.[(triple4)] Bob is quiet.[(triple3)] Bob is young.[(triple5)] Dave is blue.[(triple6)] Fiona is not nice.[(triple7)] @1: Bob is blue.[(((triple3) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((triple2) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Bob is not white.
("Bob" "is" "white" "-")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple5
Dave is blue.
("Dave" "is" "blue" "+")
triple6
Fiona is not nice.
("Fiona" "is" "nice" "-")
triple7
Bob is blue.
("Bob" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1