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