Anne is kind. Anne is smart. Bob is big. Bob is green. Bob is kind. Bob is smart. Dave is smart. All red, smart things are quiet. All kind, green things are red.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is smart.
("Dave" "is" "smart" "+")
All red, smart things are quiet.
((("something" "is" "red" "+") ("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
All kind, green things are red.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
Dave is smart.
True
1
proof
[(triple7)]
("Dave" "is" "smart" "+")
triple7
Dave is not smart.
False
1
inv-proof
[(triple7)]
("Dave" "is" "smart" "-")
triple7
Bob is red.
True
3
proof
[(((triple5 triple4) -> rule2))]
("Bob" "is" "red" "+")
((triple5 triple4) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not red.
False
3
inv-proof
[(((triple5 triple4) -> rule2))]
("Bob" "is" "red" "-")
((triple5 triple4) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is quiet.
True
5
proof
[(((((triple5 triple4) -> rule2) triple6) -> rule1))]
("Bob" "is" "quiet" "+")
((((triple5 triple4) -> (rule2 % int2)) triple6) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not quiet.
False
5
inv-proof
[(((((triple5 triple4) -> rule2) triple6) -> rule1))]
("Bob" "is" "quiet" "-")
((((triple5 triple4) -> (rule2 % int2)) triple6) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Anne is not red.
Unknown
inv-rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "red" "-")
Anne is quiet.
Unknown
rconc
[@2: Anne is quiet.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Anne" "is" "quiet" "+")
Dave is not red.
Unknown
inv-rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "red" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
@0: Anne is kind.[(triple1)] Anne is smart.[(triple2)] Bob is big.[(triple3)] Bob is green.[(triple4)] Bob is kind.[(triple5)] Bob is smart.[(triple6)] Dave is smart.[(triple7)] @1: Bob is red.[(((triple5 triple4) -> rule2))] @2: Bob is quiet.[(((((triple5 triple4) -> rule2) triple6) -> rule1))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Bob is big.
("Bob" "is" "big" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is kind.
("Bob" "is" "kind" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Dave is smart.
("Dave" "is" "smart" "+")
triple7
Bob is red.
("Bob" "is" "red" "+")
((triple5 triple4) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple5 triple4) -> (rule2 % int2)) triple6) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2