Anne is cold. Anne is furry. Anne is not green. Anne is kind. Anne is quiet. Anne is not white. Bob is furry. Bob is white. Charlie is not cold. Harry is not cold. Harry is furry. Harry is green. Harry is kind. Harry is not quiet. Harry is rough. All white things are cold. If Charlie is not white then Charlie is rough. If something is white and not cold then it is rough. All cold, white things are quiet. All kind, rough things are not quiet. If something is furry and not rough then it is kind. If something is quiet then it is not green. If something is rough and white then it is green.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is not green.
("Anne" "is" "green" "-")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is not white.
("Anne" "is" "white" "-")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is not cold.
("Charlie" "is" "cold" "-")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is not quiet.
("Harry" "is" "quiet" "-")
Harry is rough.
("Harry" "is" "rough" "+")
All white things are cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
If Charlie is not white then Charlie is rough.
((("Charlie" "is" "white" "~")) -> ("Charlie" "is" "rough" "+"))
If something is white and not cold then it is rough.
((("something" "is" "white" "+") ("something" "is" "cold" "~")) -> ("something" "is" "rough" "+"))
All cold, white things are quiet.
((("something" "is" "cold" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
All kind, rough things are not quiet.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "quiet" "-"))
If something is furry and not rough then it is kind.
((("something" "is" "furry" "+") ("something" "is" "rough" "~")) -> ("something" "is" "kind" "+"))
If something is quiet then it is not green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "-"))
If something is rough and white then it is green.
((("something" "is" "rough" "+") ("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
Anne is not white.
True
1
proof
[(triple6)]
("Anne" "is" "white" "-")
triple6
Harry is not furry.
False
1
inv-proof
[(triple11)]
("Harry" "is" "furry" "-")
triple11
Bob is cold.
True
2
proof
[(((triple8) -> rule1))]
("Bob" "is" "cold" "+")
((triple8) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not cold.
False
2
inv-proof
[(((triple8) -> rule1))]
("Bob" "is" "cold" "-")
((triple8) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
True
4
proof
[(((((triple8) -> rule1) triple8) -> rule4))]
("Bob" "is" "quiet" "+")
((((triple8) -> (rule1 % int2)) triple8) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not quiet.
False
4
inv-proof
[(((((triple8) -> rule1) triple8) -> rule4))]
("Bob" "is" "quiet" "-")
((((triple8) -> (rule1 % int2)) triple8) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not green.
True
5
proof
[(((((((triple8) -> rule1) triple8) -> rule4)) -> rule7))]
("Bob" "is" "green" "-")
((((((triple8) -> (rule1 % int3)) triple8) -> (rule4 % int2))) -> (rule7 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is green.
False
5
inv-proof
[(((((((triple8) -> rule1) triple8) -> rule4)) -> rule7))]
("Bob" "is" "green" "+")
((((((triple8) -> (rule1 % int3)) triple8) -> (rule4 % int2))) -> (rule7 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "green" "+")
Bob is not kind.
Unknown
inv-rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "kind" "-")
Charlie is kind.
Unknown
rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "kind" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Anne is cold.[(triple1)] Anne is furry.[(triple2)] Anne is kind.[(triple4)] Anne is not green.[(triple3 OR ((triple5) -> rule7))] Anne is not white.[(triple6)] Anne is quiet.[(triple5)] Bob is furry.[(triple7)] Bob is white.[(triple8)] Charlie is not cold.[(triple9)] Harry is furry.[(triple11)] Harry is green.[(triple12)] Harry is kind.[(triple13)] Harry is not cold.[(triple10)] Harry is not quiet.[(triple14 OR ((triple13 triple15) -> rule5))] Harry is rough.[(triple15)] @1: Bob is cold.[(((triple8) -> rule1))] @2: Bob is quiet.[(((((triple8) -> rule1) triple8) -> rule4))] @3: Bob is not green.[(((((((triple8) -> rule1) triple8) -> rule4)) -> rule7))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple4
Anne is not green.
("Anne" "is" "green" "-")
triple3
((triple5) -> (rule7 % int1))
Anne is not green.
("Anne" "is" "green" "-")
int1
Anne is not white.
("Anne" "is" "white" "-")
triple6
Anne is quiet.
("Anne" "is" "quiet" "+")
triple5
Bob is furry.
("Bob" "is" "furry" "+")
triple7
Bob is white.
("Bob" "is" "white" "+")
triple8
Charlie is not cold.
("Charlie" "is" "cold" "-")
triple9
Harry is furry.
("Harry" "is" "furry" "+")
triple11
Harry is green.
("Harry" "is" "green" "+")
triple12
Harry is kind.
("Harry" "is" "kind" "+")
triple13
Harry is not cold.
("Harry" "is" "cold" "-")
triple10
Harry is not quiet.
("Harry" "is" "quiet" "-")
triple14
((triple13 triple15) -> (rule5 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple15
Bob is cold.
("Bob" "is" "cold" "+")
((triple8) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple8) -> (rule1 % int2)) triple8) -> (rule4 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not green.
("Bob" "is" "green" "-")
((((((triple8) -> (rule1 % int3)) triple8) -> (rule4 % int2))) -> (rule7 % int1))
Bob is not green.
("Bob" "is" "green" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3