Charlie is young. Dave is rough. Dave is not smart. Gary is nice. Gary is smart. Gary is young. Harry is not quiet. Harry is rough. Harry is smart. Harry is not young. Young things are furry. All rough things are not young. If something is smart and not rough then it is white. If Charlie is furry then Charlie is smart. If something is quiet then it is not nice. Furry, nice things are smart.
Charlie is young.
("Charlie" "is" "young" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is not smart.
("Dave" "is" "smart" "-")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is not quiet.
("Harry" "is" "quiet" "-")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is not young.
("Harry" "is" "young" "-")
Young things are furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
All rough things are not young.
((("something" "is" "rough" "+")) -> ("something" "is" "young" "-"))
If something is smart and not rough then it is white.
((("something" "is" "smart" "+") ("something" "is" "rough" "~")) -> ("something" "is" "white" "+"))
If Charlie is furry then Charlie is smart.
((("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "smart" "+"))
If something is quiet then it is not nice.
((("something" "is" "quiet" "+")) -> ("something" "is" "nice" "-"))
Furry, nice things are smart.
((("something" "is" "furry" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
Gary is smart.
True
1
proof
[(triple5 OR ((((triple6) -> rule1) triple4) -> rule6))]
("Gary" "is" "smart" "+")
triple5
((((triple6) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Harry is quiet.
False
1
inv-proof
[(triple7)]
("Harry" "is" "quiet" "+")
triple7
Harry is not white.
Unknown
inv-rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "white" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Charlie is young.[(triple1)] Dave is not smart.[(triple3)] Dave is rough.[(triple2)] Gary is nice.[(triple4)] Gary is smart.[(triple5 OR ((((triple6) -> rule1) triple4) -> rule6))] Gary is young.[(triple6)] Harry is not quiet.[(triple7)] Harry is not young.[(triple10 OR ((triple8) -> rule2))] Harry is rough.[(triple8)] Harry is smart.[(triple9)] @1: Charlie is furry.[(((triple1) -> rule1))] Dave is not young.[(((triple2) -> rule2))] Gary is furry.[(((triple6) -> rule1))] @2: Charlie is smart.[(((((triple1) -> rule1)) -> rule4))]
Charlie is young.
("Charlie" "is" "young" "+")
triple1
Dave is not smart.
("Dave" "is" "smart" "-")
triple3
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple4
Gary is smart.
("Gary" "is" "smart" "+")
triple5
((((triple6) -> (rule1 % int2)) triple4) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
triple6
Harry is not quiet.
("Harry" "is" "quiet" "-")
triple7
Harry is not young.
("Harry" "is" "young" "-")
triple10
((triple8) -> (rule2 % int1))
Harry is not young.
("Harry" "is" "young" "-")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple8
Harry is smart.
("Harry" "is" "smart" "+")
triple9
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Dave is not young.
("Dave" "is" "young" "-")
((triple2) -> (rule2 % int1))
Dave is not young.
("Dave" "is" "young" "-")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((triple6) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2