Anne is nice. Erin is green. Fiona is furry. Gary is cold. All white things are red. If something is white and cold then it is not red. If something is cold and not nice then it is red. All nice things are not young. Green things are white. If something is nice then it is green.
Anne is nice.
("Anne" "is" "nice" "+")
Erin is green.
("Erin" "is" "green" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Gary is cold.
("Gary" "is" "cold" "+")
All white things are red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
If something is white and cold then it is not red.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "red" "-"))
If something is cold and not nice then it is red.
((("something" "is" "cold" "+") ("something" "is" "nice" "~")) -> ("something" "is" "red" "+"))
All nice things are not young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "-"))
Green things are white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If something is nice then it is green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
Erin is green.
True
1
proof
[(triple2)]
("Erin" "is" "green" "+")
triple2
Anne is not nice.
False
1
inv-proof
[(triple1)]
("Anne" "is" "nice" "-")
triple1
Erin is white.
True
2
proof
[(((triple2) -> rule5))]
("Erin" "is" "white" "+")
((triple2) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Anne is young.
False
2
inv-proof
[(((triple1) -> rule4))]
("Anne" "is" "young" "+")
((triple1) -> (rule4 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is white.
True
3
proof
[(((((triple1) -> rule6)) -> rule5))]
("Anne" "is" "white" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not white.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule5))]
("Anne" "is" "white" "-")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is red.
True
4
proof
[(((((((triple1) -> rule6)) -> rule5)) -> rule1))]
("Anne" "is" "red" "+")
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is not red.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule5)) -> rule1))]
("Anne" "is" "red" "-")
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Gary is not white.
Unknown
inv-rconc
[@2: Gary is white.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Gary" "is" "white" "-")
Fiona is green.
Unknown
rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "green" "+")
Gary is not red.
Unknown
inv-rconc
[@3: Gary is red.[CWA. Example of deepest failure = (rule1 <- rule5 <- rule6 <- FAIL)]]
("Gary" "is" "red" "-")
Fiona is white.
Unknown
rconc
[@2: Fiona is white.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Fiona" "is" "white" "+")
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
@0: Anne is nice.[(triple1)] Erin is green.[(triple2)] Fiona is furry.[(triple3)] Gary is cold.[(triple4)] @1: Anne is green.[(((triple1) -> rule6))] Anne is not young.[(((triple1) -> rule4))] Erin is white.[(((triple2) -> rule5))] @2: Anne is white.[(((((triple1) -> rule6)) -> rule5))] Erin is red.[(((((triple2) -> rule5)) -> rule1))] @3: Anne is red.[(((((((triple1) -> rule6)) -> rule5)) -> rule1))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not young.
("Anne" "is" "young" "-")
((triple1) -> (rule4 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple2) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((((((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3