Anne is not round. Erin is big. Harry is blue. Furry people are quiet. If someone is blue and green then they are big. Blue, green people are big. If someone is blue then they are furry. If Harry is quiet and Harry is blue then Harry is not green. All quiet, big people are white.
Anne is not round.
("Anne" "is" "round" "-")
Erin is big.
("Erin" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Furry people are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
If someone is blue and green then they are big.
((("someone" "is" "blue" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
Blue, green people are big.
((("someone" "is" "blue" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If someone is blue then they are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
If Harry is quiet and Harry is blue then Harry is not green.
((("Harry" "is" "quiet" "+") ("Harry" "is" "blue" "+")) -> ("Harry" "is" "green" "-"))
All quiet, big people are white.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
Erin is big.
True
1
proof
[(triple2)]
("Erin" "is" "big" "+")
triple2
Anne is round.
False
1
inv-proof
[(triple1)]
("Anne" "is" "round" "+")
triple1
Harry is furry.
True
2
proof
[(((triple3) -> rule4))]
("Harry" "is" "furry" "+")
((triple3) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple3) -> rule4))]
("Harry" "is" "furry" "-")
((triple3) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is quiet.
True
3
proof
[(((((triple3) -> rule4)) -> rule1))]
("Harry" "is" "quiet" "+")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not quiet.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule1))]
("Harry" "is" "quiet" "-")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not green.
True
5
proof
[(((((((triple3) -> rule4)) -> rule1) triple3) -> rule5))]
("Harry" "is" "green" "-")
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2)) triple3) -> (rule5 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is green.
False
5
inv-proof
[(((((((triple3) -> rule4)) -> rule1) triple3) -> rule5))]
("Harry" "is" "green" "+")
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2)) triple3) -> (rule5 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Erin is not furry.
Unknown
inv-rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "furry" "-")
Harry is white.
Unknown
rconc
[@2: Harry is white.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Harry" "is" "white" "+")
Erin is not quiet.
Unknown
inv-rconc
[@2: Erin is quiet.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Erin" "is" "quiet" "-")
Anne is big.
Unknown
rconc
[@1: Anne is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "big" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Anne is blue.
Unknown
random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "+")
@0: Anne is not round.[(triple1)] Erin is big.[(triple2)] Harry is blue.[(triple3)] @1: Harry is furry.[(((triple3) -> rule4))] @2: Harry is quiet.[(((((triple3) -> rule4)) -> rule1))] @3: Harry is not green.[(((((((triple3) -> rule4)) -> rule1) triple3) -> rule5))]
Anne is not round.
("Anne" "is" "round" "-")
triple1
Erin is big.
("Erin" "is" "big" "+")
triple2
Harry is blue.
("Harry" "is" "blue" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
((triple3) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not green.
("Harry" "is" "green" "-")
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2)) triple3) -> (rule5 % int1))
Harry is not green.
("Harry" "is" "green" "-")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3