Charlie is cold. Charlie is not furry. Charlie is not green. Charlie is kind. Charlie is not rough. Charlie is white. Charlie is young. Harry is cold. Harry is furry. Harry is green. Harry is kind. Harry is rough. Harry is white. Harry is young. If someone is cold and not green then they are kind. If someone is cold and not rough then they are white. Young, cold people are white. If someone is rough then they are white. If someone is kind then they are young. If someone is young and white then they are cold.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Charlie is not green.
("Charlie" "is" "green" "-")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is not rough.
("Charlie" "is" "rough" "-")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is cold and not green then they are kind.
((("someone" "is" "cold" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "kind" "+"))
If someone is cold and not rough then they are white.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "white" "+"))
Young, cold people are white.
((("someone" "is" "young" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
If someone is rough then they are white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
If someone is kind then they are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
If someone is young and white then they are cold.
((("someone" "is" "young" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
Harry is cold.
True
1
proof
[(triple8 OR ((triple14 triple13) -> rule6) OR ((triple14 ((triple12) -> rule4)) -> rule6) OR ((((triple11) -> rule5) triple13) -> rule6) OR ((((triple11) -> rule5) ((triple12) -> rule4)) -> rule6))]
("Harry" "is" "cold" "+")
triple8
((triple14 triple13) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple14 ((triple12) -> (rule4 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple11) -> (rule5 % int2)) triple13) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple11) -> (rule5 % int3)) ((triple12) -> (rule4 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is not rough.
False
1
inv-proof
[(triple12)]
("Harry" "is" "rough" "-")
triple12
@0: Charlie is cold.[(triple1 OR ((triple7 triple6) -> rule6) OR ((((triple4) -> rule5) triple6) -> rule6))] Charlie is kind.[(triple4 OR ((triple1 triple3) -> rule1) OR ((((triple7 triple6) -> rule6) triple3) -> rule1))] Charlie is not furry.[(triple2)] Charlie is not green.[(triple3)] Charlie is not rough.[(triple5)] Charlie is white.[(triple6 OR ((triple1 triple5) -> rule2) OR ((triple7 triple1) -> rule3) OR ((((triple4) -> rule5) triple1) -> rule3) OR ((((((triple1 triple3) -> rule1)) -> rule5) triple1) -> rule3))] Charlie is young.[(triple7 OR ((triple4) -> rule5) OR ((((triple1 triple3) -> rule1)) -> rule5))] Harry is cold.[(triple8 OR ((triple14 triple13) -> rule6) OR ((triple14 ((triple12) -> rule4)) -> rule6) OR ((((triple11) -> rule5) triple13) -> rule6) OR ((((triple11) -> rule5) ((triple12) -> rule4)) -> rule6))] Harry is furry.[(triple9)] Harry is green.[(triple10)] Harry is kind.[(triple11)] Harry is rough.[(triple12)] Harry is white.[(triple13 OR ((triple12) -> rule4) OR ((triple14 triple8) -> rule3) OR ((((triple11) -> rule5) triple8) -> rule3))] Harry is young.[(triple14 OR ((triple11) -> rule5))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
((triple7 triple6) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple4) -> (rule5 % int2)) triple6) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
((triple1 triple3) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple7 triple6) -> (rule6 % int2)) triple3) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple2
Charlie is not green.
("Charlie" "is" "green" "-")
triple3
Charlie is not rough.
("Charlie" "is" "rough" "-")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
((triple1 triple5) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple7 triple1) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple4) -> (rule5 % int2)) triple1) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((((triple1 triple3) -> (rule1 % int3))) -> (rule5 % int2)) triple1) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
triple7
((triple4) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple1 triple3) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
triple8
((triple14 triple13) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((triple14 ((triple12) -> (rule4 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple11) -> (rule5 % int2)) triple13) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((triple11) -> (rule5 % int3)) ((triple12) -> (rule4 % int2))) -> (rule6 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
triple9
Harry is green.
("Harry" "is" "green" "+")
triple10
Harry is kind.
("Harry" "is" "kind" "+")
triple11
Harry is rough.
("Harry" "is" "rough" "+")
triple12
Harry is white.
("Harry" "is" "white" "+")
triple13
((triple12) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple14 triple8) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple11) -> (rule5 % int2)) triple8) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
triple14
((triple11) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1