Bob is blue. Bob is cold. Bob is kind. Harry is big. Harry is cold. Harry is furry. Harry is quiet. If Harry is quiet and Harry is not blue then Harry is big. If someone is furry and not kind then they are big. If someone is quiet and cold then they are young.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If Harry is quiet and Harry is not blue then Harry is big.
((("Harry" "is" "quiet" "+") ("Harry" "is" "blue" "~")) -> ("Harry" "is" "big" "+"))
If someone is furry and not kind then they are big.
((("someone" "is" "furry" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "big" "+"))
If someone is quiet and cold then they are young.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
Bob is kind.
True
1
proof
[(triple3)]
("Bob" "is" "kind" "+")
triple3
Bob is not kind.
False
1
inv-proof
[(triple3)]
("Bob" "is" "kind" "-")
triple3
Harry is young.
True
3
proof
[(((triple7 triple5) -> rule3))]
("Harry" "is" "young" "+")
((triple7 triple5) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not young.
False
3
inv-proof
[(((triple7 triple5) -> rule3))]
("Harry" "is" "young" "-")
((triple7 triple5) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "big" "-")
Bob is young.
Unknown
rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "young" "+")
Harry is not kind.
Unknown
inv-random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2)] Bob is kind.[(triple3)] Harry is big.[(triple4)] Harry is cold.[(triple5)] Harry is furry.[(triple6)] Harry is quiet.[(triple7)] @1: Harry is young.[(((triple7 triple5) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
Harry is cold.
("Harry" "is" "cold" "+")
triple5
Harry is furry.
("Harry" "is" "furry" "+")
triple6
Harry is quiet.
("Harry" "is" "quiet" "+")
triple7
Harry is young.
("Harry" "is" "young" "+")
((triple7 triple5) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1