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