Dave is big. Dave is cold. Dave is kind. Dave is rough. Dave is round. Dave is white. Dave is young. All kind things are rough. If something is cold and white then it is round.
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
All kind things are rough.
((("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something is cold and white then it is round.
((("something" "is" "cold" "+") ("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
Dave is kind.
True
1
proof
[(triple3)]
("Dave" "is" "kind" "+")
triple3
Dave is not round.
False
1
inv-proof
[(triple5 OR ((triple2 triple6) -> rule2))]
("Dave" "is" "round" "-")
triple5
((triple2 triple6) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
@0: Dave is big.[(triple1)] Dave is cold.[(triple2)] Dave is kind.[(triple3)] Dave is rough.[(triple4 OR ((triple3) -> rule1))] Dave is round.[(triple5 OR ((triple2 triple6) -> rule2))] Dave is white.[(triple6)] Dave is young.[(triple7)]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is rough.
("Dave" "is" "rough" "+")
triple4
((triple3) -> (rule1 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
triple5
((triple2 triple6) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple6
Dave is young.
("Dave" "is" "young" "+")
triple7