Anne is nice. Anne is white. Bob is not big. Bob is not furry. Bob is quiet. Bob is white. Charlie is cold. Charlie is furry. Charlie is quiet. Dave is furry. Dave is quiet. Dave is not white. If Anne is not furry then Anne is quiet. Cold things are big. Furry things are smart. Furry things are quiet. If something is nice then it is white. White, big things are nice. Smart, furry things are cold. If something is white then it is not cold.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is not big.
("Bob" "is" "big" "-")
Bob is not furry.
("Bob" "is" "furry" "-")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is not white.
("Dave" "is" "white" "-")
If Anne is not furry then Anne is quiet.
((("Anne" "is" "furry" "~")) -> ("Anne" "is" "quiet" "+"))
Cold things are big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
Furry things are smart.
((("something" "is" "furry" "+")) -> ("something" "is" "smart" "+"))
Furry things are quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
If something is nice then it is white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
White, big things are nice.
((("something" "is" "white" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
Smart, furry things are cold.
((("something" "is" "smart" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
If something is white then it is not cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "-"))
Anne is nice.
True
1
proof
[(triple1)]
("Anne" "is" "nice" "+")
triple1
Anne is not white.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule5))]
("Anne" "is" "white" "-")
triple2
((triple1) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Bob is not cold.
True
2
proof
[(((triple6) -> rule8))]
("Bob" "is" "cold" "-")
((triple6) -> (rule8 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Dave is not smart.
False
2
inv-proof
[(((triple10) -> rule3))]
("Dave" "is" "smart" "-")
((triple10) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is cold.
True
4
proof
[(((((triple10) -> rule3) triple10) -> rule7))]
("Dave" "is" "cold" "+")
((((triple10) -> (rule3 % int2)) triple10) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is not cold.
False
4
inv-proof
[(((((triple10) -> rule3) triple10) -> rule7))]
("Dave" "is" "cold" "-")
((((triple10) -> (rule3 % int2)) triple10) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is big.
True
5
proof
[(((((((triple10) -> rule3) triple10) -> rule7)) -> rule2))]
("Dave" "is" "big" "+")
((((((triple10) -> (rule3 % int3)) triple10) -> (rule7 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is not big.
False
5
inv-proof
[(((((((triple10) -> rule3) triple10) -> rule7)) -> rule2))]
("Dave" "is" "big" "-")
((((((triple10) -> (rule3 % int3)) triple10) -> (rule7 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "nice" "-")
Anne is quiet.
Unknown
rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "quiet" "+")
Anne is not smart.
Unknown
inv-rconc
[@1: Anne is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "smart" "-")
Charlie is nice.
Unknown
rconc
[@2: Charlie is nice.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Charlie" "is" "nice" "+")
@0: Anne is nice.[(triple1)] Anne is white.[(triple2 OR ((triple1) -> rule5))] Bob is not big.[(triple3)] Bob is not furry.[(triple4)] Bob is quiet.[(triple5)] Bob is white.[(triple6)] Charlie is cold.[(triple7 OR ((((triple8) -> rule3) triple8) -> rule7))] Charlie is furry.[(triple8)] Charlie is quiet.[(triple9 OR ((triple8) -> rule4))] Dave is furry.[(triple10)] Dave is not white.[(triple12)] Dave is quiet.[(triple11 OR ((triple10) -> rule4))] @1: Anne is not cold.[(((triple2) -> rule8) OR ((((triple1) -> rule5)) -> rule8))] Bob is not cold.[(((triple6) -> rule8))] Charlie is big.[(((triple7) -> rule2) OR ((((((triple8) -> rule3) triple8) -> rule7)) -> rule2))] Charlie is smart.[(((triple8) -> rule3))] Dave is smart.[(((triple10) -> rule3))] @2: Dave is cold.[(((((triple10) -> rule3) triple10) -> rule7))] @3: Dave is big.[(((((((triple10) -> rule3) triple10) -> rule7)) -> rule2))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
((triple1) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Bob is not big.
("Bob" "is" "big" "-")
triple3
Bob is not furry.
("Bob" "is" "furry" "-")
triple4
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
Charlie is cold.
("Charlie" "is" "cold" "+")
triple7
((((triple8) -> (rule3 % int2)) triple8) -> (rule7 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple8
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple9
((triple8) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple10
Dave is not white.
("Dave" "is" "white" "-")
triple12
Dave is quiet.
("Dave" "is" "quiet" "+")
triple11
((triple10) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Anne is not cold.
("Anne" "is" "cold" "-")
((triple2) -> (rule8 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Bob is not cold.
("Bob" "is" "cold" "-")
((triple6) -> (rule8 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((triple7) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
((((((triple8) -> (rule3 % int3)) triple8) -> (rule7 % int2))) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple8) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple10) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((((triple10) -> (rule3 % int2)) triple10) -> (rule7 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((((triple10) -> (rule3 % int3)) triple10) -> (rule7 % int2))) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3