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