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