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