Gary is young. Harry is nice. All big, green things are nice. If Gary is big and Gary is green then Gary is blue. If something is young then it is nice. All round things are big. All round things are big. If something is blue and kind then it is big.
Gary is young.
("Gary" "is" "young" "+")
Harry is nice.
("Harry" "is" "nice" "+")
All big, green things are nice.
((("something" "is" "big" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If Gary is big and Gary is green then Gary is blue.
((("Gary" "is" "big" "+") ("Gary" "is" "green" "+")) -> ("Gary" "is" "blue" "+"))
If something is young then it is nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
All round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
All round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
If something is blue and kind then it is big.
((("something" "is" "blue" "+") ("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
Harry is nice.
True
1
proof
[(triple2)]
("Harry" "is" "nice" "+")
triple2
Gary is not young.
False
1
inv-proof
[(triple1)]
("Gary" "is" "young" "-")
triple1
Gary is nice.
True
2
proof
[(((triple1) -> rule3))]
("Gary" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not nice.
False
2
inv-proof
[(((triple1) -> rule3))]
("Gary" "is" "nice" "-")
((triple1) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "blue" "-")
Gary is big.
Unknown
rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "big" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Gary is young.[(triple1)] Harry is nice.[(triple2)] @1: Gary is nice.[(((triple1) -> rule3))]
Gary is young.
("Gary" "is" "young" "+")
triple1
Harry is nice.
("Harry" "is" "nice" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1