Anne is quiet. Anne is rough. Anne is smart. Charlie is kind. Charlie is rough. Erin is nice. Gary is not kind. All kind, green people are quiet. Rough people are young. Smart people are young. All young, kind people are green. All young, smart people are nice. All quiet, green people are smart.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Gary is not kind.
("Gary" "is" "kind" "-")
All kind, green people are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
Rough people are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
Smart people are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
All young, kind people are green.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
All young, smart people are nice.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
All quiet, green people are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
Charlie is rough.
True
1
proof
[(triple5)]
("Charlie" "is" "rough" "+")
triple5
Charlie is not kind.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "kind" "-")
triple4
Charlie is young.
True
2
proof
[(((triple5) -> rule2))]
("Charlie" "is" "young" "+")
((triple5) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Anne is not young.
False
2
inv-proof
[(((triple2) -> rule2) OR ((triple3) -> rule3))]
("Anne" "is" "young" "-")
((triple2) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((triple3) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Charlie is green.
True
4
proof
[(((((triple5) -> rule2) triple4) -> rule4))]
("Charlie" "is" "green" "+")
((((triple5) -> (rule2 % int2)) triple4) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Anne is not nice.
False
4
inv-proof
[(((((triple2) -> rule2) triple3) -> rule5) OR ((((triple3) -> rule3) triple3) -> rule5))]
("Anne" "is" "nice" "-")
((((triple2) -> (rule2 % int2)) triple3) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((((triple3) -> (rule3 % int2)) triple3) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Charlie is quiet.
True
6
proof
[(((triple4 ((((triple5) -> rule2) triple4) -> rule4)) -> rule1))]
("Charlie" "is" "quiet" "+")
((triple4 ((((triple5) -> (rule2 % int3)) triple4) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is not quiet.
False
6
inv-proof
[(((triple4 ((((triple5) -> rule2) triple4) -> rule4)) -> rule1))]
("Charlie" "is" "quiet" "-")
((triple4 ((((triple5) -> (rule2 % int3)) triple4) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is smart.
True
11
proof
[(((((triple4 ((((triple5) -> rule2) triple4) -> rule4)) -> rule1) ((((triple5) -> rule2) triple4) -> rule4)) -> rule6))]
("Charlie" "is" "smart" "+")
((((triple4 ((((triple5) -> (rule2 % int4)) triple4) -> (rule4 % int3))) -> (rule1 % int2)) ((((triple5) -> (rule2 % int4)) triple4) -> (rule4 % int3))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is not smart.
False
11
inv-proof
[(((((triple4 ((((triple5) -> rule2) triple4) -> rule4)) -> rule1) ((((triple5) -> rule2) triple4) -> rule4)) -> rule6))]
("Charlie" "is" "smart" "-")
((((triple4 ((((triple5) -> (rule2 % int4)) triple4) -> (rule4 % int3))) -> (rule1 % int2)) ((((triple5) -> (rule2 % int4)) triple4) -> (rule4 % int3))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is nice.
True
14
proof
[(((((triple5) -> rule2) ((((triple4 ((((triple5) -> rule2) triple4) -> rule4)) -> rule1) ((((triple5) -> rule2) triple4) -> rule4)) -> rule6)) -> rule5))]
("Charlie" "is" "nice" "+")
((((triple5) -> (rule2 % int5)) ((((triple4 ((((triple5) -> (rule2 % int5)) triple4) -> (rule4 % int4))) -> (rule1 % int3)) ((((triple5) -> (rule2 % int5)) triple4) -> (rule4 % int4))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4
Charlie is young.
("Charlie" "is" "young" "+")
int5
Charlie is not nice.
False
14
inv-proof
[(((((triple5) -> rule2) ((((triple4 ((((triple5) -> rule2) triple4) -> rule4)) -> rule1) ((((triple5) -> rule2) triple4) -> rule4)) -> rule6)) -> rule5))]
("Charlie" "is" "nice" "-")
((((triple5) -> (rule2 % int5)) ((((triple4 ((((triple5) -> (rule2 % int5)) triple4) -> (rule4 % int4))) -> (rule1 % int3)) ((((triple5) -> (rule2 % int5)) triple4) -> (rule4 % int4))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4
Charlie is young.
("Charlie" "is" "young" "+")
int5
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "quiet" "-")
Erin is smart.
Unknown
rconc
[@2: Erin is smart.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Erin" "is" "smart" "+")
Erin is not young.
Unknown
inv-rconc
[@3: Erin is young.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule1 <- FAIL)]]
("Erin" "is" "young" "-")
Gary is nice.
Unknown
rconc
[@3: Gary is nice.[CWA. Example of deepest failure = (rule5 <- rule6 <- rule1 <- FAIL)]]
("Gary" "is" "nice" "+")
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "quiet" "-")
Erin is green.
Unknown
rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "green" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Anne is quiet.[(triple1)] Anne is rough.[(triple2)] Anne is smart.[(triple3)] Charlie is kind.[(triple4)] Charlie is rough.[(triple5)] Erin is nice.[(triple6)] Gary is not kind.[(triple7)] @1: Anne is young.[(((triple2) -> rule2) OR ((triple3) -> rule3))] Charlie is young.[(((triple5) -> rule2))] @2: Anne is nice.[(((((triple2) -> rule2) triple3) -> rule5) OR ((((triple3) -> rule3) triple3) -> rule5))] Charlie is green.[(((((triple5) -> rule2) triple4) -> rule4))] @3: Charlie is quiet.[(((triple4 ((((triple5) -> rule2) triple4) -> rule4)) -> rule1))] @4: Charlie is smart.[(((((triple4 ((((triple5) -> rule2) triple4) -> rule4)) -> rule1) ((((triple5) -> rule2) triple4) -> rule4)) -> rule6))] @5: Charlie is nice.[(((((triple5) -> rule2) ((((triple4 ((((triple5) -> rule2) triple4) -> rule4)) -> rule1) ((((triple5) -> rule2) triple4) -> rule4)) -> rule6)) -> rule5))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Anne is smart.
("Anne" "is" "smart" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Erin is nice.
("Erin" "is" "nice" "+")
triple6
Gary is not kind.
("Gary" "is" "kind" "-")
triple7
Anne is young.
("Anne" "is" "young" "+")
((triple2) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((triple3) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple5) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple2) -> (rule2 % int2)) triple3) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
((((triple3) -> (rule3 % int2)) triple3) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
((((triple5) -> (rule2 % int2)) triple4) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple4 ((((triple5) -> (rule2 % int3)) triple4) -> (rule4 % int2))) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple4 ((((triple5) -> (rule2 % int4)) triple4) -> (rule4 % int3))) -> (rule1 % int2)) ((((triple5) -> (rule2 % int4)) triple4) -> (rule4 % int3))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is young.
("Charlie" "is" "young" "+")
int4
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple5) -> (rule2 % int5)) ((((triple4 ((((triple5) -> (rule2 % int5)) triple4) -> (rule4 % int4))) -> (rule1 % int3)) ((((triple5) -> (rule2 % int5)) triple4) -> (rule4 % int4))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is green.
("Charlie" "is" "green" "+")
int4
Charlie is young.
("Charlie" "is" "young" "+")
int5