Charlie is kind. If Charlie is young and Charlie is quiet then Charlie is furry. All young things are quiet. All kind things are furry. Green things are furry. All quiet things are green. Green, quiet things are round. If Charlie is rough and Charlie is furry then Charlie is young. Kind, furry things are young.
Charlie is kind.
("Charlie" "is" "kind" "+")
If Charlie is young and Charlie is quiet then Charlie is furry.
((("Charlie" "is" "young" "+") ("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "furry" "+"))
All young things are quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
All kind things are furry.
((("something" "is" "kind" "+")) -> ("something" "is" "furry" "+"))
Green things are furry.
((("something" "is" "green" "+")) -> ("something" "is" "furry" "+"))
All quiet things are green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
Green, quiet things are round.
((("something" "is" "green" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
If Charlie is rough and Charlie is furry then Charlie is young.
((("Charlie" "is" "rough" "+") ("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "young" "+"))
Kind, furry things are young.
((("something" "is" "kind" "+") ("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
Charlie is kind.
True
1
proof
[(triple1)]
("Charlie" "is" "kind" "+")
triple1
Charlie is not kind.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "kind" "-")
triple1
Charlie is furry.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "furry" "+")
((triple1) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not furry.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "furry" "-")
((triple1) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is young.
True
4
proof
[(((triple1 ((triple1) -> rule3)) -> rule8))]
("Charlie" "is" "young" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is not young.
False
4
inv-proof
[(((triple1 ((triple1) -> rule3)) -> rule8))]
("Charlie" "is" "young" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is quiet.
True
5
proof
[(((((triple1 ((triple1) -> rule3)) -> rule8)) -> rule2))]
("Charlie" "is" "quiet" "+")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is not quiet.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule3)) -> rule8)) -> rule2))]
("Charlie" "is" "quiet" "-")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
@0: Charlie is kind.[(triple1)] @1: Charlie is furry.[(((triple1) -> rule3))] @2: Charlie is young.[(((triple1 ((triple1) -> rule3)) -> rule8))] @3: Charlie is quiet.[(((((triple1 ((triple1) -> rule3)) -> rule8)) -> rule2))] @4: Charlie is green.[(((((((triple1 ((triple1) -> rule3)) -> rule8)) -> rule2)) -> rule5))] @5: Charlie is round.[(((((((((triple1 ((triple1) -> rule3)) -> rule8)) -> rule2)) -> rule5) ((((triple1 ((triple1) -> rule3)) -> rule8)) -> rule2)) -> rule6))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule8 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
((((((triple1 ((triple1) -> (rule3 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
int4
Charlie is round.
("Charlie" "is" "round" "+")
((((((((triple1 ((triple1) -> (rule3 % int5))) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule5 % int2)) ((((triple1 ((triple1) -> (rule3 % int5))) -> (rule8 % int4))) -> (rule2 % int3))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is furry.
("Charlie" "is" "furry" "+")
int5