Anne is big. Anne is not blue. Anne is furry. Anne is white. Bob is not big. Bob is white. Dave is not cold. Dave is furry. Dave is not quiet. Dave is red. Dave is white. Erin is big. Erin is blue. Erin is cold. Erin is furry. All cold, white people are quiet. If someone is cold then they are white. If someone is furry then they are red.
Anne is big.
("Anne" "is" "big" "+")
Anne is not blue.
("Anne" "is" "blue" "-")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is not big.
("Bob" "is" "big" "-")
Bob is white.
("Bob" "is" "white" "+")
Dave is not cold.
("Dave" "is" "cold" "-")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Dave is red.
("Dave" "is" "red" "+")
Dave is white.
("Dave" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
All cold, white people are quiet.
((("someone" "is" "cold" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If someone is cold then they are white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
If someone is furry then they are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
Dave is white.
True
1
proof
[(triple11)]
("Dave" "is" "white" "+")
triple11
Bob is big.
False
1
inv-proof
[(triple5)]
("Bob" "is" "big" "+")
triple5
Erin is white.
True
2
proof
[(((triple14) -> rule2))]
("Erin" "is" "white" "+")
((triple14) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is not red.
False
2
inv-proof
[(((triple15) -> rule3))]
("Erin" "is" "red" "-")
((triple15) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is quiet.
True
4
proof
[(((triple14 ((triple14) -> rule2)) -> rule1))]
("Erin" "is" "quiet" "+")
((triple14 ((triple14) -> (rule2 % int2))) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is not quiet.
False
4
inv-proof
[(((triple14 ((triple14) -> rule2)) -> rule1))]
("Erin" "is" "quiet" "-")
((triple14 ((triple14) -> (rule2 % int2))) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "quiet" "-")
Bob is red.
Unknown
rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "red" "+")
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "quiet" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Anne is big.[(triple1)] Anne is furry.[(triple3)] Anne is not blue.[(triple2)] Anne is white.[(triple4)] Bob is not big.[(triple5)] Bob is white.[(triple6)] Dave is furry.[(triple8)] Dave is not cold.[(triple7)] Dave is not quiet.[(triple9)] Dave is red.[(triple10 OR ((triple8) -> rule3))] Dave is white.[(triple11)] Erin is big.[(triple12)] Erin is blue.[(triple13)] Erin is cold.[(triple14)] Erin is furry.[(triple15)] @1: Anne is red.[(((triple3) -> rule3))] Erin is red.[(((triple15) -> rule3))] Erin is white.[(((triple14) -> rule2))] @2: Erin is quiet.[(((triple14 ((triple14) -> rule2)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple3
Anne is not blue.
("Anne" "is" "blue" "-")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple4
Bob is not big.
("Bob" "is" "big" "-")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
Dave is furry.
("Dave" "is" "furry" "+")
triple8
Dave is not cold.
("Dave" "is" "cold" "-")
triple7
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple9
Dave is red.
("Dave" "is" "red" "+")
triple10
((triple8) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple11
Erin is big.
("Erin" "is" "big" "+")
triple12
Erin is blue.
("Erin" "is" "blue" "+")
triple13
Erin is cold.
("Erin" "is" "cold" "+")
triple14
Erin is furry.
("Erin" "is" "furry" "+")
triple15
Anne is red.
("Anne" "is" "red" "+")
((triple3) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((triple15) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple14) -> (rule2 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple14 ((triple14) -> (rule2 % int2))) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2