Dave is not big. Dave is blue. Dave is red. If someone is cold and not red then they are not nice. All blue people are nice. If Dave is big and Dave is furry then Dave is white. White people are cold. If Dave is not furry then Dave is not nice. If someone is red then they are white.
Dave is not big.
("Dave" "is" "big" "-")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is red.
("Dave" "is" "red" "+")
If someone is cold and not red then they are not nice.
((("someone" "is" "cold" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "nice" "-"))
All blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If Dave is big and Dave is furry then Dave is white.
((("Dave" "is" "big" "+") ("Dave" "is" "furry" "+")) -> ("Dave" "is" "white" "+"))
White people are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
If Dave is not furry then Dave is not nice.
((("Dave" "is" "furry" "~")) -> ("Dave" "is" "nice" "-"))
If someone is red then they are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
Dave is not big.
True
1
proof
[(triple1)]
("Dave" "is" "big" "-")
triple1
Dave is not red.
False
1
inv-proof
[(triple3)]
("Dave" "is" "red" "-")
triple3
Dave is nice.
True
2
proof
[(((triple2) -> rule2))]
("Dave" "is" "nice" "+")
((triple2) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not white.
False
2
inv-proof
[(((triple3) -> rule6))]
("Dave" "is" "white" "-")
((triple3) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is cold.
True
3
proof
[(((((triple3) -> rule6)) -> rule4))]
("Dave" "is" "cold" "+")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not cold.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule4))]
("Dave" "is" "cold" "-")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
@0: Dave is blue.[(triple2)] Dave is not big.[(triple1)] Dave is red.[(triple3)] @1: Dave is nice.[(((triple2) -> rule2))] Dave is white.[(((triple3) -> rule6))] @2: Dave is cold.[(((((triple3) -> rule6)) -> rule4))]
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Dave is not big.
("Dave" "is" "big" "-")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
((triple2) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple3) -> (rule6 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2