Bob is red. Gary is nice. Harry is smart. If someone is smart then they are nice. If someone is quiet and big then they are young. If Bob is nice then Bob is young.
Bob is red.
("Bob" "is" "red" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If someone is smart then they are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
If someone is quiet and big then they are young.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If Bob is nice then Bob is young.
((("Bob" "is" "nice" "+")) -> ("Bob" "is" "young" "+"))
Harry is smart.
True
1
proof
[(triple3)]
("Harry" "is" "smart" "+")
triple3
Bob is not red.
False
1
inv-proof
[(triple1)]
("Bob" "is" "red" "-")
triple1
Harry is nice.
True
2
proof
[(((triple3) -> rule1))]
("Harry" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not nice.
False
2
inv-proof
[(((triple3) -> rule1))]
("Harry" "is" "nice" "-")
((triple3) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Bob is not nice.
Unknown
inv-rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "nice" "-")
Harry is young.
Unknown
rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "young" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Bob is red.[(triple1)] Gary is nice.[(triple2)] Harry is smart.[(triple3)] @1: Harry is nice.[(((triple3) -> rule1))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Gary is nice.
("Gary" "is" "nice" "+")
triple2
Harry is smart.
("Harry" "is" "smart" "+")
triple3
Harry is nice.
("Harry" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1