Anne is kind. Anne is quiet. Anne is white. Gary is kind. Gary is nice. Gary is quiet. Gary is smart. Gary is white. Harry is kind. Harry is nice. Harry is quiet. Harry is rough. Harry is smart. Harry is white. Harry is young. If something is kind and young then it is nice. If Gary is quiet and Gary is smart then Gary is young. All quiet things are smart.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is white.
("Anne" "is" "white" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is kind and young then it is nice.
((("something" "is" "kind" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If Gary is quiet and Gary is smart then Gary is young.
((("Gary" "is" "quiet" "+") ("Gary" "is" "smart" "+")) -> ("Gary" "is" "young" "+"))
All quiet things are smart.
((("something" "is" "quiet" "+")) -> ("something" "is" "smart" "+"))
Gary is quiet.
True
1
proof
[(triple6)]
("Gary" "is" "quiet" "+")
triple6
Harry is not rough.
False
1
inv-proof
[(triple12)]
("Harry" "is" "rough" "-")
triple12
Gary is young.
True
3
proof
[(((triple6 triple7) -> rule2) OR ((triple6 ((triple6) -> rule3)) -> rule2))]
("Gary" "is" "young" "+")
((triple6 triple7) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((triple6 ((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not young.
False
3
inv-proof
[(((triple6 triple7) -> rule2) OR ((triple6 ((triple6) -> rule3)) -> rule2))]
("Gary" "is" "young" "-")
((triple6 triple7) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((triple6 ((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Anne is not nice.
Unknown
inv-rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "nice" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is kind.[(triple1)] Anne is quiet.[(triple2)] Anne is white.[(triple3)] Gary is kind.[(triple4)] Gary is nice.[(triple5 OR ((triple4 ((triple6 triple7) -> rule2)) -> rule1) OR ((triple4 ((triple6 ((triple6) -> rule3)) -> rule2)) -> rule1))] Gary is quiet.[(triple6)] Gary is smart.[(triple7 OR ((triple6) -> rule3))] Gary is white.[(triple8)] Harry is kind.[(triple9)] Harry is nice.[(triple10 OR ((triple9 triple15) -> rule1))] Harry is quiet.[(triple11)] Harry is rough.[(triple12)] Harry is smart.[(triple13 OR ((triple11) -> rule3))] Harry is white.[(triple14)] Harry is young.[(triple15)] @1: Anne is smart.[(((triple2) -> rule3))] Gary is young.[(((triple6 triple7) -> rule2) OR ((triple6 ((triple6) -> rule3)) -> rule2))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
triple4
Gary is nice.
("Gary" "is" "nice" "+")
triple5
((triple4 ((triple6 triple7) -> (rule2 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
((triple4 ((triple6 ((triple6) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
Gary is smart.
("Gary" "is" "smart" "+")
triple7
((triple6) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple8
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is nice.
("Harry" "is" "nice" "+")
triple10
((triple9 triple15) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is rough.
("Harry" "is" "rough" "+")
triple12
Harry is smart.
("Harry" "is" "smart" "+")
triple13
((triple11) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple14
Harry is young.
("Harry" "is" "young" "+")
triple15
Anne is smart.
("Anne" "is" "smart" "+")
((triple2) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple6 triple7) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((triple6 ((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2