Anne is red. Erin is smart. Gary is quiet. All smart things are red. If Gary is quiet then Gary is smart. If something is smart then it is green. All blue, quiet things are green. If something is green then it is white. If Anne is smart then Anne is not blue.
Anne is red.
("Anne" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
All smart things are red.
((("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
If Gary is quiet then Gary is smart.
((("Gary" "is" "quiet" "+")) -> ("Gary" "is" "smart" "+"))
If something is smart then it is green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
All blue, quiet things are green.
((("something" "is" "blue" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
If something is green then it is white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If Anne is smart then Anne is not blue.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "blue" "-"))
Erin is smart.
True
1
proof
[(triple2)]
("Erin" "is" "smart" "+")
triple2
Erin is not smart.
False
1
inv-proof
[(triple2)]
("Erin" "is" "smart" "-")
triple2
Erin is green.
True
2
proof
[(((triple2) -> rule3))]
("Erin" "is" "green" "+")
((triple2) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not red.
False
2
inv-proof
[(((triple2) -> rule1))]
("Erin" "is" "red" "-")
((triple2) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
True
3
proof
[(((((triple2) -> rule3)) -> rule5))]
("Erin" "is" "white" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is not white.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule5))]
("Erin" "is" "white" "-")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Gary is white.
True
4
proof
[(((((((triple3) -> rule2)) -> rule3)) -> rule5))]
("Gary" "is" "white" "+")
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not white.
False
4
inv-proof
[(((((((triple3) -> rule2)) -> rule3)) -> rule5))]
("Gary" "is" "white" "-")
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "green" "-")
Anne is white.
Unknown
rconc
[@2: Anne is white.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Anne" "is" "white" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
@0: Anne is red.[(triple1)] Erin is smart.[(triple2)] Gary is quiet.[(triple3)] @1: Erin is green.[(((triple2) -> rule3))] Erin is red.[(((triple2) -> rule1))] Gary is smart.[(((triple3) -> rule2))] @2: Erin is white.[(((((triple2) -> rule3)) -> rule5))] Gary is green.[(((((triple3) -> rule2)) -> rule3))] Gary is red.[(((((triple3) -> rule2)) -> rule1))] @3: Gary is white.[(((((((triple3) -> rule2)) -> rule3)) -> rule5))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
triple2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Erin is green.
("Erin" "is" "green" "+")
((triple2) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple2) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple3) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((((triple3) -> (rule2 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3