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