Anne is nice. Bob is not furry. Dave is round. All kind things are green. If something is green then it is quiet. If Bob is green then Bob is kind. If something is kind then it is not cold. All quiet, kind things are nice. All nice things are kind. If Anne is not kind then Anne is round. If Anne is green and Anne is cold then Anne is round.
Anne is nice.
("Anne" "is" "nice" "+")
Bob is not furry.
("Bob" "is" "furry" "-")
Dave is round.
("Dave" "is" "round" "+")
All kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If something is green then it is quiet.
((("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
If Bob is green then Bob is kind.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "kind" "+"))
If something is kind then it is not cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "-"))
All quiet, kind things are nice.
((("something" "is" "quiet" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
All nice things are kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
If Anne is not kind then Anne is round.
((("Anne" "is" "kind" "~")) -> ("Anne" "is" "round" "+"))
If Anne is green and Anne is cold then Anne is round.
((("Anne" "is" "green" "+") ("Anne" "is" "cold" "+")) -> ("Anne" "is" "round" "+"))
Dave is round.
True
1
proof
[(triple3)]
("Dave" "is" "round" "+")
triple3
Anne is not nice.
False
1
inv-proof
[(triple1)]
("Anne" "is" "nice" "-")
triple1
Anne is kind.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "kind" "+")
((triple1) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not kind.
False
2
inv-proof
[(((triple1) -> rule6))]
("Anne" "is" "kind" "-")
((triple1) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not cold.
True
3
proof
[(((((triple1) -> rule6)) -> rule4))]
("Anne" "is" "cold" "-")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is not green.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule1))]
("Anne" "is" "green" "-")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is quiet.
True
4
proof
[(((((((triple1) -> rule6)) -> rule1)) -> rule2))]
("Anne" "is" "quiet" "+")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is not quiet.
False
4
inv-proof
[(((((((triple1) -> rule6)) -> rule1)) -> rule2))]
("Anne" "is" "quiet" "-")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Dave is not nice.
Unknown
inv-rconc
[@2: Dave is nice.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Dave" "is" "nice" "-")
Bob is green.
Unknown
rconc
[@4: Bob is green.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule5 <- rule2 <- FAIL)]]
("Bob" "is" "green" "+")
Bob is not kind.
Unknown
inv-rconc
[@4: Bob is kind.[CWA. Example of deepest failure = (rule3 <- rule1 <- rule6 <- rule5 <- FAIL)]]
("Bob" "is" "kind" "-")
Bob is nice.
Unknown
rconc
[@4: Bob is nice.[CWA. Example of deepest failure = (rule5 <- rule2 <- rule1 <- rule3 <- FAIL)]]
("Bob" "is" "nice" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Anne is nice.[(triple1)] Bob is not furry.[(triple2)] Dave is round.[(triple3)] @1: Anne is kind.[(((triple1) -> rule6))] @2: Anne is green.[(((((triple1) -> rule6)) -> rule1))] Anne is not cold.[(((((triple1) -> rule6)) -> rule4))] @3: Anne is quiet.[(((((((triple1) -> rule6)) -> rule1)) -> rule2))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Bob is not furry.
("Bob" "is" "furry" "-")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is not cold.
("Anne" "is" "cold" "-")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3