Anne is kind. Anne is rough. Charlie is kind. Charlie is rough. Charlie is smart. Erin is not kind. Erin is not young. Gary is nice. Gary is quiet. Gary is smart. Young, kind people are nice. If someone is nice and kind then they are quiet. If Gary is nice and Gary is quiet then Gary is kind. Rough people are red. If Charlie is smart and Charlie is rough then Charlie is quiet. If someone is red and rough then they are young. If someone is quiet then they are smart. If Erin is smart then Erin is rough.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is not kind.
("Erin" "is" "kind" "-")
Erin is not young.
("Erin" "is" "young" "-")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Young, kind people are nice.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice and kind then they are quiet.
((("someone" "is" "nice" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "+"))
If Gary is nice and Gary is quiet then Gary is kind.
((("Gary" "is" "nice" "+") ("Gary" "is" "quiet" "+")) -> ("Gary" "is" "kind" "+"))
Rough people are red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If Charlie is smart and Charlie is rough then Charlie is quiet.
((("Charlie" "is" "smart" "+") ("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "quiet" "+"))
If someone is red and rough then they are young.
((("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If someone is quiet then they are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
If Erin is smart then Erin is rough.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "rough" "+"))
Gary is nice.
True
1
proof
[(triple8)]
("Gary" "is" "nice" "+")
triple8
Gary is not nice.
False
1
inv-proof
[(triple8)]
("Gary" "is" "nice" "-")
triple8
Charlie is red.
True
2
proof
[(((triple4) -> rule4))]
("Charlie" "is" "red" "+")
((triple4) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is not quiet.
False
3
inv-proof
[(((triple5 triple4) -> rule5) OR ((((((((triple4) -> rule4) triple4) -> rule6) triple3) -> rule1) triple3) -> rule2))]
("Charlie" "is" "quiet" "-")
((triple5 triple4) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((((((triple4) -> (rule4 % int4)) triple4) -> (rule6 % int3)) triple3) -> (rule1 % int2)) triple3) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
Anne is young.
True
4
proof
[(((((triple2) -> rule4) triple2) -> rule6))]
("Anne" "is" "young" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is not young.
False
4
inv-proof
[(((((triple2) -> rule4) triple2) -> rule6))]
("Anne" "is" "young" "-")
((((triple2) -> (rule4 % int2)) triple2) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is nice.
True
6
proof
[(((((((triple2) -> rule4) triple2) -> rule6) triple1) -> rule1))]
("Anne" "is" "nice" "+")
((((((triple2) -> (rule4 % int3)) triple2) -> (rule6 % int2)) triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is not nice.
False
6
inv-proof
[(((((((triple2) -> rule4) triple2) -> rule6) triple1) -> rule1))]
("Anne" "is" "nice" "-")
((((((triple2) -> (rule4 % int3)) triple2) -> (rule6 % int2)) triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is quiet.
True
8
proof
[(((((((((triple2) -> rule4) triple2) -> rule6) triple1) -> rule1) triple1) -> rule2))]
("Anne" "is" "quiet" "+")
((((((((triple2) -> (rule4 % int4)) triple2) -> (rule6 % int3)) triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is not quiet.
False
8
inv-proof
[(((((((((triple2) -> rule4) triple2) -> rule6) triple1) -> rule1) triple1) -> rule2))]
("Anne" "is" "quiet" "-")
((((((((triple2) -> (rule4 % int4)) triple2) -> (rule6 % int3)) triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is smart.
True
9
proof
[(((((((((((triple2) -> rule4) triple2) -> rule6) triple1) -> rule1) triple1) -> rule2)) -> rule7))]
("Anne" "is" "smart" "+")
((((((((((triple2) -> (rule4 % int5)) triple2) -> (rule6 % int4)) triple1) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is red.
("Anne" "is" "red" "+")
int5
Anne is not smart.
False
9
inv-proof
[(((((((((((triple2) -> rule4) triple2) -> rule6) triple1) -> rule1) triple1) -> rule2)) -> rule7))]
("Anne" "is" "smart" "-")
((((((((((triple2) -> (rule4 % int5)) triple2) -> (rule6 % int4)) triple1) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is red.
("Anne" "is" "red" "+")
int5
Erin is not nice.
Unknown
inv-rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "nice" "-")
Erin is rough.
Unknown
rconc
[@3: Erin is rough.[CWA. Example of deepest failure = (rule8 <- rule7 <- rule2 <- FAIL)]]
("Erin" "is" "rough" "+")
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "quiet" "-")
Gary is young.
Unknown
rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "young" "+")
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "red" "-")
Erin is red.
Unknown
rconc
[@4: Erin is red.[CWA. Example of deepest failure = (rule4 <- rule8 <- rule7 <- rule2 <- FAIL)]]
("Erin" "is" "red" "+")
@0: Anne is kind.[(triple1)] Anne is rough.[(triple2)] Charlie is kind.[(triple3)] Charlie is rough.[(triple4)] Charlie is smart.[(triple5 OR ((((((((((triple4) -> rule4) triple4) -> rule6) triple3) -> rule1) triple3) -> rule2)) -> rule7))] Erin is not kind.[(triple6)] Erin is not young.[(triple7)] Gary is nice.[(triple8)] Gary is quiet.[(triple9)] Gary is smart.[(triple10 OR ((triple9) -> rule7))] @1: Anne is red.[(((triple2) -> rule4))] Charlie is quiet.[(((triple5 triple4) -> rule5) OR ((((((((triple4) -> rule4) triple4) -> rule6) triple3) -> rule1) triple3) -> rule2))] Charlie is red.[(((triple4) -> rule4))] Gary is kind.[(((triple8 triple9) -> rule3))] @2: Anne is young.[(((((triple2) -> rule4) triple2) -> rule6))] Charlie is young.[(((((triple4) -> rule4) triple4) -> rule6))] @3: Anne is nice.[(((((((triple2) -> rule4) triple2) -> rule6) triple1) -> rule1))] Charlie is nice.[(((((((triple4) -> rule4) triple4) -> rule6) triple3) -> rule1))] @4: Anne is quiet.[(((((((((triple2) -> rule4) triple2) -> rule6) triple1) -> rule1) triple1) -> rule2))] @5: Anne is smart.[(((((((((((triple2) -> rule4) triple2) -> rule6) triple1) -> rule1) triple1) -> rule2)) -> rule7))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
((((((((((triple4) -> (rule4 % int5)) triple4) -> (rule6 % int4)) triple3) -> (rule1 % int3)) triple3) -> (rule2 % int2))) -> (rule7 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is red.
("Charlie" "is" "red" "+")
int5
Erin is not kind.
("Erin" "is" "kind" "-")
triple6
Erin is not young.
("Erin" "is" "young" "-")
triple7
Gary is nice.
("Gary" "is" "nice" "+")
triple8
Gary is quiet.
("Gary" "is" "quiet" "+")
triple9
Gary is smart.
("Gary" "is" "smart" "+")
triple10
((triple9) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((triple2) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple5 triple4) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((((((triple4) -> (rule4 % int4)) triple4) -> (rule6 % int3)) triple3) -> (rule1 % int2)) triple3) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is red.
("Charlie" "is" "red" "+")
int4
Charlie is red.
("Charlie" "is" "red" "+")
((triple4) -> (rule4 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple8 triple9) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((((triple2) -> (rule4 % int2)) triple2) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((((triple4) -> (rule4 % int2)) triple4) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
((((((triple2) -> (rule4 % int3)) triple2) -> (rule6 % int2)) triple1) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Charlie is nice.
("Charlie" "is" "nice" "+")
((((((triple4) -> (rule4 % int3)) triple4) -> (rule6 % int2)) triple3) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
((((((((triple2) -> (rule4 % int4)) triple2) -> (rule6 % int3)) triple1) -> (rule1 % int2)) triple1) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
int4
Anne is smart.
("Anne" "is" "smart" "+")
((((((((((triple2) -> (rule4 % int5)) triple2) -> (rule6 % int4)) triple1) -> (rule1 % int3)) triple1) -> (rule2 % int2))) -> (rule7 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is red.
("Anne" "is" "red" "+")
int5