Charlie is cold. Charlie is not furry. Charlie is quiet. Charlie is smart. Gary is cold. Gary is furry. Gary is green. Gary is quiet. Gary is round. Gary is smart. Round people are big. If Charlie is round and Charlie is furry then Charlie is not green. Smart, big people are cold. If someone is cold then they are round. If Charlie is smart and Charlie is not big then Charlie is not quiet. If someone is cold and quiet then they are green.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Round people are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If Charlie is round and Charlie is furry then Charlie is not green.
((("Charlie" "is" "round" "+") ("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "green" "-"))
Smart, big people are cold.
((("someone" "is" "smart" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
If someone is cold then they are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If Charlie is smart and Charlie is not big then Charlie is not quiet.
((("Charlie" "is" "smart" "+") ("Charlie" "is" "big" "~")) -> ("Charlie" "is" "quiet" "-"))
If someone is cold and quiet then they are green.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
Gary is smart.
True
1
proof
[(triple10)]
("Gary" "is" "smart" "+")
triple10
Gary is not round.
False
1
inv-proof
[(triple9 OR ((triple5) -> rule4))]
("Gary" "is" "round" "-")
triple9
((triple5) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Charlie is green.
True
3
proof
[(((triple1 triple3) -> rule6))]
("Charlie" "is" "green" "+")
((triple1 triple3) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not green.
False
3
inv-proof
[(((triple1 triple3) -> rule6))]
("Charlie" "is" "green" "-")
((triple1 triple3) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is big.
True
3
proof
[(((((triple1) -> rule4)) -> rule1))]
("Charlie" "is" "big" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is not big.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule1))]
("Charlie" "is" "big" "-")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
@0: Charlie is cold.[(triple1)] Charlie is not furry.[(triple2)] Charlie is quiet.[(triple3)] Charlie is smart.[(triple4)] Gary is cold.[(triple5 OR ((triple10 ((triple9) -> rule1)) -> rule3))] Gary is furry.[(triple6)] Gary is green.[(triple7 OR ((triple5 triple8) -> rule6) OR ((((triple10 ((triple9) -> rule1)) -> rule3) triple8) -> rule6))] Gary is quiet.[(triple8)] Gary is round.[(triple9 OR ((triple5) -> rule4))] Gary is smart.[(triple10)] @1: Charlie is green.[(((triple1 triple3) -> rule6))] Charlie is round.[(((triple1) -> rule4))] Gary is big.[(((triple9) -> rule1) OR ((((triple5) -> rule4)) -> rule1))] @2: Charlie is big.[(((((triple1) -> rule4)) -> rule1))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
triple5
((triple10 ((triple9) -> (rule1 % int2))) -> (rule3 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
triple6
Gary is green.
("Gary" "is" "green" "+")
triple7
((triple5 triple8) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
((((triple10 ((triple9) -> (rule1 % int3))) -> (rule3 % int2)) triple8) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple8
Gary is round.
("Gary" "is" "round" "+")
triple9
((triple5) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple10
Charlie is green.
("Charlie" "is" "green" "+")
((triple1 triple3) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
((triple1) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((triple9) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
((((triple5) -> (rule4 % int2))) -> (rule1 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2