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