Gary is not green. Gary is white. Gary is young. If Gary is young then Gary is not cold. If Gary is big then Gary is not quiet. If Gary is young then Gary is nice. If something is young and not nice then it is cold. If something is white and not cold then it is quiet. Green, white things are not quiet.
Gary is not green.
("Gary" "is" "green" "-")
Gary is white.
("Gary" "is" "white" "+")
Gary is young.
("Gary" "is" "young" "+")
If Gary is young then Gary is not cold.
((("Gary" "is" "young" "+")) -> ("Gary" "is" "cold" "-"))
If Gary is big then Gary is not quiet.
((("Gary" "is" "big" "+")) -> ("Gary" "is" "quiet" "-"))
If Gary is young then Gary is nice.
((("Gary" "is" "young" "+")) -> ("Gary" "is" "nice" "+"))
If something is young and not nice then it is cold.
((("something" "is" "young" "+") ("something" "is" "nice" "~")) -> ("something" "is" "cold" "+"))
If something is white and not cold then it is quiet.
((("something" "is" "white" "+") ("something" "is" "cold" "~")) -> ("something" "is" "quiet" "+"))
Green, white things are not quiet.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "-"))
Gary is not green.
True
1
proof
[(triple1)]
("Gary" "is" "green" "-")
triple1
Gary is not young.
False
1
inv-proof
[(triple3)]
("Gary" "is" "young" "-")
triple3
Gary is nice.
True
2
proof
[(((triple3) -> rule3))]
("Gary" "is" "nice" "+")
((triple3) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not nice.
False
2
inv-proof
[(((triple3) -> rule3))]
("Gary" "is" "nice" "-")
((triple3) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
@0: Gary is not green.[(triple1)] Gary is white.[(triple2)] Gary is young.[(triple3)] @1: Gary is nice.[(((triple3) -> rule3))] Gary is not cold.[(((triple3) -> rule1))] @2: Gary is quiet.[(((triple2 ((triple3) -> rule1)) -> rule5))]
Gary is not green.
("Gary" "is" "green" "-")
triple1
Gary is white.
("Gary" "is" "white" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Gary is nice.
("Gary" "is" "nice" "+")
((triple3) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not cold.
("Gary" "is" "cold" "-")
((triple3) -> (rule1 % int1))
Gary is not cold.
("Gary" "is" "cold" "-")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple2 ((triple3) -> (rule1 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not cold.
("Gary" "is" "cold" "-")
int2