Dave is not big. Dave is kind. Dave is quiet. Dave is rough. Dave is round. Dave is smart. Dave is young. Harry is kind. Harry is rough. Harry is round. Harry is smart. Harry is young. All smart things are not big.
Dave is not big.
("Dave" "is" "big" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
All smart things are not big.
((("something" "is" "smart" "+")) -> ("something" "is" "big" "-"))
Harry is smart.
True
1
proof
[(triple11)]
("Harry" "is" "smart" "+")
triple11
Harry is not rough.
False
1
inv-proof
[(triple9)]
("Harry" "is" "rough" "-")
triple9
Harry is not big.
True
2
proof
[(((triple11) -> rule1))]
("Harry" "is" "big" "-")
((triple11) -> (rule1 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is big.
False
2
inv-proof
[(((triple11) -> rule1))]
("Harry" "is" "big" "+")
((triple11) -> (rule1 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
@0: Dave is kind.[(triple2)] Dave is not big.[(triple1 OR ((triple6) -> rule1))] Dave is quiet.[(triple3)] Dave is rough.[(triple4)] Dave is round.[(triple5)] Dave is smart.[(triple6)] Dave is young.[(triple7)] Harry is kind.[(triple8)] Harry is rough.[(triple9)] Harry is round.[(triple10)] Harry is smart.[(triple11)] Harry is young.[(triple12)] @1: Harry is not big.[(((triple11) -> rule1))]
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is not big.
("Dave" "is" "big" "-")
triple1
((triple6) -> (rule1 % int1))
Dave is not big.
("Dave" "is" "big" "-")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple3
Dave is rough.
("Dave" "is" "rough" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7
Harry is kind.
("Harry" "is" "kind" "+")
triple8
Harry is rough.
("Harry" "is" "rough" "+")
triple9
Harry is round.
("Harry" "is" "round" "+")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
Harry is not big.
("Harry" "is" "big" "-")
((triple11) -> (rule1 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1