Anne is not big. Anne is quiet. Anne is not young. Erin is not big. Erin is green. Harry is furry. Harry is not green. If something is furry then it is quiet. If something is furry then it is quiet. White things are young. If something is white then it is furry. Green things are white. White things are green. If something is white and not big then it is green. If Harry is white then Harry is green.
Anne is not big.
("Anne" "is" "big" "-")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is not young.
("Anne" "is" "young" "-")
Erin is not big.
("Erin" "is" "big" "-")
Erin is green.
("Erin" "is" "green" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is not green.
("Harry" "is" "green" "-")
If something is furry then it is quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
If something is furry then it is quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
White things are young.
((("something" "is" "white" "+")) -> ("something" "is" "young" "+"))
If something is white then it is furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
Green things are white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
White things are green.
((("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
If something is white and not big then it is green.
((("something" "is" "white" "+") ("something" "is" "big" "~")) -> ("something" "is" "green" "+"))
If Harry is white then Harry is green.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "green" "+"))
Erin is not big.
True
1
proof
[(triple4)]
("Erin" "is" "big" "-")
triple4
Harry is green.
False
1
inv-proof
[(triple7)]
("Harry" "is" "green" "+")
triple7
Erin is white.
True
2
proof
[(((triple5) -> rule5))]
("Erin" "is" "white" "+")
((triple5) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is not white.
False
2
inv-proof
[(((triple5) -> rule5))]
("Erin" "is" "white" "-")
((triple5) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is young.
True
3
proof
[(((((triple5) -> rule5)) -> rule3))]
("Erin" "is" "young" "+")
((((triple5) -> (rule5 % int2))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is not young.
False
3
inv-proof
[(((((triple5) -> rule5)) -> rule3))]
("Erin" "is" "young" "-")
((((triple5) -> (rule5 % int2))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is quiet.
True
4
proof
[(((((((triple5) -> rule5)) -> rule4)) -> rule1) OR ((((((triple5) -> rule5)) -> rule4)) -> rule2))]
("Erin" "is" "quiet" "+")
((((((triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
((((((triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is not quiet.
False
4
inv-proof
[(((((((triple5) -> rule5)) -> rule4)) -> rule1) OR ((((((triple5) -> rule5)) -> rule4)) -> rule2))]
("Erin" "is" "quiet" "-")
((((((triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
((((((triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Harry is not white.
Unknown
inv-rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "white" "-")
Anne is white.
Unknown
rconc
[@2: Anne is white.[CWA. Example of deepest failure = (rule5 <- rule6 <- FAIL)]]
("Anne" "is" "white" "+")
Anne is not green.
Unknown
inv-rconc
[@3: Anne is green.[CWA. Example of deepest failure = (rule6 <- rule5 <- rule7 <- FAIL)]]
("Anne" "is" "green" "-")
Harry is young.
Unknown
rconc
[@2: Harry is young.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Harry" "is" "young" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Anne is not big.[(triple1)] Anne is not young.[(triple3)] Anne is quiet.[(triple2)] Erin is green.[(triple5)] Erin is not big.[(triple4)] Harry is furry.[(triple6)] Harry is not green.[(triple7)] @1: Erin is white.[(((triple5) -> rule5))] Harry is quiet.[(((triple6) -> rule1) OR ((triple6) -> rule2))] @2: Erin is furry.[(((((triple5) -> rule5)) -> rule4))] Erin is young.[(((((triple5) -> rule5)) -> rule3))] @3: Erin is quiet.[(((((((triple5) -> rule5)) -> rule4)) -> rule1) OR ((((((triple5) -> rule5)) -> rule4)) -> rule2))]
Anne is not big.
("Anne" "is" "big" "-")
triple1
Anne is not young.
("Anne" "is" "young" "-")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Erin is green.
("Erin" "is" "green" "+")
triple5
Erin is not big.
("Erin" "is" "big" "-")
triple4
Harry is furry.
("Harry" "is" "furry" "+")
triple6
Harry is not green.
("Harry" "is" "green" "-")
triple7
Erin is white.
("Erin" "is" "white" "+")
((triple5) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple6) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((triple6) -> (rule2 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((((triple5) -> (rule5 % int2))) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((((triple5) -> (rule5 % int2))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((((((triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
((((((triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3