Dave is cold. Dave is red. Dave is rough. Dave is round. Dave is smart. Dave is young. Gary is big. Gary is cold. Gary is red. Gary is rough. Gary is round. Gary is young. If someone is big and rough then they are smart.
Dave is cold.
("Dave" "is" "cold" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
If someone is big and rough then they are smart.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
Dave is young.
True
1
proof
[(triple6)]
("Dave" "is" "young" "+")
triple6
Dave is not rough.
False
1
inv-proof
[(triple3)]
("Dave" "is" "rough" "-")
triple3
Gary is smart.
True
3
proof
[(((triple7 triple10) -> rule1))]
("Gary" "is" "smart" "+")
((triple7 triple10) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not smart.
False
3
inv-proof
[(((triple7 triple10) -> rule1))]
("Gary" "is" "smart" "-")
((triple7 triple10) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
@0: Dave is cold.[(triple1)] Dave is red.[(triple2)] Dave is rough.[(triple3)] Dave is round.[(triple4)] Dave is smart.[(triple5)] Dave is young.[(triple6)] Gary is big.[(triple7)] Gary is cold.[(triple8)] Gary is red.[(triple9)] Gary is rough.[(triple10)] Gary is round.[(triple11)] Gary is young.[(triple12)] @1: Gary is smart.[(((triple7 triple10) -> rule1))]
Dave is cold.
("Dave" "is" "cold" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Dave is young.
("Dave" "is" "young" "+")
triple6
Gary is big.
("Gary" "is" "big" "+")
triple7
Gary is cold.
("Gary" "is" "cold" "+")
triple8
Gary is red.
("Gary" "is" "red" "+")
triple9
Gary is rough.
("Gary" "is" "rough" "+")
triple10
Gary is round.
("Gary" "is" "round" "+")
triple11
Gary is young.
("Gary" "is" "young" "+")
triple12
Gary is smart.
("Gary" "is" "smart" "+")
((triple7 triple10) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1