Charlie is big. Charlie is cold. Charlie is furry. Charlie is red. Charlie is not rough. Charlie is smart. Charlie is white. All red, furry things are cold. If something is red then it is big. If something is smart and furry then it is red. If something is cold and furry then it is white. If something is furry then it is white. If something is rough and not big then it is white.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is not rough.
("Charlie" "is" "rough" "-")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
All red, furry things are cold.
((("something" "is" "red" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
If something is red then it is big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If something is smart and furry then it is red.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
If something is cold and furry then it is white.
((("something" "is" "cold" "+") ("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
If something is furry then it is white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
If something is rough and not big then it is white.
((("something" "is" "rough" "+") ("something" "is" "big" "~")) -> ("something" "is" "white" "+"))
Charlie is not rough.
True
1
proof
[(triple5)]
("Charlie" "is" "rough" "-")
triple5
Charlie is not big.
False
1
inv-proof
[(triple1 OR ((triple4) -> rule2) OR ((((triple6 triple3) -> rule3)) -> rule2))]
("Charlie" "is" "big" "-")
triple1
((triple4) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple6 triple3) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
@0: Charlie is big.[(triple1 OR ((triple4) -> rule2) OR ((((triple6 triple3) -> rule3)) -> rule2))] Charlie is cold.[(triple2 OR ((triple4 triple3) -> rule1) OR ((((triple6 triple3) -> rule3) triple3) -> rule1))] Charlie is furry.[(triple3)] Charlie is not rough.[(triple5)] Charlie is red.[(triple4 OR ((triple6 triple3) -> rule3))] Charlie is smart.[(triple6)] Charlie is white.[(triple7 OR ((triple3) -> rule5) OR ((triple2 triple3) -> rule4) OR ((((triple4 triple3) -> rule1) triple3) -> rule4) OR ((((((triple6 triple3) -> rule3) triple3) -> rule1) triple3) -> rule4))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple4) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple6 triple3) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
((triple4 triple3) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple6 triple3) -> (rule3 % int2)) triple3) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Charlie is not rough.
("Charlie" "is" "rough" "-")
triple5
Charlie is red.
("Charlie" "is" "red" "+")
triple4
((triple6 triple3) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Charlie is white.
("Charlie" "is" "white" "+")
triple7
((triple3) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple2 triple3) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple4 triple3) -> (rule1 % int2)) triple3) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((((triple6 triple3) -> (rule3 % int3)) triple3) -> (rule1 % int2)) triple3) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3