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