Charlie is furry. Charlie is green. Charlie is kind. Charlie is white. Erin is big. Erin is furry. Erin is green. Erin is kind. Erin is quiet. Erin is white. If someone is white and big then they are smart. If Charlie is big then Charlie is quiet. If Charlie is furry and Charlie is white then Charlie is smart. All smart, quiet people are big. All white, smart people are quiet. If Erin is white and Erin is quiet then Erin is kind. Green, smart people are big. All white people are green.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is white.
("Erin" "is" "white" "+")
If someone is white and big then they are smart.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
If Charlie is big then Charlie is quiet.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "quiet" "+"))
If Charlie is furry and Charlie is white then Charlie is smart.
((("Charlie" "is" "furry" "+") ("Charlie" "is" "white" "+")) -> ("Charlie" "is" "smart" "+"))
All smart, quiet people are big.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
All white, smart people are quiet.
((("someone" "is" "white" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
If Erin is white and Erin is quiet then Erin is kind.
((("Erin" "is" "white" "+") ("Erin" "is" "quiet" "+")) -> ("Erin" "is" "kind" "+"))
Green, smart people are big.
((("someone" "is" "green" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
All white people are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
Charlie is green.
True
1
proof
[(triple2 OR ((triple4) -> rule8))]
("Charlie" "is" "green" "+")
triple2
((triple4) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not furry.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "furry" "-")
triple1
Charlie is smart.
True
3
proof
[(((triple1 triple4) -> rule3))]
("Charlie" "is" "smart" "+")
((triple1 triple4) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Erin is not smart.
False
3
inv-proof
[(((triple10 triple5) -> rule1))]
("Erin" "is" "smart" "-")
((triple10 triple5) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
@0: Charlie is furry.[(triple1)] Charlie is green.[(triple2 OR ((triple4) -> rule8))] Charlie is kind.[(triple3)] Charlie is white.[(triple4)] Erin is big.[(triple5)] Erin is furry.[(triple6)] Erin is green.[(triple7 OR ((triple10) -> rule8))] Erin is kind.[(triple8 OR ((triple10 triple9) -> rule6) OR ((triple10 ((triple10 ((triple10 triple5) -> rule1)) -> rule5)) -> rule6))] Erin is quiet.[(triple9 OR ((triple10 ((triple10 triple5) -> rule1)) -> rule5))] Erin is white.[(triple10)] @1: Charlie is smart.[(((triple1 triple4) -> rule3))] Erin is smart.[(((triple10 triple5) -> rule1))] @2: Charlie is big.[(((triple2 ((triple1 triple4) -> rule3)) -> rule7) OR ((((triple4) -> rule8) ((triple1 triple4) -> rule3)) -> rule7) OR ((((triple1 triple4) -> rule3) ((triple4 ((triple1 triple4) -> rule3)) -> rule5)) -> rule4))] Charlie is quiet.[(((triple4 ((triple1 triple4) -> rule3)) -> rule5) OR ((((triple2 ((triple1 triple4) -> rule3)) -> rule7)) -> rule2) OR ((((((triple4) -> rule8) ((triple1 triple4) -> rule3)) -> rule7)) -> rule2))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
((triple4) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
triple5
Erin is furry.
("Erin" "is" "furry" "+")
triple6
Erin is green.
("Erin" "is" "green" "+")
triple7
((triple10) -> (rule8 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
triple8
((triple10 triple9) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple10 ((triple10 ((triple10 triple5) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
((triple10 ((triple10 triple5) -> (rule1 % int2))) -> (rule5 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
triple10
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple1 triple4) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple10 triple5) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((triple2 ((triple1 triple4) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
((((triple4) -> (rule8 % int3)) ((triple1 triple4) -> (rule3 % int2))) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
((((triple1 triple4) -> (rule3 % int3)) ((triple4 ((triple1 triple4) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple4 ((triple1 triple4) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
((((triple2 ((triple1 triple4) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
((((((triple4) -> (rule8 % int4)) ((triple1 triple4) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4