Charlie is cold. Charlie is furry. Charlie is green. Charlie is not nice. Charlie is quiet. Charlie is white. Charlie is young. Erin is cold. Erin is furry. Erin is green. Erin is nice. Erin is not quiet. Erin is white. Erin is young. All cold things are young. If something is furry and not cold then it is not young. Quiet, nice things are furry. If something is nice and young then it is furry. Cold, nice things are not quiet. If something is furry and not green then it is white. If something is young and quiet then it is white. If something is cold and not furry then it is not white.
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 quiet.
("Charlie" "is" "quiet" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is not quiet.
("Erin" "is" "quiet" "-")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
All cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If something is furry and not cold then it is not young.
((("something" "is" "furry" "+") ("something" "is" "cold" "~")) -> ("something" "is" "young" "-"))
Quiet, nice things are furry.
((("something" "is" "quiet" "+") ("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
If something is nice and young then it is furry.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
Cold, nice things are not quiet.
((("something" "is" "cold" "+") ("something" "is" "nice" "+")) -> ("something" "is" "quiet" "-"))
If something is furry and not green then it is white.
((("something" "is" "furry" "+") ("something" "is" "green" "~")) -> ("something" "is" "white" "+"))
If something is young and quiet then it is white.
((("something" "is" "young" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
If something is cold and not furry then it is not white.
((("something" "is" "cold" "+") ("something" "is" "furry" "~")) -> ("something" "is" "white" "-"))
Charlie is green.
True
1
proof
[(triple3)]
("Charlie" "is" "green" "+")
triple3
Charlie is not quiet.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "quiet" "-")
triple5
@0: Charlie is cold.[(triple1)] Charlie is furry.[(triple2)] Charlie is green.[(triple3)] Charlie is not nice.[(triple4)] Charlie is quiet.[(triple5)] Charlie is white.[(triple6 OR ((triple7 triple5) -> rule7) OR ((((triple1) -> rule1) triple5) -> rule7))] Charlie is young.[(triple7 OR ((triple1) -> rule1))] Erin is cold.[(triple8)] Erin is furry.[(triple9 OR ((triple11 triple14) -> rule4) OR ((triple11 ((triple8) -> rule1)) -> rule4))] Erin is green.[(triple10)] Erin is nice.[(triple11)] Erin is not quiet.[(triple12 OR ((triple8 triple11) -> rule5))] Erin is white.[(triple13)] Erin is young.[(triple14 OR ((triple8) -> rule1))]
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 quiet.
("Charlie" "is" "quiet" "+")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
((triple7 triple5) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple1) -> (rule1 % int2)) triple5) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
triple7
((triple1) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
triple8
Erin is furry.
("Erin" "is" "furry" "+")
triple9
((triple11 triple14) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple11 ((triple8) -> (rule1 % int2))) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
triple10
Erin is nice.
("Erin" "is" "nice" "+")
triple11
Erin is not quiet.
("Erin" "is" "quiet" "-")
triple12
((triple8 triple11) -> (rule5 % int1))
Erin is not quiet.
("Erin" "is" "quiet" "-")
int1
Erin is white.
("Erin" "is" "white" "+")
triple13
Erin is young.
("Erin" "is" "young" "+")
triple14
((triple8) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1