Charlie is not cold. Charlie is furry. Charlie is green. Charlie is kind. Charlie is nice. Charlie is not round. Charlie is smart. Dave is not furry. Dave is green. Dave is kind. Dave is round. Dave is not smart. If something is cold and nice then it is not furry. If something is round and nice then it is furry. If Dave is nice then Dave is cold. If something is cold and not round then it is not nice. Kind things are not cold. Round, nice things are cold.
Charlie is not cold.
("Charlie" "is" "cold" "-")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is not round.
("Charlie" "is" "round" "-")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is not smart.
("Dave" "is" "smart" "-")
If something is cold and nice then it is not furry.
((("something" "is" "cold" "+") ("something" "is" "nice" "+")) -> ("something" "is" "furry" "-"))
If something is round and nice then it is furry.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
If Dave is nice then Dave is cold.
((("Dave" "is" "nice" "+")) -> ("Dave" "is" "cold" "+"))
If something is cold and not round then it is not nice.
((("something" "is" "cold" "+") ("something" "is" "round" "~")) -> ("something" "is" "nice" "-"))
Kind things are not cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "-"))
Round, nice things are cold.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
Charlie is green.
True
1
proof
[(triple3)]
("Charlie" "is" "green" "+")
triple3
Dave is smart.
False
1
inv-proof
[(triple12)]
("Dave" "is" "smart" "+")
triple12
Dave is not cold.
True
2
proof
[(((triple10) -> rule5))]
("Dave" "is" "cold" "-")
((triple10) -> (rule5 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
Dave is cold.
False
2
inv-proof
[(((triple10) -> rule5))]
("Dave" "is" "cold" "+")
((triple10) -> (rule5 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1
@0: Charlie is furry.[(triple2)] Charlie is green.[(triple3)] Charlie is kind.[(triple4)] Charlie is nice.[(triple5)] Charlie is not cold.[(triple1 OR ((triple4) -> rule5))] Charlie is not round.[(triple6)] Charlie is smart.[(triple7)] Dave is green.[(triple9)] Dave is kind.[(triple10)] Dave is not furry.[(triple8)] Dave is not smart.[(triple12)] Dave is round.[(triple11)] @1: Dave is not cold.[(((triple10) -> rule5))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple1
((triple4) -> (rule5 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is not round.
("Charlie" "is" "round" "-")
triple6
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7
Dave is green.
("Dave" "is" "green" "+")
triple9
Dave is kind.
("Dave" "is" "kind" "+")
triple10
Dave is not furry.
("Dave" "is" "furry" "-")
triple8
Dave is not smart.
("Dave" "is" "smart" "-")
triple12
Dave is round.
("Dave" "is" "round" "+")
triple11
Dave is not cold.
("Dave" "is" "cold" "-")
((triple10) -> (rule5 % int1))
Dave is not cold.
("Dave" "is" "cold" "-")
int1