Anne is blue. Charlie is round. Erin is blue. Fiona is furry. Cold people are furry. Furry people are red. Furry people are red. If Anne is blue then Anne is cold. If Charlie is not smart and Charlie is not round then Charlie is red. If Erin is blue and Erin is not red then Erin is round.
Anne is blue.
("Anne" "is" "blue" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Cold people are furry.
((("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
Furry people are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
Furry people are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
If Anne is blue then Anne is cold.
((("Anne" "is" "blue" "+")) -> ("Anne" "is" "cold" "+"))
If Charlie is not smart and Charlie is not round then Charlie is red.
((("Charlie" "is" "smart" "~") ("Charlie" "is" "round" "~")) -> ("Charlie" "is" "red" "+"))
If Erin is blue and Erin is not red then Erin is round.
((("Erin" "is" "blue" "+") ("Erin" "is" "red" "~")) -> ("Erin" "is" "round" "+"))
Fiona is furry.
True
1
proof
[(triple4)]
("Fiona" "is" "furry" "+")
triple4
Erin is not blue.
False
1
inv-proof
[(triple3)]
("Erin" "is" "blue" "-")
triple3
Anne is cold.
True
2
proof
[(((triple1) -> rule4))]
("Anne" "is" "cold" "+")
((triple1) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Fiona is not red.
False
2
inv-proof
[(((triple4) -> rule2) OR ((triple4) -> rule3))]
("Fiona" "is" "red" "-")
((triple4) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((triple4) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Anne is furry.
True
3
proof
[(((((triple1) -> rule4)) -> rule1))]
("Anne" "is" "furry" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is not furry.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule1))]
("Anne" "is" "furry" "-")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is red.
True
4
proof
[(((((((triple1) -> rule4)) -> rule1)) -> rule2) OR ((((((triple1) -> rule4)) -> rule1)) -> rule3))]
("Anne" "is" "red" "+")
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is not red.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule1)) -> rule2) OR ((((((triple1) -> rule4)) -> rule1)) -> rule3))]
("Anne" "is" "red" "-")
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is red.
Unknown
rconc
[@2: Charlie is red.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Charlie" "is" "red" "+")
Erin is not furry.
Unknown
inv-rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "furry" "-")
Erin is red.
Unknown
rconc
[@2: Erin is red.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Erin" "is" "red" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Fiona is not cold.
Unknown
inv-random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Anne is blue.[(triple1)] Charlie is round.[(triple2)] Erin is blue.[(triple3)] Fiona is furry.[(triple4)] @1: Anne is cold.[(((triple1) -> rule4))] Fiona is red.[(((triple4) -> rule2) OR ((triple4) -> rule3))] @2: Anne is furry.[(((((triple1) -> rule4)) -> rule1))] @3: Anne is red.[(((((((triple1) -> rule4)) -> rule1)) -> rule2) OR ((((((triple1) -> rule4)) -> rule1)) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Erin is blue.
("Erin" "is" "blue" "+")
triple3
Fiona is furry.
("Fiona" "is" "furry" "+")
triple4
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple4) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((triple4) -> (rule3 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3