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