Anne is nice. Anne is quiet. Anne is white. Bob is blue. Bob is not rough. Charlie is nice. Charlie is rough. All blue people are quiet. Rough people are not quiet. Quiet people are white. If someone is quiet and white then they are nice. If Charlie is white then Charlie is not furry. If Charlie is quiet and Charlie is not white then Charlie is not nice.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is not rough.
("Bob" "is" "rough" "-")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
All blue people are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
Rough people are not quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "-"))
Quiet people are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If someone is quiet and white then they are nice.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
If Charlie is white then Charlie is not furry.
((("Charlie" "is" "white" "+")) -> ("Charlie" "is" "furry" "-"))
If Charlie is quiet and Charlie is not white then Charlie is not nice.
((("Charlie" "is" "quiet" "+") ("Charlie" "is" "white" "~")) -> ("Charlie" "is" "nice" "-"))
Bob is blue.
True
1
proof
[(triple4)]
("Bob" "is" "blue" "+")
triple4
Anne is not white.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule3))]
("Anne" "is" "white" "-")
triple3
((triple2) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Bob is quiet.
True
2
proof
[(((triple4) -> rule1))]
("Bob" "is" "quiet" "+")
((triple4) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Charlie is quiet.
False
2
inv-proof
[(((triple7) -> rule2))]
("Charlie" "is" "quiet" "+")
((triple7) -> (rule2 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Bob is white.
True
3
proof
[(((((triple4) -> rule1)) -> rule3))]
("Bob" "is" "white" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not white.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule3))]
("Bob" "is" "white" "-")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is nice.
True
6
proof
[(((((triple4) -> rule1) ((((triple4) -> rule1)) -> rule3)) -> rule4))]
("Bob" "is" "nice" "+")
((((triple4) -> (rule1 % int3)) ((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is not nice.
False
6
inv-proof
[(((((triple4) -> rule1) ((((triple4) -> rule1)) -> rule3)) -> rule4))]
("Bob" "is" "nice" "-")
((((triple4) -> (rule1 % int3)) ((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "white" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Anne is nice.[(triple1 OR ((triple2 triple3) -> rule4) OR ((triple2 ((triple2) -> rule3)) -> rule4))] Anne is quiet.[(triple2)] Anne is white.[(triple3 OR ((triple2) -> rule3))] Bob is blue.[(triple4)] Bob is not rough.[(triple5)] Charlie is nice.[(triple6)] Charlie is rough.[(triple7)] @1: Bob is quiet.[(((triple4) -> rule1))] Charlie is not quiet.[(((triple7) -> rule2))] @2: Bob is white.[(((((triple4) -> rule1)) -> rule3))] @3: Bob is nice.[(((((triple4) -> rule1) ((((triple4) -> rule1)) -> rule3)) -> rule4))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
((triple2 triple3) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((triple2 ((triple2) -> (rule3 % int2))) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
((triple2) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
triple4
Bob is not rough.
("Bob" "is" "rough" "-")
triple5
Charlie is nice.
("Charlie" "is" "nice" "+")
triple6
Charlie is rough.
("Charlie" "is" "rough" "+")
triple7
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple4) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
((triple7) -> (rule2 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Bob is white.
("Bob" "is" "white" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
((((triple4) -> (rule1 % int3)) ((((triple4) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3