Charlie is cold. Charlie is furry. Charlie is green. Charlie is not nice. Charlie is red. Charlie is not smart. Charlie is young. Dave is cold. Dave is furry. Dave is green. Dave is nice. Dave is not red. Dave is smart. Dave is young. If something is nice then it is cold. All smart things are cold. If Dave is red then Dave is furry. Nice things are green. If something is smart and not nice then it is furry. Nice, cold things are smart.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is not nice.
("Charlie" "is" "nice" "-")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is not smart.
("Charlie" "is" "smart" "-")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is not red.
("Dave" "is" "red" "-")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
If something is nice then it is cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
All smart things are cold.
((("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
If Dave is red then Dave is furry.
((("Dave" "is" "red" "+")) -> ("Dave" "is" "furry" "+"))
Nice things are green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If something is smart and not nice then it is furry.
((("something" "is" "smart" "+") ("something" "is" "nice" "~")) -> ("something" "is" "furry" "+"))
Nice, cold things are smart.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Dave is furry.
True
1
proof
[(triple9)]
("Dave" "is" "furry" "+")
triple9
Dave is red.
False
1
inv-proof
[(triple12)]
("Dave" "is" "red" "+")
triple12
@0: Charlie is cold.[(triple1)] Charlie is furry.[(triple2)] Charlie is green.[(triple3)] Charlie is not nice.[(triple4)] Charlie is not smart.[(triple6)] Charlie is red.[(triple5)] Charlie is young.[(triple7)] Dave is cold.[(triple8 OR ((triple11) -> rule1) OR ((triple13) -> rule2))] Dave is furry.[(triple9)] Dave is green.[(triple10 OR ((triple11) -> rule4))] Dave is nice.[(triple11)] Dave is not red.[(triple12)] Dave is smart.[(triple13 OR ((triple11 triple8) -> rule6) OR ((triple11 ((triple11) -> rule1)) -> rule6))] Dave is young.[(triple14)]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple4
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple6
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Charlie is young.
("Charlie" "is" "young" "+")
triple7
Dave is cold.
("Dave" "is" "cold" "+")
triple8
((triple11) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
((triple13) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple9
Dave is green.
("Dave" "is" "green" "+")
triple10
((triple11) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple11
Dave is not red.
("Dave" "is" "red" "-")
triple12
Dave is smart.
("Dave" "is" "smart" "+")
triple13
((triple11 triple8) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
((triple11 ((triple11) -> (rule1 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
triple14