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