Charlie is red. Dave is quiet. All quiet, white people are not smart. If someone is quiet then they are white. All round people are red. If Charlie is red then Charlie is round. Round people are quiet. Red people are quiet.
Charlie is red.
("Charlie" "is" "red" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
All quiet, white people are not smart.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "smart" "-"))
If someone is quiet then they are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
All round people are red.
((("someone" "is" "round" "+")) -> ("someone" "is" "red" "+"))
If Charlie is red then Charlie is round.
((("Charlie" "is" "red" "+")) -> ("Charlie" "is" "round" "+"))
Round people are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
Red people are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
Charlie is red.
True
1
proof
[(triple1)]
("Charlie" "is" "red" "+")
triple1
Charlie is not red.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "red" "-")
triple1
Charlie is round.
True
2
proof
[(((triple1) -> rule4))]
("Charlie" "is" "round" "+")
((triple1) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is not quiet.
False
2
inv-proof
[(((triple1) -> rule6) OR ((((triple1) -> rule4)) -> rule5))]
("Charlie" "is" "quiet" "-")
((triple1) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Dave is not smart.
True
4
proof
[(((triple2 ((triple2) -> rule2)) -> rule1))]
("Dave" "is" "smart" "-")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is smart.
False
4
inv-proof
[(((triple2 ((triple2) -> rule2)) -> rule1))]
("Dave" "is" "smart" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Charlie is not smart.
True
6
proof
[(((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule2)) -> rule1) OR ((((((triple1) -> rule4)) -> rule5) ((((triple1) -> rule6)) -> rule2)) -> rule1) OR ((((triple1) -> rule6) ((((((triple1) -> rule4)) -> rule5)) -> rule2)) -> rule1) OR ((((((triple1) -> rule4)) -> rule5) ((((((triple1) -> rule4)) -> rule5)) -> rule2)) -> rule1))]
("Charlie" "is" "smart" "-")
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((((triple1) -> (rule4 % int4))) -> (rule5 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
((((triple1) -> (rule6 % int4)) ((((((triple1) -> (rule4 % int3))) -> (rule5 % int4))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
((((((triple1) -> (rule4 % int4))) -> (rule5 % int3)) ((((((triple1) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Charlie is smart.
False
6
inv-proof
[(((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule2)) -> rule1) OR ((((((triple1) -> rule4)) -> rule5) ((((triple1) -> rule6)) -> rule2)) -> rule1) OR ((((triple1) -> rule6) ((((((triple1) -> rule4)) -> rule5)) -> rule2)) -> rule1) OR ((((((triple1) -> rule4)) -> rule5) ((((((triple1) -> rule4)) -> rule5)) -> rule2)) -> rule1))]
("Charlie" "is" "smart" "+")
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((((triple1) -> (rule4 % int4))) -> (rule5 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
((((triple1) -> (rule6 % int4)) ((((((triple1) -> (rule4 % int3))) -> (rule5 % int4))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
((((((triple1) -> (rule4 % int4))) -> (rule5 % int3)) ((((((triple1) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
Dave is not red.
Unknown
inv-rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "red" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Charlie is red.[(triple1)] Dave is quiet.[(triple2)] @1: Charlie is quiet.[(((triple1) -> rule6) OR ((((triple1) -> rule4)) -> rule5))] Charlie is round.[(((triple1) -> rule4))] Dave is white.[(((triple2) -> rule2))] @2: Charlie is white.[(((((triple1) -> rule6)) -> rule2) OR ((((((triple1) -> rule4)) -> rule5)) -> rule2))] Dave is not smart.[(((triple2 ((triple2) -> rule2)) -> rule1))] @3: Charlie is not smart.[(((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule2)) -> rule1) OR ((((((triple1) -> rule4)) -> rule5) ((((triple1) -> rule6)) -> rule2)) -> rule1) OR ((((triple1) -> rule6) ((((((triple1) -> rule4)) -> rule5)) -> rule2)) -> rule1) OR ((((((triple1) -> rule4)) -> rule5) ((((((triple1) -> rule4)) -> rule5)) -> rule2)) -> rule1))]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((triple1) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple2) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Dave is not smart.
("Dave" "is" "smart" "-")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Charlie is not smart.
("Charlie" "is" "smart" "-")
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
((((((triple1) -> (rule4 % int4))) -> (rule5 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4
((((triple1) -> (rule6 % int4)) ((((((triple1) -> (rule4 % int3))) -> (rule5 % int4))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
((((((triple1) -> (rule4 % int4))) -> (rule5 % int3)) ((((((triple1) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is not smart.
("Charlie" "is" "smart" "-")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is round.
("Charlie" "is" "round" "+")
int4