Anne is rough. Bob is smart. Gary is white. Harry is furry. All white, rough things are blue. Rough, kind things are white. Furry, white things are not green. All furry things are not rough. If Gary is kind then Gary is white. If something is rough then it is kind. If Anne is rough and Anne is blue then Anne is smart. If Harry is green and Harry is not white then Harry is smart.
Anne is rough.
("Anne" "is" "rough" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is furry.
("Harry" "is" "furry" "+")
All white, rough things are blue.
((("something" "is" "white" "+") ("something" "is" "rough" "+")) -> ("something" "is" "blue" "+"))
Rough, kind things are white.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Furry, white things are not green.
((("something" "is" "furry" "+") ("something" "is" "white" "+")) -> ("something" "is" "green" "-"))
All furry things are not rough.
((("something" "is" "furry" "+")) -> ("something" "is" "rough" "-"))
If Gary is kind then Gary is white.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "white" "+"))
If something is rough then it is kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If Anne is rough and Anne is blue then Anne is smart.
((("Anne" "is" "rough" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "smart" "+"))
If Harry is green and Harry is not white then Harry is smart.
((("Harry" "is" "green" "+") ("Harry" "is" "white" "~")) -> ("Harry" "is" "smart" "+"))
Anne is rough.
True
1
proof
[(triple1)]
("Anne" "is" "rough" "+")
triple1
Gary is not white.
False
1
inv-proof
[(triple3)]
("Gary" "is" "white" "-")
triple3
Anne is kind.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "kind" "+")
((triple1) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Harry is rough.
False
2
inv-proof
[(((triple4) -> rule4))]
("Harry" "is" "rough" "+")
((triple4) -> (rule4 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Anne is white.
True
4
proof
[(((triple1 ((triple1) -> rule6)) -> rule2))]
("Anne" "is" "white" "+")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is not white.
False
4
inv-proof
[(((triple1 ((triple1) -> rule6)) -> rule2))]
("Anne" "is" "white" "-")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is blue.
True
6
proof
[(((((triple1 ((triple1) -> rule6)) -> rule2) triple1) -> rule1))]
("Anne" "is" "blue" "+")
((((triple1 ((triple1) -> (rule6 % int3))) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is not blue.
False
6
inv-proof
[(((((triple1 ((triple1) -> rule6)) -> rule2) triple1) -> rule1))]
("Anne" "is" "blue" "-")
((((triple1 ((triple1) -> (rule6 % int3))) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Harry" "is" "smart" "-")
Harry is white.
Unknown
rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "white" "+")
Harry is not blue.
Unknown
inv-rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "blue" "-")
Gary is kind.
Unknown
rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "kind" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
@0: Anne is rough.[(triple1)] Bob is smart.[(triple2)] Gary is white.[(triple3)] Harry is furry.[(triple4)] @1: Anne is kind.[(((triple1) -> rule6))] Harry is not rough.[(((triple4) -> rule4))] @2: Anne is white.[(((triple1 ((triple1) -> rule6)) -> rule2))] @3: Anne is blue.[(((((triple1 ((triple1) -> rule6)) -> rule2) triple1) -> rule1))] @4: Anne is smart.[(((triple1 ((((triple1 ((triple1) -> rule6)) -> rule2) triple1) -> rule1)) -> rule7))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Gary is white.
("Gary" "is" "white" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Harry is not rough.
("Harry" "is" "rough" "-")
((triple4) -> (rule4 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1 ((triple1) -> (rule6 % int3))) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
((triple1 ((((triple1 ((triple1) -> (rule6 % int4))) -> (rule2 % int3)) triple1) -> (rule1 % int2))) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4