Anne is kind. Bob is red. Charlie is not furry. Harry is not white. If Charlie is kind then Charlie is not furry. If Anne is blue then Anne is big. Kind things are white. All quiet things are white. Furry, red things are big. All white things are not big. If Bob is red and Bob is not furry then Bob is not big. If Charlie is red and Charlie is not kind then Charlie is blue.
Anne is kind.
("Anne" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Charlie is not furry.
("Charlie" "is" "furry" "-")
Harry is not white.
("Harry" "is" "white" "-")
If Charlie is kind then Charlie is not furry.
((("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "furry" "-"))
If Anne is blue then Anne is big.
((("Anne" "is" "blue" "+")) -> ("Anne" "is" "big" "+"))
Kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
All quiet things are white.
((("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
Furry, red things are big.
((("something" "is" "furry" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
All white things are not big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "-"))
If Bob is red and Bob is not furry then Bob is not big.
((("Bob" "is" "red" "+") ("Bob" "is" "furry" "~")) -> ("Bob" "is" "big" "-"))
If Charlie is red and Charlie is not kind then Charlie is blue.
((("Charlie" "is" "red" "+") ("Charlie" "is" "kind" "~")) -> ("Charlie" "is" "blue" "+"))
Harry is not white.
True
1
proof
[(triple4)]
("Harry" "is" "white" "-")
triple4
Charlie is furry.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "furry" "+")
triple3
Anne is white.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "white" "+")
((triple1) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not white.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "white" "-")
((triple1) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not big.
True
3
proof
[(((((triple1) -> rule3)) -> rule6))]
("Anne" "is" "big" "-")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is big.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule6))]
("Anne" "is" "big" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "white" "-")
Bob is white.
Unknown
rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "white" "+")
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "big" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Anne is kind.[(triple1)] Bob is red.[(triple2)] Charlie is not furry.[(triple3)] Harry is not white.[(triple4)] @1: Anne is white.[(((triple1) -> rule3))] @2: Anne is not big.[(((((triple1) -> rule3)) -> rule6))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Bob is red.
("Bob" "is" "red" "+")
triple2
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple3
Harry is not white.
("Harry" "is" "white" "-")
triple4
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not big.
("Anne" "is" "big" "-")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2