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