Anne is cold. Charlie is blue. Dave is kind. Erin is rough. If something is smart and furry then it is green. If something is cold then it is smart. If something is rough then it is furry. If something is furry and rough then it is kind. Green, smart things are furry. If Erin is cold and Erin is blue then Erin is rough. All furry things are cold. All furry, kind things are rough.
Anne is cold.
("Anne" "is" "cold" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Erin is rough.
("Erin" "is" "rough" "+")
If something is smart and furry then it is green.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
If something is cold then it is smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If something is rough then it is furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
If something is furry and rough then it is kind.
((("something" "is" "furry" "+") ("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
Green, smart things are furry.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
If Erin is cold and Erin is blue then Erin is rough.
((("Erin" "is" "cold" "+") ("Erin" "is" "blue" "+")) -> ("Erin" "is" "rough" "+"))
All furry things are cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
All furry, kind things are rough.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
Anne is cold.
True
1
proof
[(triple1)]
("Anne" "is" "cold" "+")
triple1
Dave is not kind.
False
1
inv-proof
[(triple3)]
("Dave" "is" "kind" "-")
triple3
Anne is smart.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "smart" "-")
((triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Erin is kind.
True
4
proof
[(((((triple4) -> rule3) triple4) -> rule4))]
("Erin" "is" "kind" "+")
((((triple4) -> (rule3 % int2)) triple4) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is not kind.
False
4
inv-proof
[(((((triple4) -> rule3) triple4) -> rule4))]
("Erin" "is" "kind" "-")
((((triple4) -> (rule3 % int2)) triple4) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
True
4
proof
[(((((((triple4) -> rule3)) -> rule7)) -> rule2))]
("Erin" "is" "smart" "+")
((((((triple4) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is not smart.
False
4
inv-proof
[(((((((triple4) -> rule3)) -> rule7)) -> rule2))]
("Erin" "is" "smart" "-")
((((((triple4) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Anne is not furry.
Unknown
inv-rconc
[@4: Anne is furry.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule3 <- rule8 <- FAIL)]]
("Anne" "is" "furry" "-")
Charlie is furry.
Unknown
rconc
[@4: Charlie is furry.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule3 <- rule8 <- FAIL)]]
("Charlie" "is" "furry" "+")
Anne is not kind.
Unknown
inv-rconc
[@2: Anne is kind.[CWA. Example of deepest failure = (rule4 <- rule8 <- FAIL)]]
("Anne" "is" "kind" "-")
Anne is green.
Unknown
rconc
[@4: Anne is green.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule8 <- rule5 <- FAIL)]]
("Anne" "is" "green" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is cold.[(triple1)] Charlie is blue.[(triple2)] Dave is kind.[(triple3)] Erin is rough.[(triple4)] @1: Anne is smart.[(((triple1) -> rule2))] Erin is furry.[(((triple4) -> rule3))] @2: Erin is cold.[(((((triple4) -> rule3)) -> rule7))] Erin is kind.[(((((triple4) -> rule3) triple4) -> rule4))] @3: Erin is smart.[(((((((triple4) -> rule3)) -> rule7)) -> rule2))] @4: Erin is green.[(((((((((triple4) -> rule3)) -> rule7)) -> rule2) ((triple4) -> rule3)) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Erin is rough.
("Erin" "is" "rough" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple4) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((((triple4) -> (rule3 % int2))) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((((triple4) -> (rule3 % int2)) triple4) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
((((((triple4) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
((((((((triple4) -> (rule3 % int4))) -> (rule7 % int3))) -> (rule2 % int2)) ((triple4) -> (rule3 % int4))) -> (rule1 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
int4