Anne is young. Smart things are quiet. If something is smart and green then it is blue. If Anne is young and Anne is kind then Anne is smart. If something is young then it is quiet. If something is young then it is round. All kind, blue things are round. If Anne is green then Anne is round. If something is quiet and young then it is kind.
Anne is young.
("Anne" "is" "young" "+")
Smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
If something is smart and green then it is blue.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If Anne is young and Anne is kind then Anne is smart.
((("Anne" "is" "young" "+") ("Anne" "is" "kind" "+")) -> ("Anne" "is" "smart" "+"))
If something is young then it is quiet.
((("something" "is" "young" "+")) -> ("something" "is" "quiet" "+"))
If something is young then it is round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
All kind, blue things are round.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If Anne is green then Anne is round.
((("Anne" "is" "green" "+")) -> ("Anne" "is" "round" "+"))
If something is quiet and young then it is kind.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
Anne is young.
True
1
proof
[(triple1)]
("Anne" "is" "young" "+")
triple1
Anne is not young.
False
1
inv-proof
[(triple1)]
("Anne" "is" "young" "-")
triple1
Anne is quiet.
True
2
proof
[(((triple1) -> rule4))]
("Anne" "is" "quiet" "+")
((triple1) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is not round.
False
2
inv-proof
[(((triple1) -> rule5))]
("Anne" "is" "round" "-")
((triple1) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
True
4
proof
[(((((triple1) -> rule4) triple1) -> rule8))]
("Anne" "is" "kind" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not kind.
False
4
inv-proof
[(((((triple1) -> rule4) triple1) -> rule8))]
("Anne" "is" "kind" "-")
((((triple1) -> (rule4 % int2)) triple1) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
True
6
proof
[(((triple1 ((((triple1) -> rule4) triple1) -> rule8)) -> rule3))]
("Anne" "is" "smart" "+")
((triple1 ((((triple1) -> (rule4 % int3)) triple1) -> (rule8 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is not smart.
False
6
inv-proof
[(((triple1 ((((triple1) -> rule4) triple1) -> rule8)) -> rule3))]
("Anne" "is" "smart" "-")
((triple1 ((((triple1) -> (rule4 % int3)) triple1) -> (rule8 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "blue" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is young.[(triple1)] @1: Anne is quiet.[(((triple1) -> rule4))] Anne is round.[(((triple1) -> rule5))] @2: Anne is kind.[(((((triple1) -> rule4) triple1) -> rule8))] @3: Anne is smart.[(((triple1 ((((triple1) -> rule4) triple1) -> rule8)) -> rule3))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule4 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule8 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
((triple1 ((((triple1) -> (rule4 % int3)) triple1) -> (rule8 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3