Anne is white. Bob is smart. Dave is smart. If someone is rough and furry then they are big. All white people are big. All smart, rough people are big. All white people are furry. Rough people are cold. Furry people are cold. All smart, cold people are rough. White, cold people are rough.
Anne is white.
("Anne" "is" "white" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is smart.
("Dave" "is" "smart" "+")
If someone is rough and furry then they are big.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
All white people are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
All smart, rough people are big.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
All white people are furry.
((("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
Rough people are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
Furry people are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
All smart, cold people are rough.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
White, cold people are rough.
((("someone" "is" "white" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
Dave is smart.
True
1
proof
[(triple3)]
("Dave" "is" "smart" "+")
triple3
Dave is not smart.
False
1
inv-proof
[(triple3)]
("Dave" "is" "smart" "-")
triple3
Anne is furry.
True
2
proof
[(((triple1) -> rule4))]
("Anne" "is" "furry" "+")
((triple1) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not furry.
False
2
inv-proof
[(((triple1) -> rule4))]
("Anne" "is" "furry" "-")
((triple1) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
True
3
proof
[(((((triple1) -> rule4)) -> rule6))]
("Anne" "is" "cold" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not cold.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule6))]
("Anne" "is" "cold" "-")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is rough.
True
5
proof
[(((triple1 ((((triple1) -> rule4)) -> rule6)) -> rule8))]
("Anne" "is" "rough" "+")
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is not rough.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule4)) -> rule6)) -> rule8))]
("Anne" "is" "rough" "-")
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Bob is not rough.
Unknown
inv-rconc
[@3: Bob is rough.[CWA. Example of deepest failure = (rule7 <- rule5 <- rule8 <- FAIL)]]
("Bob" "is" "rough" "-")
Dave is cold.
Unknown
rconc
[@4: Dave is cold.[CWA. Example of deepest failure = (rule5 <- rule7 <- rule6 <- rule4 <- FAIL)]]
("Dave" "is" "cold" "+")
Bob is not big.
Unknown
inv-rconc
[@4: Bob is big.[CWA. Example of deepest failure = (rule3 <- rule7 <- rule5 <- rule8 <- FAIL)]]
("Bob" "is" "big" "-")
Dave is furry.
Unknown
rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "furry" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is white.[(triple1)] Bob is smart.[(triple2)] Dave is smart.[(triple3)] @1: Anne is big.[(((triple1) -> rule2) OR ((((triple1 ((((triple1) -> rule4)) -> rule6)) -> rule8) ((triple1) -> rule4)) -> rule1))] Anne is furry.[(((triple1) -> rule4))] @2: Anne is cold.[(((((triple1) -> rule4)) -> rule6))] @3: Anne is rough.[(((triple1 ((((triple1) -> rule4)) -> rule6)) -> rule8))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
((((triple1 ((((triple1) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule8 % int2)) ((triple1) -> (rule4 % int4))) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule4 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
((((triple1) -> (rule4 % int2))) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3