Bob is blue. Dave is young. Gary is kind. Nice, kind things are young. If something is young then it is big. Young, furry things are smart.
Bob is blue.
("Bob" "is" "blue" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Nice, kind things are young.
((("something" "is" "nice" "+") ("something" "is" "kind" "+")) -> ("something" "is" "young" "+"))
If something is young then it is big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
Young, furry things are smart.
((("something" "is" "young" "+") ("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
Dave is young.
True
1
proof
[(triple2)]
("Dave" "is" "young" "+")
triple2
Dave is not young.
False
1
inv-proof
[(triple2)]
("Dave" "is" "young" "-")
triple2
Dave is big.
True
2
proof
[(((triple2) -> rule2))]
("Dave" "is" "big" "+")
((triple2) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not big.
False
2
inv-proof
[(((triple2) -> rule2))]
("Dave" "is" "big" "-")
((triple2) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Gary is not young.
Unknown
inv-rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "young" "-")
Bob is big.
Unknown
rconc
[@2: Bob is big.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Bob" "is" "big" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Bob is blue.[(triple1)] Dave is young.[(triple2)] Gary is kind.[(triple3)] @1: Dave is big.[(((triple2) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Dave is young.
("Dave" "is" "young" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
((triple2) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1