Anne is kind. Anne is nice. Charlie is not kind. Erin is nice. Harry is kind. Harry is not quiet. Harry is not red. If Harry is green and Harry is kind then Harry is not round. If someone is red and nice then they are quiet. Nice people are green. Kind, quiet people are green. If Erin is green then Erin is red. Quiet people are round. If someone is round then they are kind.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Charlie is not kind.
("Charlie" "is" "kind" "-")
Erin is nice.
("Erin" "is" "nice" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is not quiet.
("Harry" "is" "quiet" "-")
Harry is not red.
("Harry" "is" "red" "-")
If Harry is green and Harry is kind then Harry is not round.
((("Harry" "is" "green" "+") ("Harry" "is" "kind" "+")) -> ("Harry" "is" "round" "-"))
If someone is red and nice then they are quiet.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
Nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
Kind, quiet people are green.
((("someone" "is" "kind" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
If Erin is green then Erin is red.
((("Erin" "is" "green" "+")) -> ("Erin" "is" "red" "+"))
Quiet people are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If someone is round then they are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
Charlie is not kind.
True
1
proof
[(triple3)]
("Charlie" "is" "kind" "-")
triple3
Harry is not kind.
False
1
inv-proof
[(triple5)]
("Harry" "is" "kind" "-")
triple5
Anne is green.
True
2
proof
[(((triple2) -> rule3))]
("Anne" "is" "green" "+")
((triple2) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple4) -> rule3))]
("Erin" "is" "green" "-")
((triple4) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
True
3
proof
[(((((triple4) -> rule3)) -> rule5))]
("Erin" "is" "red" "+")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is not red.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule5))]
("Erin" "is" "red" "-")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is quiet.
True
5
proof
[(((((((triple4) -> rule3)) -> rule5) triple4) -> rule2))]
("Erin" "is" "quiet" "+")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is not quiet.
False
5
inv-proof
[(((((((triple4) -> rule3)) -> rule5) triple4) -> rule2))]
("Erin" "is" "quiet" "-")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is round.
True
6
proof
[(((((((((triple4) -> rule3)) -> rule5) triple4) -> rule2)) -> rule6))]
("Erin" "is" "round" "+")
((((((((triple4) -> (rule3 % int4))) -> (rule5 % int3)) triple4) -> (rule2 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is not round.
False
6
inv-proof
[(((((((((triple4) -> rule3)) -> rule5) triple4) -> rule2)) -> rule6))]
("Erin" "is" "round" "-")
((((((((triple4) -> (rule3 % int4))) -> (rule5 % int3)) triple4) -> (rule2 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is kind.
True
7
proof
[(((((((((((triple4) -> rule3)) -> rule5) triple4) -> rule2)) -> rule6)) -> rule7))]
("Erin" "is" "kind" "+")
((((((((((triple4) -> (rule3 % int5))) -> (rule5 % int4)) triple4) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
Erin is green.
("Erin" "is" "green" "+")
int5
Erin is not kind.
False
7
inv-proof
[(((((((((((triple4) -> rule3)) -> rule5) triple4) -> rule2)) -> rule6)) -> rule7))]
("Erin" "is" "kind" "-")
((((((((((triple4) -> (rule3 % int5))) -> (rule5 % int4)) triple4) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
Erin is green.
("Erin" "is" "green" "+")
int5
Harry is not round.
Unknown
inv-rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "round" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "green" "+")
Charlie is not round.
Unknown
inv-rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Charlie" "is" "round" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Anne is quiet.
Unknown
rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "quiet" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
Erin is not furry.
Unknown
inv-random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "-")
Anne is furry.
Unknown
random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Anne is kind.[(triple1)] Anne is nice.[(triple2)] Charlie is not kind.[(triple3)] Erin is nice.[(triple4)] Harry is kind.[(triple5)] Harry is not quiet.[(triple6)] Harry is not red.[(triple7)] @1: Anne is green.[(((triple2) -> rule3))] Erin is green.[(((triple4) -> rule3))] @2: Erin is red.[(((((triple4) -> rule3)) -> rule5))] @3: Erin is quiet.[(((((((triple4) -> rule3)) -> rule5) triple4) -> rule2))] @4: Erin is round.[(((((((((triple4) -> rule3)) -> rule5) triple4) -> rule2)) -> rule6))] @5: Erin is kind.[(((((((((((triple4) -> rule3)) -> rule5) triple4) -> rule2)) -> rule6)) -> rule7))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Charlie is not kind.
("Charlie" "is" "kind" "-")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Harry is kind.
("Harry" "is" "kind" "+")
triple5
Harry is not quiet.
("Harry" "is" "quiet" "-")
triple6
Harry is not red.
("Harry" "is" "red" "-")
triple7
Anne is green.
("Anne" "is" "green" "+")
((triple2) -> (rule3 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple4) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
((((((triple4) -> (rule3 % int3))) -> (rule5 % int2)) triple4) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
((((((((triple4) -> (rule3 % int4))) -> (rule5 % int3)) triple4) -> (rule2 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Erin is kind.
("Erin" "is" "kind" "+")
((((((((((triple4) -> (rule3 % int5))) -> (rule5 % int4)) triple4) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
int4
Erin is green.
("Erin" "is" "green" "+")
int5