Charlie is cold. Charlie is young. Gary is not quiet. White things are quiet. If something is white and round then it is not cold. All cold things are white.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is not quiet.
("Gary" "is" "quiet" "-")
White things are quiet.
((("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
If something is white and round then it is not cold.
((("something" "is" "white" "+") ("something" "is" "round" "+")) -> ("something" "is" "cold" "-"))
All cold things are white.
((("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
Gary is not quiet.
True
1
proof
[(triple3)]
("Gary" "is" "quiet" "-")
triple3
Gary is quiet.
False
1
inv-proof
[(triple3)]
("Gary" "is" "quiet" "+")
triple3
Charlie is white.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "white" "+")
((triple1) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "white" "-")
((triple1) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Charlie" "is" "quiet" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not quiet.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Charlie" "is" "quiet" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Gary is not white.
Unknown
inv-rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "white" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
Charlie is not kind.
Unknown
inv-random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Charlie is cold.[(triple1)] Charlie is young.[(triple2)] Gary is not quiet.[(triple3)] @1: Charlie is white.[(((triple1) -> rule3))] @2: Charlie is quiet.[(((((triple1) -> rule3)) -> rule1))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is young.
("Charlie" "is" "young" "+")
triple2
Gary is not quiet.
("Gary" "is" "quiet" "-")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
((triple1) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2