Charlie is not red. Erin is red. Gary is cold. If Gary is red then Gary is not round. If Erin is quiet and Erin is white then Erin is cold. If Gary is smart then Gary is not quiet. Smart things are white. All red things are smart. If Gary is not smart and Gary is not quiet then Gary is not white. If something is red and blue then it is round. If something is white then it is round.
Charlie is not red.
("Charlie" "is" "red" "-")
Erin is red.
("Erin" "is" "red" "+")
Gary is cold.
("Gary" "is" "cold" "+")
If Gary is red then Gary is not round.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "round" "-"))
If Erin is quiet and Erin is white then Erin is cold.
((("Erin" "is" "quiet" "+") ("Erin" "is" "white" "+")) -> ("Erin" "is" "cold" "+"))
If Gary is smart then Gary is not quiet.
((("Gary" "is" "smart" "+")) -> ("Gary" "is" "quiet" "-"))
Smart things are white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
All red things are smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
If Gary is not smart and Gary is not quiet then Gary is not white.
((("Gary" "is" "smart" "~") ("Gary" "is" "quiet" "~")) -> ("Gary" "is" "white" "-"))
If something is red and blue then it is round.
((("something" "is" "red" "+") ("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If something is white then it is round.
((("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
Gary is cold.
True
1
proof
[(triple3)]
("Gary" "is" "cold" "+")
triple3
Erin is not red.
False
1
inv-proof
[(triple2)]
("Erin" "is" "red" "-")
triple2
Erin is smart.
True
2
proof
[(((triple2) -> rule5))]
("Erin" "is" "smart" "+")
((triple2) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not smart.
False
2
inv-proof
[(((triple2) -> rule5))]
("Erin" "is" "smart" "-")
((triple2) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
True
3
proof
[(((((triple2) -> rule5)) -> rule4))]
("Erin" "is" "white" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is not white.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule4))]
("Erin" "is" "white" "-")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
True
4
proof
[(((((((triple2) -> rule5)) -> rule4)) -> rule8))]
("Erin" "is" "round" "+")
((((((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is not round.
False
4
inv-proof
[(((((((triple2) -> rule5)) -> rule4)) -> rule8))]
("Erin" "is" "round" "-")
((((((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "smart" "-")
Gary is round.
Unknown
rconc
[@3: Gary is round.[CWA. Example of deepest failure = (rule8 <- rule4 <- rule5 <- FAIL)]]
("Gary" "is" "round" "+")
Gary is not white.
Unknown
inv-rconc
[@2: Gary is white.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Gary" "is" "white" "-")
Charlie is white.
Unknown
rconc
[@2: Charlie is white.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Charlie" "is" "white" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
@0: Charlie is not red.[(triple1)] Erin is red.[(triple2)] Gary is cold.[(triple3)] @1: Erin is smart.[(((triple2) -> rule5))] @2: Erin is white.[(((((triple2) -> rule5)) -> rule4))] @3: Erin is round.[(((((((triple2) -> rule5)) -> rule4)) -> rule8))]
Charlie is not red.
("Charlie" "is" "red" "-")
triple1
Erin is red.
("Erin" "is" "red" "+")
triple2
Gary is cold.
("Gary" "is" "cold" "+")
triple3
Erin is smart.
("Erin" "is" "smart" "+")
((triple2) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((((((triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3