Charlie is kind. Dave is quiet. Erin is rough. Fiona is nice. If something is nice and not white then it is round. All rough things are round. All quiet things are round. If something is round and rough then it is nice. If something is rough then it is nice. All quiet, kind things are rough. If Dave is round then Dave is not blue. If something is kind then it is quiet.
Charlie is kind.
("Charlie" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
If something is nice and not white then it is round.
((("something" "is" "nice" "+") ("something" "is" "white" "~")) -> ("something" "is" "round" "+"))
All rough things are round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
All quiet things are round.
((("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
If something is round and rough then it is nice.
((("something" "is" "round" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something is rough then it is nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
All quiet, kind things are rough.
((("something" "is" "quiet" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If Dave is round then Dave is not blue.
((("Dave" "is" "round" "+")) -> ("Dave" "is" "blue" "-"))
If something is kind then it is quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
Fiona is nice.
True
1
proof
[(triple4)]
("Fiona" "is" "nice" "+")
triple4
Charlie is not kind.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "kind" "-")
triple1
Dave is round.
True
2
proof
[(((triple2) -> rule3))]
("Dave" "is" "round" "+")
((triple2) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Erin is not nice.
False
2
inv-proof
[(((triple3) -> rule5) OR ((((triple3) -> rule2) triple3) -> rule4))]
("Erin" "is" "nice" "-")
((triple3) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple3) -> (rule2 % int2)) triple3) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Charlie is rough.
True
4
proof
[(((((triple1) -> rule8) triple1) -> rule6))]
("Charlie" "is" "rough" "+")
((((triple1) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Dave is blue.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule7))]
("Dave" "is" "blue" "+")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Charlie is nice.
True
5
proof
[(((((((triple1) -> rule8) triple1) -> rule6)) -> rule5) OR ((((((triple1) -> rule8)) -> rule3) ((((triple1) -> rule8) triple1) -> rule6)) -> rule4) OR ((((((((triple1) -> rule8) triple1) -> rule6)) -> rule2) ((((triple1) -> rule8) triple1) -> rule6)) -> rule4))]
("Charlie" "is" "nice" "+")
((((((triple1) -> (rule8 % int3)) triple1) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((((triple1) -> (rule8 % int4))) -> (rule3 % int3)) ((((triple1) -> (rule8 % int4)) triple1) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
((((((((triple1) -> (rule8 % int4)) triple1) -> (rule6 % int3))) -> (rule2 % int2)) ((((triple1) -> (rule8 % int4)) triple1) -> (rule6 % int3))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is not nice.
False
5
inv-proof
[(((((((triple1) -> rule8) triple1) -> rule6)) -> rule5) OR ((((((triple1) -> rule8)) -> rule3) ((((triple1) -> rule8) triple1) -> rule6)) -> rule4) OR ((((((((triple1) -> rule8) triple1) -> rule6)) -> rule2) ((((triple1) -> rule8) triple1) -> rule6)) -> rule4))]
("Charlie" "is" "nice" "-")
((((((triple1) -> (rule8 % int3)) triple1) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((((triple1) -> (rule8 % int4))) -> (rule3 % int3)) ((((triple1) -> (rule8 % int4)) triple1) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
((((((((triple1) -> (rule8 % int4)) triple1) -> (rule6 % int3))) -> (rule2 % int2)) ((((triple1) -> (rule8 % int4)) triple1) -> (rule6 % int3))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "quiet" "-")
Dave is rough.
Unknown
rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "rough" "+")
Dave is not nice.
Unknown
inv-rconc
[@2: Dave is nice.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Dave" "is" "nice" "-")
Fiona is quiet.
Unknown
rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "quiet" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
@0: Charlie is kind.[(triple1)] Dave is quiet.[(triple2)] Erin is rough.[(triple3)] Fiona is nice.[(triple4)] @1: Charlie is quiet.[(((triple1) -> rule8))] Dave is round.[(((triple2) -> rule3))] Erin is nice.[(((triple3) -> rule5) OR ((((triple3) -> rule2) triple3) -> rule4))] Erin is round.[(((triple3) -> rule2))] @2: Charlie is rough.[(((((triple1) -> rule8) triple1) -> rule6))] Charlie is round.[(((((triple1) -> rule8)) -> rule3) OR ((((((triple1) -> rule8) triple1) -> rule6)) -> rule2))] Dave is not blue.[(((((triple2) -> rule3)) -> rule7))] @3: Charlie is nice.[(((((((triple1) -> rule8) triple1) -> rule6)) -> rule5) OR ((((((triple1) -> rule8)) -> rule3) ((((triple1) -> rule8) triple1) -> rule6)) -> rule4) OR ((((((((triple1) -> rule8) triple1) -> rule6)) -> rule2) ((((triple1) -> rule8) triple1) -> rule6)) -> rule4))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Erin is rough.
("Erin" "is" "rough" "+")
triple3
Fiona is nice.
("Fiona" "is" "nice" "+")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1) -> (rule8 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple2) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((triple3) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple3) -> (rule2 % int2)) triple3) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((triple3) -> (rule2 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple1) -> (rule8 % int2)) triple1) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((((triple1) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((((triple1) -> (rule8 % int3)) triple1) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Dave is not blue.
("Dave" "is" "blue" "-")
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
Dave is not blue.
("Dave" "is" "blue" "-")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((((triple1) -> (rule8 % int3)) triple1) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((((triple1) -> (rule8 % int4))) -> (rule3 % int3)) ((((triple1) -> (rule8 % int4)) triple1) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
((((((((triple1) -> (rule8 % int4)) triple1) -> (rule6 % int3))) -> (rule2 % int2)) ((((triple1) -> (rule8 % int4)) triple1) -> (rule6 % int3))) -> (rule4 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4