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