Charlie is not smart. Dave is round. Fiona is rough. Gary is white. If someone is red and not smart then they are not white. If someone is smart then they are not white. All white people are quiet. If someone is round and smart then they are not rough. If someone is quiet then they are cold. If someone is rough and not quiet then they are not cold.
Charlie is not smart.
("Charlie" "is" "smart" "-")
Dave is round.
("Dave" "is" "round" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Gary is white.
("Gary" "is" "white" "+")
If someone is red and not smart then they are not white.
((("someone" "is" "red" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "white" "-"))
If someone is smart then they are not white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "-"))
All white people are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If someone is round and smart then they are not rough.
((("someone" "is" "round" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "-"))
If someone is quiet then they are cold.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "cold" "+"))
If someone is rough and not quiet then they are not cold.
((("someone" "is" "rough" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "cold" "-"))
Charlie is not smart.
True
1
proof
[(triple1)]
("Charlie" "is" "smart" "-")
triple1
Gary is not white.
False
1
inv-proof
[(triple4)]
("Gary" "is" "white" "-")
triple4
Gary is quiet.
True
2
proof
[(((triple4) -> rule3))]
("Gary" "is" "quiet" "+")
((triple4) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is not quiet.
False
2
inv-proof
[(((triple4) -> rule3))]
("Gary" "is" "quiet" "-")
((triple4) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
True
3
proof
[(((((triple4) -> rule3)) -> rule5))]
("Gary" "is" "cold" "+")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is not cold.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule5))]
("Gary" "is" "cold" "-")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "quiet" "-")
Charlie is quiet.
Unknown
rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Charlie is not cold.
Unknown
inv-rconc
[@2: Charlie is cold.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Charlie" "is" "cold" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Gary is not smart.
Unknown
inv-random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Charlie is not smart.[(triple1)] Dave is round.[(triple2)] Fiona is rough.[(triple3)] Gary is white.[(triple4)] @1: Gary is quiet.[(((triple4) -> rule3))] @2: Gary is cold.[(((((triple4) -> rule3)) -> rule5))]
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple1
Dave is round.
("Dave" "is" "round" "+")
triple2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple3
Gary is white.
("Gary" "is" "white" "+")
triple4
Gary is quiet.
("Gary" "is" "quiet" "+")
((triple4) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is cold.
("Gary" "is" "cold" "+")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2