Anne is red. Bob is furry. Dave is nice. Fiona is quiet. If someone is furry and blue then they are nice. If someone is nice then they are quiet. All quiet people are blue.
Anne is red.
("Anne" "is" "red" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
If someone is furry and blue then they are nice.
((("someone" "is" "furry" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice then they are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
All quiet people are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
Anne is red.
True
1
proof
[(triple1)]
("Anne" "is" "red" "+")
triple1
Dave is not nice.
False
1
inv-proof
[(triple3)]
("Dave" "is" "nice" "-")
triple3
Dave is quiet.
True
2
proof
[(((triple3) -> rule2))]
("Dave" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not quiet.
False
2
inv-proof
[(((triple3) -> rule2))]
("Dave" "is" "quiet" "-")
((triple3) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
True
3
proof
[(((((triple3) -> rule2)) -> rule3))]
("Dave" "is" "blue" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not blue.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule3))]
("Dave" "is" "blue" "-")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Bob is not nice.
Unknown
inv-rconc
[@3: Bob is nice.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule2 <- FAIL)]]
("Bob" "is" "nice" "-")
Anne is quiet.
Unknown
rconc
[@2: Anne is quiet.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Anne" "is" "quiet" "+")
Fiona is not nice.
Unknown
inv-rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "nice" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
Dave is not round.
Unknown
inv-random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
@0: Anne is red.[(triple1)] Bob is furry.[(triple2)] Dave is nice.[(triple3)] Fiona is quiet.[(triple4)] @1: Dave is quiet.[(((triple3) -> rule2))] Fiona is blue.[(((triple4) -> rule3))] @2: Dave is blue.[(((((triple3) -> rule2)) -> rule3))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple4
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple3) -> (rule2 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple4) -> (rule3 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2