Anne is furry. Anne is smart. Anne is young. Dave is not furry. Dave is green. Dave is not quiet. Dave is not young. Erin is rough. Harry is blue. Harry is furry. All rough, quiet things are young. If something is young then it is not blue. All rough things are quiet.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is green.
("Dave" "is" "green" "+")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Dave is not young.
("Dave" "is" "young" "-")
Erin is rough.
("Erin" "is" "rough" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
All rough, quiet things are young.
((("something" "is" "rough" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
If something is young then it is not blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "-"))
All rough things are quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
Anne is smart.
True
1
proof
[(triple2)]
("Anne" "is" "smart" "+")
triple2
Erin is not rough.
False
1
inv-proof
[(triple8)]
("Erin" "is" "rough" "-")
triple8
Anne is not blue.
True
2
proof
[(((triple3) -> rule2))]
("Anne" "is" "blue" "-")
((triple3) -> (rule2 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
Anne is blue.
False
2
inv-proof
[(((triple3) -> rule2))]
("Anne" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
Erin is young.
True
4
proof
[(((triple8 ((triple8) -> rule3)) -> rule1))]
("Erin" "is" "young" "+")
((triple8 ((triple8) -> (rule3 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is not young.
False
4
inv-proof
[(((triple8 ((triple8) -> rule3)) -> rule1))]
("Erin" "is" "young" "-")
((triple8 ((triple8) -> (rule3 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is not blue.
True
5
proof
[(((((triple8 ((triple8) -> rule3)) -> rule1)) -> rule2))]
("Erin" "is" "blue" "-")
((((triple8 ((triple8) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is blue.
False
5
inv-proof
[(((((triple8 ((triple8) -> rule3)) -> rule1)) -> rule2))]
("Erin" "is" "blue" "+")
((((triple8 ((triple8) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "quiet" "-")
Harry is young.
Unknown
rconc
[@1: Harry is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "young" "+")
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "quiet" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
Anne is not green.
Unknown
inv-random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
@0: Anne is furry.[(triple1)] Anne is smart.[(triple2)] Anne is young.[(triple3)] Dave is green.[(triple5)] Dave is not furry.[(triple4)] Dave is not quiet.[(triple6)] Dave is not young.[(triple7)] Erin is rough.[(triple8)] Harry is blue.[(triple9)] Harry is furry.[(triple10)] @1: Anne is not blue.[(((triple3) -> rule2))] Erin is quiet.[(((triple8) -> rule3))] @2: Erin is young.[(((triple8 ((triple8) -> rule3)) -> rule1))] @3: Erin is not blue.[(((((triple8 ((triple8) -> rule3)) -> rule1)) -> rule2))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
Dave is green.
("Dave" "is" "green" "+")
triple5
Dave is not furry.
("Dave" "is" "furry" "-")
triple4
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple6
Dave is not young.
("Dave" "is" "young" "-")
triple7
Erin is rough.
("Erin" "is" "rough" "+")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is furry.
("Harry" "is" "furry" "+")
triple10
Anne is not blue.
("Anne" "is" "blue" "-")
((triple3) -> (rule2 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple8) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple8 ((triple8) -> (rule3 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is not blue.
("Erin" "is" "blue" "-")
((((triple8 ((triple8) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3