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