Charlie is furry. Charlie is green. Charlie is kind. Charlie is nice. Charlie is not red. Charlie is round. Harry is furry. Harry is green. Harry is kind. Harry is nice. Harry is red. Harry is round. Red things are kind. Kind, red things are furry. All nice things are green. All green, kind things are not big. If something is furry then it is not big. If something is big and furry then it is not round. If Charlie is not kind then Charlie is not furry. All round things are nice.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is not red.
("Charlie" "is" "red" "-")
Charlie is round.
("Charlie" "is" "round" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
Kind, red things are furry.
((("something" "is" "kind" "+") ("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
All nice things are green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
All green, kind things are not big.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "big" "-"))
If something is furry then it is not big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "-"))
If something is big and furry then it is not round.
((("something" "is" "big" "+") ("something" "is" "furry" "+")) -> ("something" "is" "round" "-"))
If Charlie is not kind then Charlie is not furry.
((("Charlie" "is" "kind" "~")) -> ("Charlie" "is" "furry" "-"))
All round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
Harry is nice.
True
1
proof
[(triple10 OR ((triple12) -> rule8))]
("Harry" "is" "nice" "+")
triple10
((triple12) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not nice.
False
1
inv-proof
[(triple10 OR ((triple12) -> rule8))]
("Harry" "is" "nice" "-")
triple10
((triple12) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
@0: Charlie is furry.[(triple1)] Charlie is green.[(triple2 OR ((triple4) -> rule3) OR ((((triple6) -> rule8)) -> rule3))] Charlie is kind.[(triple3)] Charlie is nice.[(triple4 OR ((triple6) -> rule8))] Charlie is not red.[(triple5)] Charlie is round.[(triple6)] Harry is furry.[(triple7 OR ((triple9 triple11) -> rule2) OR ((((triple11) -> rule1) triple11) -> rule2))] Harry is green.[(triple8 OR ((triple10) -> rule3) OR ((((triple12) -> rule8)) -> rule3))] Harry is kind.[(triple9 OR ((triple11) -> rule1))] Harry is nice.[(triple10 OR ((triple12) -> rule8))] Harry is red.[(triple11)] Harry is round.[(triple12)] @1: Charlie is not big.[(((triple1) -> rule5) OR ((triple2 triple3) -> rule4) OR ((((triple4) -> rule3) triple3) -> rule4) OR ((((((triple6) -> rule8)) -> rule3) triple3) -> rule4))] Harry is not big.[(((triple7) -> rule5) OR ((triple8 triple9) -> rule4) OR ((((triple9 triple11) -> rule2)) -> rule5) OR ((triple8 ((triple11) -> rule1)) -> rule4) OR ((((triple10) -> rule3) triple9) -> rule4) OR ((((triple10) -> rule3) ((triple11) -> rule1)) -> rule4) OR ((((((triple11) -> rule1) triple11) -> rule2)) -> rule5) OR ((((((triple12) -> rule8)) -> rule3) triple9) -> rule4) OR ((((((triple12) -> rule8)) -> rule3) ((triple11) -> rule1)) -> rule4))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
((triple4) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((((triple6) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
((triple6) -> (rule8 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not red.
("Charlie" "is" "red" "-")
triple5
Charlie is round.
("Charlie" "is" "round" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7
((triple9 triple11) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple11) -> (rule1 % int2)) triple11) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
triple8
((triple10) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple12) -> (rule8 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
triple9
((triple11) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple10
((triple12) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple11
Harry is round.
("Harry" "is" "round" "+")
triple12
Charlie is not big.
("Charlie" "is" "big" "-")
((triple1) -> (rule5 % int1))
Charlie is not big.
("Charlie" "is" "big" "-")
int1
((triple2 triple3) -> (rule4 % int1))
Charlie is not big.
("Charlie" "is" "big" "-")
int1
((((triple4) -> (rule3 % int2)) triple3) -> (rule4 % int1))
Charlie is not big.
("Charlie" "is" "big" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((((((triple6) -> (rule8 % int3))) -> (rule3 % int2)) triple3) -> (rule4 % int1))
Charlie is not big.
("Charlie" "is" "big" "-")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Harry is not big.
("Harry" "is" "big" "-")
((triple7) -> (rule5 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
((triple8 triple9) -> (rule4 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
((((triple9 triple11) -> (rule2 % int2))) -> (rule5 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
((triple8 ((triple11) -> (rule1 % int2))) -> (rule4 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
((((triple10) -> (rule3 % int2)) triple9) -> (rule4 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple10) -> (rule3 % int3)) ((triple11) -> (rule1 % int2))) -> (rule4 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((((triple11) -> (rule1 % int3)) triple11) -> (rule2 % int2))) -> (rule5 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
int3
((((((triple12) -> (rule8 % int3))) -> (rule3 % int2)) triple9) -> (rule4 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
((((((triple12) -> (rule8 % int4))) -> (rule3 % int3)) ((triple11) -> (rule1 % int2))) -> (rule4 % int1))
Harry is not big.
("Harry" "is" "big" "-")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4