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