Charlie is furry. Charlie is white. Dave is furry. Dave is red. Dave is white. Gary is kind. Gary is white. All red, white people are furry. Round, red people are furry. All furry people are red. All red, furry people are nice. All furry, round people are red. If someone is red then they are round. If someone is smart then they are kind. Round people are smart.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is white.
("Gary" "is" "white" "+")
All red, white people are furry.
((("someone" "is" "red" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
Round, red people are furry.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
All furry people are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
All red, furry people are nice.
((("someone" "is" "red" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
All furry, round people are red.
((("someone" "is" "furry" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If someone is red then they are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If someone is smart then they are kind.
((("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
Round people are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
Charlie is furry.
True
1
proof
[(triple1)]
("Charlie" "is" "furry" "+")
triple1
Gary is not white.
False
1
inv-proof
[(triple7)]
("Gary" "is" "white" "-")
triple7
@0: Charlie is furry.[(triple1)] Charlie is white.[(triple2)] Dave is furry.[(triple3 OR ((triple4 triple5) -> rule1) OR ((((triple4) -> rule6) triple4) -> rule2))] Dave is red.[(triple4 OR ((triple3) -> rule3))] Dave is white.[(triple5)] Gary is kind.[(triple6)] Gary is white.[(triple7)] @1: Charlie is red.[(((triple1) -> rule3))] Dave is nice.[(((triple4 triple3) -> rule4) OR ((triple4 ((triple4 triple5) -> rule1)) -> rule4) OR ((((triple3) -> rule3) triple3) -> rule4) OR ((((triple3) -> rule3) ((triple4 triple5) -> rule1)) -> rule4) OR ((triple4 ((((triple4) -> rule6) triple4) -> rule2)) -> rule4) OR ((((triple3) -> rule3) ((((triple4) -> rule6) triple4) -> rule2)) -> rule4))] Dave is round.[(((triple4) -> rule6) OR ((((triple3) -> rule3)) -> rule6))] @2: Charlie is nice.[(((((triple1) -> rule3) triple1) -> rule4))] Charlie is round.[(((((triple1) -> rule3)) -> rule6))] Dave is smart.[(((((triple4) -> rule6)) -> rule8) OR ((((((triple3) -> rule3)) -> rule6)) -> rule8))] @3: Charlie is smart.[(((((((triple1) -> rule3)) -> rule6)) -> rule8))] Dave is kind.[(((((((triple4) -> rule6)) -> rule8)) -> rule7) OR ((((((((triple3) -> rule3)) -> rule6)) -> rule8)) -> rule7))] @4: Charlie is kind.[(((((((((triple1) -> rule3)) -> rule6)) -> rule8)) -> rule7))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is white.
("Charlie" "is" "white" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
((triple4 triple5) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple4) -> (rule6 % int2)) triple4) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple4
((triple3) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple5
Gary is kind.
("Gary" "is" "kind" "+")
triple6
Gary is white.
("Gary" "is" "white" "+")
triple7
Charlie is red.
("Charlie" "is" "red" "+")
((triple1) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple4 triple3) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple4 ((triple4 triple5) -> (rule1 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((triple3) -> (rule3 % int2)) triple3) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
((((triple3) -> (rule3 % int3)) ((triple4 triple5) -> (rule1 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
((triple4 ((((triple4) -> (rule6 % int3)) triple4) -> (rule2 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((((triple3) -> (rule3 % int4)) ((((triple4) -> (rule6 % int3)) triple4) -> (rule2 % int2))) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
Dave is round.
("Dave" "is" "round" "+")
((triple4) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((triple4) -> (rule6 % int2))) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
((((((triple4) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
((((((((triple3) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Dave is red.
("Dave" "is" "red" "+")
int4
Charlie is kind.
("Charlie" "is" "kind" "+")
((((((((triple1) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4