Charlie is nice. Charlie is rough. Charlie is smart. If someone is kind then they are furry. If someone is furry and kind then they are smart. If Charlie is round then Charlie is kind. Rough, nice people are smart. If someone is cold and rough then they are smart. If Charlie is smart then Charlie is kind. All round, rough people are kind. All nice, kind people are round.
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
If someone is kind then they are furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
If someone is furry and kind then they are smart.
((("someone" "is" "furry" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "smart" "+"))
If Charlie is round then Charlie is kind.
((("Charlie" "is" "round" "+")) -> ("Charlie" "is" "kind" "+"))
Rough, nice people are smart.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If someone is cold and rough then they are smart.
((("someone" "is" "cold" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
If Charlie is smart then Charlie is kind.
((("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "kind" "+"))
All round, rough people are kind.
((("someone" "is" "round" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
All nice, kind people are round.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "round" "+"))
Charlie is rough.
True
1
proof
[(triple2)]
("Charlie" "is" "rough" "+")
triple2
Charlie is not nice.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "nice" "-")
triple1
Charlie is kind.
True
2
proof
[(((triple3) -> rule6) OR ((((triple2 triple1) -> rule4)) -> rule6))]
("Charlie" "is" "kind" "+")
((triple3) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple2 triple1) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not kind.
False
2
inv-proof
[(((triple3) -> rule6) OR ((((triple2 triple1) -> rule4)) -> rule6))]
("Charlie" "is" "kind" "-")
((triple3) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple2 triple1) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is furry.
True
3
proof
[(((((triple3) -> rule6)) -> rule1) OR ((((((triple2 triple1) -> rule4)) -> rule6)) -> rule1))]
("Charlie" "is" "furry" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((((triple2 triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is not furry.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule1) OR ((((((triple2 triple1) -> rule4)) -> rule6)) -> rule1))]
("Charlie" "is" "furry" "-")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((((triple2 triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
@0: Charlie is nice.[(triple1)] Charlie is rough.[(triple2)] Charlie is smart.[(triple3 OR ((triple2 triple1) -> rule4))] @1: Charlie is kind.[(((triple3) -> rule6) OR ((((triple2 triple1) -> rule4)) -> rule6))] @2: Charlie is furry.[(((((triple3) -> rule6)) -> rule1) OR ((((((triple2 triple1) -> rule4)) -> rule6)) -> rule1))] Charlie is round.[(((triple1 ((triple3) -> rule6)) -> rule8) OR ((triple1 ((((triple2 triple1) -> rule4)) -> rule6)) -> rule8))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
((triple2 triple1) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple3) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
((((triple2 triple1) -> (rule4 % int2))) -> (rule6 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((((((triple2 triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
((triple1 ((triple3) -> (rule6 % int2))) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
((triple1 ((((triple2 triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3