Dave is big. Dave is cold. Dave is kind. Dave is not nice. Dave is round. Dave is young. Gary is not big. Gary is not cold. Gary is furry. Gary is kind. Gary is round. Gary is young. If someone is round then they are furry. All big people are cold. If Dave is big and Dave is not nice then Dave is cold.
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is not nice.
("Dave" "is" "nice" "-")
Dave is round.
("Dave" "is" "round" "+")
Dave is young.
("Dave" "is" "young" "+")
Gary is not big.
("Gary" "is" "big" "-")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is young.
("Gary" "is" "young" "+")
If someone is round then they are furry.
((("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
All big people are cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
If Dave is big and Dave is not nice then Dave is cold.
((("Dave" "is" "big" "+") ("Dave" "is" "nice" "~")) -> ("Dave" "is" "cold" "+"))
Gary is not cold.
True
1
proof
[(triple8)]
("Gary" "is" "cold" "-")
triple8
Gary is cold.
False
1
inv-proof
[(triple8)]
("Gary" "is" "cold" "+")
triple8
Dave is furry.
True
2
proof
[(((triple5) -> rule1))]
("Dave" "is" "furry" "+")
((triple5) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not furry.
False
2
inv-proof
[(((triple5) -> rule1))]
("Dave" "is" "furry" "-")
((triple5) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
@0: Dave is big.[(triple1)] Dave is cold.[(triple2 OR ((triple1) -> rule2) OR ((triple1 triple4) -> rule3))] Dave is kind.[(triple3)] Dave is not nice.[(triple4)] Dave is round.[(triple5)] Dave is young.[(triple6)] Gary is furry.[(triple9 OR ((triple11) -> rule1))] Gary is kind.[(triple10)] Gary is not big.[(triple7)] Gary is not cold.[(triple8)] Gary is round.[(triple11)] Gary is young.[(triple12)] @1: Dave is furry.[(((triple5) -> rule1))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
((triple1) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple1 triple4) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is not nice.
("Dave" "is" "nice" "-")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
Dave is young.
("Dave" "is" "young" "+")
triple6
Gary is furry.
("Gary" "is" "furry" "+")
triple9
((triple11) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple10
Gary is not big.
("Gary" "is" "big" "-")
triple7
Gary is not cold.
("Gary" "is" "cold" "-")
triple8
Gary is round.
("Gary" "is" "round" "+")
triple11
Gary is young.
("Gary" "is" "young" "+")
triple12
Dave is furry.
("Dave" "is" "furry" "+")
((triple5) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1