Gary is big. Gary is cold. Gary is nice. If Gary is nice then Gary is cold. If something is big and nice then it is young. All nice things are quiet.
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is nice.
("Gary" "is" "nice" "+")
If Gary is nice then Gary is cold.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "cold" "+"))
If something is big and nice then it is young.
((("something" "is" "big" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
All nice things are quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
Gary is nice.
True
1
proof
[(triple3)]
("Gary" "is" "nice" "+")
triple3
Gary is not big.
False
1
inv-proof
[(triple1)]
("Gary" "is" "big" "-")
triple1
Gary is quiet.
True
2
proof
[(((triple3) -> rule3))]
("Gary" "is" "quiet" "+")
((triple3) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not young.
False
3
inv-proof
[(((triple1 triple3) -> rule2))]
("Gary" "is" "young" "-")
((triple1 triple3) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Gary is big.[(triple1)] Gary is cold.[(triple2 OR ((triple3) -> rule1))] Gary is nice.[(triple3)] @1: Gary is quiet.[(((triple3) -> rule3))] Gary is young.[(((triple1 triple3) -> rule2))]
Gary is big.
("Gary" "is" "big" "+")
triple1
Gary is cold.
("Gary" "is" "cold" "+")
triple2
((triple3) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple3) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple1 triple3) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1