Dave is big. Dave is furry. Dave is green. Dave is kind. Dave is quiet. Dave is not rough. Dave is round. Gary is big. Gary is furry. Gary is green. Gary is kind. Gary is quiet. Gary is rough. Gary is round. If Gary is kind then Gary is rough. Round things are furry. If something is furry and not rough then it is round. Kind things are round. Big, quiet things are round. If something is kind then it is round.
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is not rough.
("Dave" "is" "rough" "-")
Dave is round.
("Dave" "is" "round" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
If Gary is kind then Gary is rough.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "rough" "+"))
Round things are furry.
((("something" "is" "round" "+")) -> ("something" "is" "furry" "+"))
If something is furry and not rough then it is round.
((("something" "is" "furry" "+") ("something" "is" "rough" "~")) -> ("something" "is" "round" "+"))
Kind things are round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
Big, quiet things are round.
((("something" "is" "big" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
If something is kind then it is round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
Dave is round.
True
1
proof
[(triple7 OR ((triple4) -> rule4) OR ((triple4) -> rule6) OR ((triple1 triple5) -> rule5) OR ((triple2 triple6) -> rule3))]
("Dave" "is" "round" "+")
triple7
((triple4) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple4) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple1 triple5) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple2 triple6) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Gary is not rough.
False
1
inv-proof
[(triple13 OR ((triple11) -> rule1))]
("Gary" "is" "rough" "-")
triple13
((triple11) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
@0: Dave is big.[(triple1)] Dave is furry.[(triple2 OR ((triple7) -> rule2) OR ((((triple4) -> rule4)) -> rule2) OR ((((triple4) -> rule6)) -> rule2) OR ((((triple1 triple5) -> rule5)) -> rule2))] Dave is green.[(triple3)] Dave is kind.[(triple4)] Dave is not rough.[(triple6)] Dave is quiet.[(triple5)] Dave is round.[(triple7 OR ((triple4) -> rule4) OR ((triple4) -> rule6) OR ((triple1 triple5) -> rule5) OR ((triple2 triple6) -> rule3))] Gary is big.[(triple8)] Gary is furry.[(triple9 OR ((triple14) -> rule2) OR ((((triple11) -> rule4)) -> rule2) OR ((((triple11) -> rule6)) -> rule2) OR ((((triple8 triple12) -> rule5)) -> rule2))] Gary is green.[(triple10)] Gary is kind.[(triple11)] Gary is quiet.[(triple12)] Gary is rough.[(triple13 OR ((triple11) -> rule1))] Gary is round.[(triple14 OR ((triple11) -> rule4) OR ((triple11) -> rule6) OR ((triple8 triple12) -> rule5))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
((triple7) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((triple4) -> (rule6 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((triple1 triple5) -> (rule5 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
triple3
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is not rough.
("Dave" "is" "rough" "-")
triple6
Dave is quiet.
("Dave" "is" "quiet" "+")
triple5
Dave is round.
("Dave" "is" "round" "+")
triple7
((triple4) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple4) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple1 triple5) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple2 triple6) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
triple8
Gary is furry.
("Gary" "is" "furry" "+")
triple9
((triple14) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((((triple11) -> (rule4 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((triple11) -> (rule6 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((triple8 triple12) -> (rule5 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
triple10
Gary is kind.
("Gary" "is" "kind" "+")
triple11
Gary is quiet.
("Gary" "is" "quiet" "+")
triple12
Gary is rough.
("Gary" "is" "rough" "+")
triple13
((triple11) -> (rule1 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
triple14
((triple11) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple11) -> (rule6 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple8 triple12) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1