Anne is green. Anne is not round. Bob is cold. Bob is round. Dave is round. Gary is nice. Gary is not quiet. Round things are not kind. All white, cold things are quiet. If Bob is not kind then Bob is white.
Anne is green.
("Anne" "is" "green" "+")
Anne is not round.
("Anne" "is" "round" "-")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is not quiet.
("Gary" "is" "quiet" "-")
Round things are not kind.
((("something" "is" "round" "+")) -> ("something" "is" "kind" "-"))
All white, cold things are quiet.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
If Bob is not kind then Bob is white.
((("Bob" "is" "kind" "~")) -> ("Bob" "is" "white" "+"))
Dave is round.
True
1
proof
[(triple5)]
("Dave" "is" "round" "+")
triple5
Gary is quiet.
False
1
inv-proof
[(triple7)]
("Gary" "is" "quiet" "+")
triple7
Bob is not kind.
True
2
proof
[(((triple4) -> rule1))]
("Bob" "is" "kind" "-")
((triple4) -> (rule1 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Bob is kind.
False
2
inv-proof
[(((triple4) -> rule1))]
("Bob" "is" "kind" "+")
((triple4) -> (rule1 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
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 not kind.
("Bob" "is" "kind" "-")
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 not kind.
("Bob" "is" "kind" "-")
int2
Bob is quiet.
True
5
proof
[(((((((triple4) -> rule1)) -> rule3) triple3) -> rule2))]
("Bob" "is" "quiet" "+")
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not kind.
("Bob" "is" "kind" "-")
int3
Bob is not quiet.
False
5
inv-proof
[(((((((triple4) -> rule1)) -> rule3) triple3) -> rule2))]
("Bob" "is" "quiet" "-")
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not kind.
("Bob" "is" "kind" "-")
int3
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "quiet" "-")
Dave is quiet.
Unknown
rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "quiet" "+")
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is green.[(triple1)] Anne is not round.[(triple2)] Bob is cold.[(triple3)] Bob is round.[(triple4)] Dave is round.[(triple5)] Gary is nice.[(triple6)] Gary is not quiet.[(triple7)] @1: Bob is not kind.[(((triple4) -> rule1))] Dave is not kind.[(((triple5) -> rule1))] @2: Bob is white.[(((((triple4) -> rule1)) -> rule3))] @3: Bob is quiet.[(((((((triple4) -> rule1)) -> rule3) triple3) -> rule2))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is not round.
("Anne" "is" "round" "-")
triple2
Bob is cold.
("Bob" "is" "cold" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
Gary is nice.
("Gary" "is" "nice" "+")
triple6
Gary is not quiet.
("Gary" "is" "quiet" "-")
triple7
Bob is not kind.
("Bob" "is" "kind" "-")
((triple4) -> (rule1 % int1))
Bob is not kind.
("Bob" "is" "kind" "-")
int1
Dave is not kind.
("Dave" "is" "kind" "-")
((triple5) -> (rule1 % int1))
Dave is not kind.
("Dave" "is" "kind" "-")
int1
Bob is white.
("Bob" "is" "white" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not kind.
("Bob" "is" "kind" "-")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((((((triple4) -> (rule1 % int3))) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not kind.
("Bob" "is" "kind" "-")
int3