Anne is round. Bob is blue. Fiona is smart. Gary is not cold. All smart, furry things are red. If something is round and quiet then it is furry. Round things are smart. Furry things are not cold. If something is cold and not round then it is blue. If something is smart then it is quiet.
Anne is round.
("Anne" "is" "round" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
All smart, furry things are red.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
If something is round and quiet then it is furry.
((("something" "is" "round" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
Round things are smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
Furry things are not cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "-"))
If something is cold and not round then it is blue.
((("something" "is" "cold" "+") ("something" "is" "round" "~")) -> ("something" "is" "blue" "+"))
If something is smart then it is quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
Bob is blue.
True
1
proof
[(triple2)]
("Bob" "is" "blue" "+")
triple2
Bob is not blue.
False
1
inv-proof
[(triple2)]
("Bob" "is" "blue" "-")
triple2
Anne is smart.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "smart" "-")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is quiet.
True
3
proof
[(((((triple1) -> rule3)) -> rule6))]
("Anne" "is" "quiet" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not quiet.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule6))]
("Anne" "is" "quiet" "-")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
True
5
proof
[(((triple1 ((((triple1) -> rule3)) -> rule6)) -> rule2))]
("Anne" "is" "furry" "+")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is not furry.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule3)) -> rule6)) -> rule2))]
("Anne" "is" "furry" "-")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Bob is not red.
Unknown
inv-rconc
[@2: Bob is red.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Bob" "is" "red" "-")
Gary is red.
Unknown
rconc
[@2: Gary is red.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Gary" "is" "red" "+")
Fiona is not blue.
Unknown
inv-rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "blue" "-")
Gary is smart.
Unknown
rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "smart" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
Fiona is not round.
Unknown
inv-random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
@0: Anne is round.[(triple1)] Bob is blue.[(triple2)] Fiona is smart.[(triple3)] Gary is not cold.[(triple4)] @1: Anne is smart.[(((triple1) -> rule3))] Fiona is quiet.[(((triple3) -> rule6))] @2: Anne is quiet.[(((((triple1) -> rule3)) -> rule6))] @3: Anne is furry.[(((triple1 ((((triple1) -> rule3)) -> rule6)) -> rule2))] @4: Anne is not cold.[(((((triple1 ((((triple1) -> rule3)) -> rule6)) -> rule2)) -> rule4))] Anne is red.[(((((triple1) -> rule3) ((triple1 ((((triple1) -> rule3)) -> rule6)) -> rule2)) -> rule1))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Gary is not cold.
("Gary" "is" "cold" "-")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple3) -> (rule6 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
((triple1 ((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is not cold.
("Anne" "is" "cold" "-")
((((triple1 ((((triple1) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule3 % int4)) ((triple1 ((((triple1) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4