Dave is blue. Dave is furry. Dave is nice. Dave is quiet. Dave is red. Dave is white. Gary is furry. Gary is nice. Gary is quiet. Gary is red. Gary is white. Gary is young. All blue people are white. Nice, quiet people are furry. If someone is white and furry then they are red. All quiet people are nice. White, quiet people are young. If Gary is red then Gary is quiet. If someone is blue and red then they are furry. If someone is blue and quiet then they are nice.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
All blue people are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
Nice, quiet people are furry.
((("someone" "is" "nice" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
If someone is white and furry then they are red.
((("someone" "is" "white" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
All quiet people are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
White, quiet people are young.
((("someone" "is" "white" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
If Gary is red then Gary is quiet.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "quiet" "+"))
If someone is blue and red then they are furry.
((("someone" "is" "blue" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
If someone is blue and quiet then they are nice.
((("someone" "is" "blue" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
Dave is blue.
True
1
proof
[(triple1)]
("Dave" "is" "blue" "+")
triple1
Gary is not white.
False
1
inv-proof
[(triple11)]
("Gary" "is" "white" "-")
triple11
@0: Dave is blue.[(triple1)] Dave is furry.[(triple2 OR ((triple1 triple5) -> rule7) OR ((triple3 triple4) -> rule2) OR ((((triple4) -> rule4) triple4) -> rule2) OR ((((triple1 triple4) -> rule8) triple4) -> rule2))] Dave is nice.[(triple3 OR ((triple4) -> rule4) OR ((triple1 triple4) -> rule8))] Dave is quiet.[(triple4)] Dave is red.[(triple5 OR ((triple6 triple2) -> rule3) OR ((triple6 ((triple3 triple4) -> rule2)) -> rule3) OR ((((triple1) -> rule1) triple2) -> rule3) OR ((((triple1) -> rule1) ((triple3 triple4) -> rule2)) -> rule3) OR ((triple6 ((((triple4) -> rule4) triple4) -> rule2)) -> rule3) OR ((triple6 ((((triple1 triple4) -> rule8) triple4) -> rule2)) -> rule3) OR ((((triple1) -> rule1) ((((triple4) -> rule4) triple4) -> rule2)) -> rule3) OR ((((triple1) -> rule1) ((((triple1 triple4) -> rule8) triple4) -> rule2)) -> rule3))] Dave is white.[(triple6 OR ((triple1) -> rule1))] Gary is furry.[(triple7 OR ((triple8 triple9) -> rule2) OR ((triple8 ((triple10) -> rule6)) -> rule2) OR ((((triple9) -> rule4) triple9) -> rule2) OR ((((triple9) -> rule4) ((triple10) -> rule6)) -> rule2) OR ((((((triple10) -> rule6)) -> rule4) triple9) -> rule2) OR ((((((triple10) -> rule6)) -> rule4) ((triple10) -> rule6)) -> rule2))] Gary is nice.[(triple8 OR ((triple9) -> rule4) OR ((((triple10) -> rule6)) -> rule4) OR ((((((triple11 triple7) -> rule3)) -> rule6)) -> rule4))] Gary is quiet.[(triple9 OR ((triple10) -> rule6) OR ((((triple11 triple7) -> rule3)) -> rule6))] Gary is red.[(triple10 OR ((triple11 triple7) -> rule3) OR ((triple11 ((triple8 triple9) -> rule2)) -> rule3) OR ((triple11 ((((triple9) -> rule4) triple9) -> rule2)) -> rule3))] Gary is white.[(triple11)] Gary is young.[(triple12 OR ((triple11 triple9) -> rule5) OR ((triple11 ((triple10) -> rule6)) -> rule5) OR ((triple11 ((((triple11 triple7) -> rule3)) -> rule6)) -> rule5))] @1: Dave is young.[(((triple6 triple4) -> rule5) OR ((((triple1) -> rule1) triple4) -> rule5))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
((triple1 triple5) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((triple3 triple4) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple4) -> (rule4 % int2)) triple4) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple1 triple4) -> (rule8 % int2)) triple4) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
((triple4) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple1 triple4) -> (rule8 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple4
Dave is red.
("Dave" "is" "red" "+")
triple5
((triple6 triple2) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
((triple6 ((triple3 triple4) -> (rule2 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
((((triple1) -> (rule1 % int2)) triple2) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
((((triple1) -> (rule1 % int3)) ((triple3 triple4) -> (rule2 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
((triple6 ((((triple4) -> (rule4 % int3)) triple4) -> (rule2 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((triple6 ((((triple1 triple4) -> (rule8 % int3)) triple4) -> (rule2 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
((((triple1) -> (rule1 % int4)) ((((triple4) -> (rule4 % int3)) triple4) -> (rule2 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
((((triple1) -> (rule1 % int4)) ((((triple1 triple4) -> (rule8 % int3)) triple4) -> (rule2 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
int4
Dave is white.
("Dave" "is" "white" "+")
triple6
((triple1) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
triple7
((triple8 triple9) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple8 ((triple10) -> (rule6 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((triple9) -> (rule4 % int2)) triple9) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
((((triple9) -> (rule4 % int3)) ((triple10) -> (rule6 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
((((((triple10) -> (rule6 % int3))) -> (rule4 % int2)) triple9) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
((((((triple10) -> (rule6 % int3))) -> (rule4 % int2)) ((triple10) -> (rule6 % int3))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
triple8
((triple9) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple10) -> (rule6 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((((((triple11 triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
triple9
((triple10) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple11 triple7) -> (rule3 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
triple10
((triple11 triple7) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple11 ((triple8 triple9) -> (rule2 % int2))) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
((triple11 ((((triple9) -> (rule4 % int3)) triple9) -> (rule2 % int2))) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is white.
("Gary" "is" "white" "+")
triple11
Gary is young.
("Gary" "is" "young" "+")
triple12
((triple11 triple9) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
((triple11 ((triple10) -> (rule6 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
((triple11 ((((triple11 triple7) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
((triple6 triple4) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple1) -> (rule1 % int2)) triple4) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2