Gary is furry. Harry is nice. Harry is smart. All nice, young things are rough. All smart things are young. If something is nice then it is smart.
Gary is furry.
("Gary" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All nice, young things are rough.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
All smart things are young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
If something is nice then it is smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
Harry is smart.
True
1
proof
[(triple3 OR ((triple2) -> rule3))]
("Harry" "is" "smart" "+")
triple3
((triple2) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Gary is not furry.
False
1
inv-proof
[(triple1)]
("Gary" "is" "furry" "-")
triple1
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "smart" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Gary is furry.[(triple1)] Harry is nice.[(triple2)] Harry is smart.[(triple3 OR ((triple2) -> rule3))] @1: Harry is young.[(((triple3) -> rule2) OR ((((triple2) -> rule3)) -> rule2))] @2: Harry is rough.[(((triple2 ((triple3) -> rule2)) -> rule1) OR ((triple2 ((((triple2) -> rule3)) -> rule2)) -> rule1))]
Gary is furry.
("Gary" "is" "furry" "+")
triple1
Harry is nice.
("Harry" "is" "nice" "+")
triple2
Harry is smart.
("Harry" "is" "smart" "+")
triple3
((triple2) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((triple3) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((triple2 ((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((triple2 ((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3