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