Charlie is furry. Charlie is rough. Charlie is round. If someone is furry then they are rough. If Charlie is young and Charlie is rough then Charlie is smart. Rough, round people are young. Smart people are kind. If someone is young then they are furry. If someone is kind then they are young. All young people are rough. Quiet, furry people are young.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
If someone is furry then they are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
If Charlie is young and Charlie is rough then Charlie is smart.
((("Charlie" "is" "young" "+") ("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "smart" "+"))
Rough, round people are young.
((("someone" "is" "rough" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
Smart people are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
If someone is young then they are furry.
((("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
If someone is kind then they are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
All young people are rough.
((("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
Quiet, furry people are young.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
Charlie is round.
True
1
proof
[(triple3)]
("Charlie" "is" "round" "+")
triple3
Charlie is not furry.
False
1
inv-proof
[(triple1 OR ((((triple2 triple3) -> rule3)) -> rule5))]
("Charlie" "is" "furry" "-")
triple1
((((triple2 triple3) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is young.
True
3
proof
[(((triple2 triple3) -> rule3) OR ((((triple1) -> rule1) triple3) -> rule3))]
("Charlie" "is" "young" "+")
((triple2 triple3) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple1) -> (rule1 % int2)) triple3) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not young.
False
3
inv-proof
[(((triple2 triple3) -> rule3) OR ((((triple1) -> rule1) triple3) -> rule3))]
("Charlie" "is" "young" "-")
((triple2 triple3) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple1) -> (rule1 % int2)) triple3) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is smart.
True
5
proof
[(((((triple2 triple3) -> rule3) triple2) -> rule2) OR ((((triple2 triple3) -> rule3) ((triple1) -> rule1)) -> rule2) OR ((((((triple1) -> rule1) triple3) -> rule3) triple2) -> rule2) OR ((((((triple1) -> rule1) triple3) -> rule3) ((triple1) -> rule1)) -> rule2))]
("Charlie" "is" "smart" "+")
((((triple2 triple3) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((triple2 triple3) -> (rule3 % int3)) ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
((((((triple1) -> (rule1 % int3)) triple3) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
((((((triple1) -> (rule1 % int3)) triple3) -> (rule3 % int2)) ((triple1) -> (rule1 % int3))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is not smart.
False
5
inv-proof
[(((((triple2 triple3) -> rule3) triple2) -> rule2) OR ((((triple2 triple3) -> rule3) ((triple1) -> rule1)) -> rule2) OR ((((((triple1) -> rule1) triple3) -> rule3) triple2) -> rule2) OR ((((((triple1) -> rule1) triple3) -> rule3) ((triple1) -> rule1)) -> rule2))]
("Charlie" "is" "smart" "-")
((((triple2 triple3) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((triple2 triple3) -> (rule3 % int3)) ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
((((((triple1) -> (rule1 % int3)) triple3) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
((((((triple1) -> (rule1 % int3)) triple3) -> (rule3 % int2)) ((triple1) -> (rule1 % int3))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is kind.
True
6
proof
[(((((((triple2 triple3) -> rule3) triple2) -> rule2)) -> rule4) OR ((((((triple2 triple3) -> rule3) ((triple1) -> rule1)) -> rule2)) -> rule4) OR ((((((((triple1) -> rule1) triple3) -> rule3) triple2) -> rule2)) -> rule4) OR ((((((((triple1) -> rule1) triple3) -> rule3) ((triple1) -> rule1)) -> rule2)) -> rule4))]
("Charlie" "is" "kind" "+")
((((((triple2 triple3) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
((((((triple2 triple3) -> (rule3 % int4)) ((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
((((((((triple1) -> (rule1 % int4)) triple3) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
((((((((triple1) -> (rule1 % int4)) triple3) -> (rule3 % int3)) ((triple1) -> (rule1 % int4))) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
Charlie is not kind.
False
6
inv-proof
[(((((((triple2 triple3) -> rule3) triple2) -> rule2)) -> rule4) OR ((((((triple2 triple3) -> rule3) ((triple1) -> rule1)) -> rule2)) -> rule4) OR ((((((((triple1) -> rule1) triple3) -> rule3) triple2) -> rule2)) -> rule4) OR ((((((((triple1) -> rule1) triple3) -> rule3) ((triple1) -> rule1)) -> rule2)) -> rule4))]
("Charlie" "is" "kind" "-")
((((((triple2 triple3) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
((((((triple2 triple3) -> (rule3 % int4)) ((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
((((((((triple1) -> (rule1 % int4)) triple3) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
((((((((triple1) -> (rule1 % int4)) triple3) -> (rule3 % int3)) ((triple1) -> (rule1 % int4))) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
@0: Charlie is furry.[(triple1 OR ((((triple2 triple3) -> rule3)) -> rule5))] Charlie is rough.[(triple2 OR ((triple1) -> rule1))] Charlie is round.[(triple3)] @1: Charlie is young.[(((triple2 triple3) -> rule3) OR ((((triple1) -> rule1) triple3) -> rule3))] @2: Charlie is smart.[(((((triple2 triple3) -> rule3) triple2) -> rule2) OR ((((triple2 triple3) -> rule3) ((triple1) -> rule1)) -> rule2) OR ((((((triple1) -> rule1) triple3) -> rule3) triple2) -> rule2) OR ((((((triple1) -> rule1) triple3) -> rule3) ((triple1) -> rule1)) -> rule2))] @3: Charlie is kind.[(((((((triple2 triple3) -> rule3) triple2) -> rule2)) -> rule4) OR ((((((triple2 triple3) -> rule3) ((triple1) -> rule1)) -> rule2)) -> rule4) OR ((((((((triple1) -> rule1) triple3) -> rule3) triple2) -> rule2)) -> rule4) OR ((((((((triple1) -> rule1) triple3) -> rule3) ((triple1) -> rule1)) -> rule2)) -> rule4))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
((((triple2 triple3) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
((triple1) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Charlie is young.
("Charlie" "is" "young" "+")
((triple2 triple3) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple1) -> (rule1 % int2)) triple3) -> (rule3 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple2 triple3) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
((((triple2 triple3) -> (rule3 % int3)) ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
((((((triple1) -> (rule1 % int3)) triple3) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
((((((triple1) -> (rule1 % int3)) triple3) -> (rule3 % int2)) ((triple1) -> (rule1 % int3))) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
((((((triple2 triple3) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
((((((triple2 triple3) -> (rule3 % int4)) ((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
((((((((triple1) -> (rule1 % int4)) triple3) -> (rule3 % int3)) triple2) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
((((((((triple1) -> (rule1 % int4)) triple3) -> (rule3 % int3)) ((triple1) -> (rule1 % int4))) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4