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