Anne is quiet. Bob is blue. Dave is not furry. Gary is not green. All quiet, cold people are not blue. If Dave is blue then Dave is green. If someone is cold and smart then they are furry. All smart people are cold. If someone is blue and young then they are not cold. All quiet people are smart.
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Dave is not furry.
("Dave" "is" "furry" "-")
Gary is not green.
("Gary" "is" "green" "-")
All quiet, cold people are not blue.
((("someone" "is" "quiet" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "-"))
If Dave is blue then Dave is green.
((("Dave" "is" "blue" "+")) -> ("Dave" "is" "green" "+"))
If someone is cold and smart then they are furry.
((("someone" "is" "cold" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
All smart people are cold.
((("someone" "is" "smart" "+")) -> ("someone" "is" "cold" "+"))
If someone is blue and young then they are not cold.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "cold" "-"))
All quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
Dave is not furry.
True
1
proof
[(triple3)]
("Dave" "is" "furry" "-")
triple3
Gary is green.
False
1
inv-proof
[(triple4)]
("Gary" "is" "green" "+")
triple4
Anne is smart.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule6))]
("Anne" "is" "smart" "-")
((triple1) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
True
3
proof
[(((((triple1) -> rule6)) -> rule4))]
("Anne" "is" "cold" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not cold.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule4))]
("Anne" "is" "cold" "-")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not blue.
True
5
proof
[(((triple1 ((((triple1) -> rule6)) -> rule4)) -> rule1))]
("Anne" "is" "blue" "-")
((triple1 ((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is blue.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule6)) -> rule4)) -> rule1))]
("Anne" "is" "blue" "+")
((triple1 ((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "smart" "-")
Dave is cold.
Unknown
rconc
[@2: Dave is cold.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Dave" "is" "cold" "+")
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "smart" "-")
Gary is cold.
Unknown
rconc
[@2: Gary is cold.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Gary" "is" "cold" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Anne is quiet.[(triple1)] Bob is blue.[(triple2)] Dave is not furry.[(triple3)] Gary is not green.[(triple4)] @1: Anne is smart.[(((triple1) -> rule6))] @2: Anne is cold.[(((((triple1) -> rule6)) -> rule4))] @3: Anne is furry.[(((((((triple1) -> rule6)) -> rule4) ((triple1) -> rule6)) -> rule3))] Anne is not blue.[(((triple1 ((((triple1) -> rule6)) -> rule4)) -> rule1))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
Dave is not furry.
("Dave" "is" "furry" "-")
triple3
Gary is not green.
("Gary" "is" "green" "-")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
((((((triple1) -> (rule6 % int3))) -> (rule4 % int2)) ((triple1) -> (rule6 % int3))) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is not blue.
("Anne" "is" "blue" "-")
((triple1 ((((triple1) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3