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