Charlie is big. Charlie is blue. Charlie is cold. Charlie is furry. Charlie is nice. Charlie is red. Charlie is young. If someone is young and not blue then they are not nice. All blue people are nice. If someone is blue and red then they are cold. All furry people are cold. Cold, young people are big. If someone is big and not furry then they are young.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is young.
("Charlie" "is" "young" "+")
If someone is young and not blue then they are not nice.
((("someone" "is" "young" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "nice" "-"))
All blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If someone is blue and red then they are cold.
((("someone" "is" "blue" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
All furry people are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
Cold, young people are big.
((("someone" "is" "cold" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
If someone is big and not furry then they are young.
((("someone" "is" "big" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "young" "+"))
Charlie is nice.
True
1
proof
[(triple5 OR ((triple2) -> rule2))]
("Charlie" "is" "nice" "+")
triple5
((triple2) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not young.
False
1
inv-proof
[(triple7)]
("Charlie" "is" "young" "-")
triple7
@0: Charlie is big.[(triple1 OR ((triple3 triple7) -> rule5) OR ((((triple4) -> rule4) triple7) -> rule5) OR ((((triple2 triple6) -> rule3) triple7) -> rule5))] Charlie is blue.[(triple2)] Charlie is cold.[(triple3 OR ((triple4) -> rule4) OR ((triple2 triple6) -> rule3))] Charlie is furry.[(triple4)] Charlie is nice.[(triple5 OR ((triple2) -> rule2))] Charlie is red.[(triple6)] Charlie is young.[(triple7)]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
((triple3 triple7) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((triple4) -> (rule4 % int2)) triple7) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
((((triple2 triple6) -> (rule3 % int2)) triple7) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple3
((triple4) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple2 triple6) -> (rule3 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple4
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
((triple2) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7