Charlie is blue. If something is blue and smart then it is quiet. Blue things are big. If something is big then it is quiet. All quiet, furry things are big. If something is quiet then it is furry. All quiet things are round. All blue, big things are quiet. If Charlie is blue and Charlie is big then Charlie is green.
Charlie is blue.
("Charlie" "is" "blue" "+")
If something is blue and smart then it is quiet.
((("something" "is" "blue" "+") ("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
Blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If something is big then it is quiet.
((("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
All quiet, furry things are big.
((("something" "is" "quiet" "+") ("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
If something is quiet then it is furry.
((("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
All quiet things are round.
((("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
All blue, big things are quiet.
((("something" "is" "blue" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
If Charlie is blue and Charlie is big then Charlie is green.
((("Charlie" "is" "blue" "+") ("Charlie" "is" "big" "+")) -> ("Charlie" "is" "green" "+"))
Charlie is blue.
True
1
proof
[(triple1)]
("Charlie" "is" "blue" "+")
triple1
Charlie is not blue.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "blue" "-")
triple1
Charlie is big.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "big" "+")
((triple1) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "big" "-")
((triple1) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
True
3
proof
[(((((triple1) -> rule2)) -> rule3) OR ((triple1 ((triple1) -> rule2)) -> rule7))]
("Charlie" "is" "quiet" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((triple1 ((triple1) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not quiet.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3) OR ((triple1 ((triple1) -> rule2)) -> rule7))]
("Charlie" "is" "quiet" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((triple1 ((triple1) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is round.
True
4
proof
[(((((((triple1) -> rule2)) -> rule3)) -> rule6) OR ((((triple1 ((triple1) -> rule2)) -> rule7)) -> rule6))]
("Charlie" "is" "round" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is not round.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule3)) -> rule6) OR ((((triple1 ((triple1) -> rule2)) -> rule7)) -> rule6))]
("Charlie" "is" "round" "-")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
@0: Charlie is blue.[(triple1)] @1: Charlie is big.[(((triple1) -> rule2))] @2: Charlie is green.[(((triple1 ((triple1) -> rule2)) -> rule8))] Charlie is quiet.[(((((triple1) -> rule2)) -> rule3) OR ((triple1 ((triple1) -> rule2)) -> rule7))] @3: Charlie is furry.[(((((((triple1) -> rule2)) -> rule3)) -> rule5) OR ((((triple1 ((triple1) -> rule2)) -> rule7)) -> rule5))] Charlie is round.[(((((((triple1) -> rule2)) -> rule3)) -> rule6) OR ((((triple1 ((triple1) -> rule2)) -> rule7)) -> rule6))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
((triple1) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
((triple1 ((triple1) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3