Anne is quiet. Dave is smart. Erin is nice. Harry is white. If someone is cold and quiet then they are round. If Erin is cold and Erin is nice then Erin is white. All white, quiet people are smart. All white people are quiet. If someone is kind then they are cold. If someone is round and nice then they are white. If someone is quiet and white then they are cold. If someone is smart and white then they are cold.
Anne is quiet.
("Anne" "is" "quiet" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is cold and quiet then they are round.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If Erin is cold and Erin is nice then Erin is white.
((("Erin" "is" "cold" "+") ("Erin" "is" "nice" "+")) -> ("Erin" "is" "white" "+"))
All white, quiet people are smart.
((("someone" "is" "white" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
All white people are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
If someone is kind then they are cold.
((("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If someone is round and nice then they are white.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
If someone is quiet and white then they are cold.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
If someone is smart and white then they are cold.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
Dave is smart.
True
1
proof
[(triple2)]
("Dave" "is" "smart" "+")
triple2
Dave is not smart.
False
1
inv-proof
[(triple2)]
("Dave" "is" "smart" "-")
triple2
Harry is quiet.
True
2
proof
[(((triple4) -> rule4))]
("Harry" "is" "quiet" "+")
((triple4) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not quiet.
False
2
inv-proof
[(((triple4) -> rule4))]
("Harry" "is" "quiet" "-")
((triple4) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is smart.
True
4
proof
[(((triple4 ((triple4) -> rule4)) -> rule3))]
("Harry" "is" "smart" "+")
((triple4 ((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not smart.
False
4
inv-proof
[(((triple4 ((triple4) -> rule4)) -> rule3))]
("Harry" "is" "smart" "-")
((triple4 ((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is round.
True
7
proof
[(((((((triple4) -> rule4) triple4) -> rule7) ((triple4) -> rule4)) -> rule1) OR ((((((triple4 ((triple4) -> rule4)) -> rule3) triple4) -> rule8) ((triple4) -> rule4)) -> rule1))]
("Harry" "is" "round" "+")
((((((triple4) -> (rule4 % int3)) triple4) -> (rule7 % int2)) ((triple4) -> (rule4 % int3))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((triple4 ((triple4) -> (rule4 % int4))) -> (rule3 % int3)) triple4) -> (rule8 % int2)) ((triple4) -> (rule4 % int4))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Harry is not round.
False
7
inv-proof
[(((((((triple4) -> rule4) triple4) -> rule7) ((triple4) -> rule4)) -> rule1) OR ((((((triple4 ((triple4) -> rule4)) -> rule3) triple4) -> rule8) ((triple4) -> rule4)) -> rule1))]
("Harry" "is" "round" "-")
((((((triple4) -> (rule4 % int3)) triple4) -> (rule7 % int2)) ((triple4) -> (rule4 % int3))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((triple4 ((triple4) -> (rule4 % int4))) -> (rule3 % int3)) triple4) -> (rule8 % int2)) ((triple4) -> (rule4 % int4))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4
Dave is not quiet.
Unknown
inv-rconc
[@2: Dave is quiet.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Dave" "is" "quiet" "-")
Erin is white.
Unknown
rconc
[@5: Erin is white.[CWA. Example of deepest failure = (rule2 <- rule7 <- rule4 <- rule6 <- rule1 <- FAIL)]]
("Erin" "is" "white" "+")
Erin is not quiet.
Unknown
inv-rconc
[@4: Erin is quiet.[CWA. Example of deepest failure = (rule4 <- rule2 <- rule8 <- rule3 <- FAIL)]]
("Erin" "is" "quiet" "-")
Erin is smart.
Unknown
rconc
[@4: Erin is smart.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule2 <- rule5 <- FAIL)]]
("Erin" "is" "smart" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Anne is quiet.[(triple1)] Dave is smart.[(triple2)] Erin is nice.[(triple3)] Harry is white.[(triple4)] @1: Harry is quiet.[(((triple4) -> rule4))] @2: Harry is cold.[(((((triple4) -> rule4) triple4) -> rule7) OR ((((triple4 ((triple4) -> rule4)) -> rule3) triple4) -> rule8))] Harry is smart.[(((triple4 ((triple4) -> rule4)) -> rule3))] @3: Harry is round.[(((((((triple4) -> rule4) triple4) -> rule7) ((triple4) -> rule4)) -> rule1) OR ((((((triple4 ((triple4) -> rule4)) -> rule3) triple4) -> rule8) ((triple4) -> rule4)) -> rule1))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
triple3
Harry is white.
("Harry" "is" "white" "+")
triple4
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple4) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((((triple4) -> (rule4 % int2)) triple4) -> (rule7 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((triple4 ((triple4) -> (rule4 % int3))) -> (rule3 % int2)) triple4) -> (rule8 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
((triple4 ((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((((triple4) -> (rule4 % int3)) triple4) -> (rule7 % int2)) ((triple4) -> (rule4 % int3))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
int3
((((((triple4 ((triple4) -> (rule4 % int4))) -> (rule3 % int3)) triple4) -> (rule8 % int2)) ((triple4) -> (rule4 % int4))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
int4