Anne is cold. Erin is cold. Erin is furry. Erin is red. Fiona is furry. Fiona is green. Fiona is nice. If something is cold then it is smart. Smart, green things are blue. If something is cold then it is red. If something is red and not furry then it is cold. Red things are green. If Anne is not cold then Anne is not nice.
Anne is cold.
("Anne" "is" "cold" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is red.
("Erin" "is" "red" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
If something is cold then it is smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Smart, green things are blue.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If something is cold then it is red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
If something is red and not furry then it is cold.
((("something" "is" "red" "+") ("something" "is" "furry" "~")) -> ("something" "is" "cold" "+"))
Red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
If Anne is not cold then Anne is not nice.
((("Anne" "is" "cold" "~")) -> ("Anne" "is" "nice" "-"))
Erin is cold.
True
1
proof
[(triple2)]
("Erin" "is" "cold" "+")
triple2
Anne is not cold.
False
1
inv-proof
[(triple1)]
("Anne" "is" "cold" "-")
triple1
Anne is red.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "red" "+")
((triple1) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not red.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "red" "-")
((triple1) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is green.
True
3
proof
[(((((triple1) -> rule3)) -> rule5))]
("Anne" "is" "green" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is not green.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule5))]
("Anne" "is" "green" "-")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is blue.
True
6
proof
[(((((triple1) -> rule1) ((((triple1) -> rule3)) -> rule5)) -> rule2))]
("Anne" "is" "blue" "+")
((((triple1) -> (rule1 % int4)) ((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is not blue.
False
6
inv-proof
[(((((triple1) -> rule1) ((((triple1) -> rule3)) -> rule5)) -> rule2))]
("Anne" "is" "blue" "-")
((((triple1) -> (rule1 % int4)) ((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Fiona is not smart.
Unknown
inv-rconc
[@2: Fiona is smart.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is red.
Unknown
rconc
[@2: Fiona is red.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("Fiona" "is" "red" "+")
Fiona is not blue.
Unknown
inv-rconc
[@3: Fiona is blue.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule4 <- FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is cold.
Unknown
rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "cold" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
@0: Anne is cold.[(triple1)] Erin is cold.[(triple2)] Erin is furry.[(triple3)] Erin is red.[(triple4 OR ((triple2) -> rule3))] Fiona is furry.[(triple5)] Fiona is green.[(triple6)] Fiona is nice.[(triple7)] @1: Anne is red.[(((triple1) -> rule3))] Anne is smart.[(((triple1) -> rule1))] Erin is green.[(((triple4) -> rule5) OR ((((triple2) -> rule3)) -> rule5))] Erin is smart.[(((triple2) -> rule1))] @2: Anne is green.[(((((triple1) -> rule3)) -> rule5))] Erin is blue.[(((((triple2) -> rule1) ((triple4) -> rule5)) -> rule2) OR ((((triple2) -> rule1) ((((triple2) -> rule3)) -> rule5)) -> rule2))] @3: Anne is blue.[(((((triple1) -> rule1) ((((triple1) -> rule3)) -> rule5)) -> rule2))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
triple3
Erin is red.
("Erin" "is" "red" "+")
triple4
((triple2) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple5
Fiona is green.
("Fiona" "is" "green" "+")
triple6
Fiona is nice.
("Fiona" "is" "nice" "+")
triple7
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple4) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((triple2) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
((((triple2) -> (rule1 % int3)) ((triple4) -> (rule5 % int2))) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
((((triple2) -> (rule1 % int4)) ((((triple2) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
int4
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule1 % int4)) ((((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4