Gary is round. All smart people are big. If someone is quiet and round then they are cold. If someone is round then they are quiet.
Gary is round.
("Gary" "is" "round" "+")
All smart people are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
If someone is quiet and round then they are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
If someone is round then they are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
Gary is round.
True
1
proof
[(triple1)]
("Gary" "is" "round" "+")
triple1
Gary is not round.
False
1
inv-proof
[(triple1)]
("Gary" "is" "round" "-")
triple1
Gary is quiet.
True
2
proof
[(((triple1) -> rule3))]
("Gary" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not quiet.
False
2
inv-proof
[(((triple1) -> rule3))]
("Gary" "is" "quiet" "-")
((triple1) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
True
4
proof
[(((((triple1) -> rule3) triple1) -> rule2))]
("Gary" "is" "cold" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not cold.
False
4
inv-proof
[(((((triple1) -> rule3) triple1) -> rule2))]
("Gary" "is" "cold" "-")
((((triple1) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "big" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Gary is round.[(triple1)] @1: Gary is quiet.[(((triple1) -> rule3))] @2: Gary is cold.[(((((triple1) -> rule3) triple1) -> rule2))]
Gary is round.
("Gary" "is" "round" "+")
triple1
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2