Anne is red. Bob is white. Charlie is not blue. Fiona is red. If Bob is cold and Bob is not blue then Bob is not smart. If Anne is cold and Anne is smart then Anne is furry. All furry things are cold. If Anne is red then Anne is cold. All cold things are furry. Furry things are smart.
Anne is red.
("Anne" "is" "red" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is not blue.
("Charlie" "is" "blue" "-")
Fiona is red.
("Fiona" "is" "red" "+")
If Bob is cold and Bob is not blue then Bob is not smart.
((("Bob" "is" "cold" "+") ("Bob" "is" "blue" "~")) -> ("Bob" "is" "smart" "-"))
If Anne is cold and Anne is smart then Anne is furry.
((("Anne" "is" "cold" "+") ("Anne" "is" "smart" "+")) -> ("Anne" "is" "furry" "+"))
All furry things are cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
If Anne is red then Anne is cold.
((("Anne" "is" "red" "+")) -> ("Anne" "is" "cold" "+"))
All cold things are furry.
((("something" "is" "cold" "+")) -> ("something" "is" "furry" "+"))
Furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
Fiona is red.
True
1
proof
[(triple4)]
("Fiona" "is" "red" "+")
triple4
Anne is not red.
False
1
inv-proof
[(triple1)]
("Anne" "is" "red" "-")
triple1
Anne is cold.
True
2
proof
[(((triple1) -> rule4))]
("Anne" "is" "cold" "+")
((triple1) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not cold.
False
2
inv-proof
[(((triple1) -> rule4))]
("Anne" "is" "cold" "-")
((triple1) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
True
3
proof
[(((((triple1) -> rule4)) -> rule5))]
("Anne" "is" "furry" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % 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)) -> rule5))]
("Anne" "is" "furry" "-")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is smart.
True
4
proof
[(((((((triple1) -> rule4)) -> rule5)) -> rule6))]
("Anne" "is" "smart" "+")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is not smart.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule5)) -> rule6))]
("Anne" "is" "smart" "-")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Fiona is not cold.
Unknown
inv-rconc
[@2: Fiona is cold.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Fiona" "is" "cold" "-")
Charlie is furry.
Unknown
rconc
[@2: Charlie is furry.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Charlie" "is" "furry" "+")
Fiona is not furry.
Unknown
inv-rconc
[@2: Fiona is furry.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Fiona" "is" "furry" "-")
Bob is cold.
Unknown
rconc
[@2: Bob is cold.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Bob" "is" "cold" "+")
Anne is not white.
Unknown
inv-random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
Fiona is not round.
Unknown
inv-random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Anne is red.[(triple1)] Bob is white.[(triple2)] Charlie is not blue.[(triple3)] Fiona is red.[(triple4)] @1: Anne is cold.[(((triple1) -> rule4))] @2: Anne is furry.[(((((triple1) -> rule4)) -> rule5))] @3: Anne is smart.[(((((((triple1) -> rule4)) -> rule5)) -> rule6))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Charlie is not blue.
("Charlie" "is" "blue" "-")
triple3
Fiona is red.
("Fiona" "is" "red" "+")
triple4
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3