Anne is cold. Bob is cold. Bob is smart. Erin is nice. Erin is quiet. Erin is smart. Fiona is rough. All smart, kind things are cold. Quiet, nice things are kind. Cold, quiet things are kind. If something is cold and smart then it is white. If something is white and kind then it is nice. If Fiona is kind and Fiona is cold then Fiona is rough. All cold, white things are quiet. All cold things are smart.
Anne is cold.
("Anne" "is" "cold" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
All smart, kind things are cold.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
Quiet, nice things are kind.
((("something" "is" "quiet" "+") ("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
Cold, quiet things are kind.
((("something" "is" "cold" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
If something is cold and smart then it is white.
((("something" "is" "cold" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If something is white and kind then it is nice.
((("something" "is" "white" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
If Fiona is kind and Fiona is cold then Fiona is rough.
((("Fiona" "is" "kind" "+") ("Fiona" "is" "cold" "+")) -> ("Fiona" "is" "rough" "+"))
All cold, white things are quiet.
((("something" "is" "cold" "+") ("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
All cold things are smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
Anne is cold.
True
1
proof
[(triple1)]
("Anne" "is" "cold" "+")
triple1
Bob is not cold.
False
1
inv-proof
[(triple2)]
("Bob" "is" "cold" "-")
triple2
Anne is smart.
True
2
proof
[(((triple1) -> rule8))]
("Anne" "is" "smart" "+")
((triple1) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Bob is not white.
False
3
inv-proof
[(((triple2 triple3) -> rule4) OR ((triple2 ((triple2) -> rule8)) -> rule4))]
("Bob" "is" "white" "-")
((triple2 triple3) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple2 ((triple2) -> (rule8 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Anne is white.
True
4
proof
[(((triple1 ((triple1) -> rule8)) -> rule4))]
("Anne" "is" "white" "+")
((triple1 ((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not white.
False
4
inv-proof
[(((triple1 ((triple1) -> rule8)) -> rule4))]
("Anne" "is" "white" "-")
((triple1 ((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is quiet.
True
6
proof
[(((triple1 ((triple1 ((triple1) -> rule8)) -> rule4)) -> rule7))]
("Anne" "is" "quiet" "+")
((triple1 ((triple1 ((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Bob is not kind.
False
7
inv-proof
[(((triple2 ((triple2 ((triple2 triple3) -> rule4)) -> rule7)) -> rule3) OR ((triple2 ((triple2 ((triple2 ((triple2) -> rule8)) -> rule4)) -> rule7)) -> rule3))]
("Bob" "is" "kind" "-")
((triple2 ((triple2 ((triple2 triple3) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((triple2 ((triple2 ((triple2 ((triple2) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Anne is kind.
True
8
proof
[(((triple1 ((triple1 ((triple1 ((triple1) -> rule8)) -> rule4)) -> rule7)) -> rule3))]
("Anne" "is" "kind" "+")
((triple1 ((triple1 ((triple1 ((triple1) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is not kind.
False
8
inv-proof
[(((triple1 ((triple1 ((triple1 ((triple1) -> rule8)) -> rule4)) -> rule7)) -> rule3))]
("Anne" "is" "kind" "-")
((triple1 ((triple1 ((triple1 ((triple1) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is nice.
True
13
proof
[(((((triple1 ((triple1) -> rule8)) -> rule4) ((triple1 ((triple1 ((triple1 ((triple1) -> rule8)) -> rule4)) -> rule7)) -> rule3)) -> rule5))]
("Anne" "is" "nice" "+")
((((triple1 ((triple1) -> (rule8 % int5))) -> (rule4 % int4)) ((triple1 ((triple1 ((triple1 ((triple1) -> (rule8 % int5))) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is smart.
("Anne" "is" "smart" "+")
int5
Anne is not nice.
False
13
inv-proof
[(((((triple1 ((triple1) -> rule8)) -> rule4) ((triple1 ((triple1 ((triple1 ((triple1) -> rule8)) -> rule4)) -> rule7)) -> rule3)) -> rule5))]
("Anne" "is" "nice" "-")
((((triple1 ((triple1) -> (rule8 % int5))) -> (rule4 % int4)) ((triple1 ((triple1 ((triple1 ((triple1) -> (rule8 % int5))) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is smart.
("Anne" "is" "smart" "+")
int5
Fiona is not cold.
Unknown
inv-rconc
[@2: Fiona is cold.[CWA. Example of deepest failure = (rule1 <- rule8 <- FAIL)]]
("Fiona" "is" "cold" "-")
Fiona is kind.
Unknown
rconc
[@4: Fiona is kind.[CWA. Example of deepest failure = (rule2 <- rule7 <- rule1 <- rule8 <- FAIL)]]
("Fiona" "is" "kind" "+")
Fiona is not quiet.
Unknown
inv-rconc
[@3: Fiona is quiet.[CWA. Example of deepest failure = (rule7 <- rule1 <- rule8 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Fiona is white.
Unknown
rconc
[@3: Fiona is white.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule8 <- FAIL)]]
("Fiona" "is" "white" "+")
Fiona is not nice.
Unknown
inv-rconc
[@4: Fiona is nice.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule1 <- rule8 <- FAIL)]]
("Fiona" "is" "nice" "-")
Fiona is smart.
Unknown
rconc
[@2: Fiona is smart.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("Fiona" "is" "smart" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
@0: Anne is cold.[(triple1)] Bob is cold.[(triple2)] Bob is smart.[(triple3 OR ((triple2) -> rule8))] Erin is nice.[(triple4)] Erin is quiet.[(triple5)] Erin is smart.[(triple6)] Fiona is rough.[(triple7)] @1: Anne is smart.[(((triple1) -> rule8))] Bob is white.[(((triple2 triple3) -> rule4) OR ((triple2 ((triple2) -> rule8)) -> rule4))] Erin is kind.[(((triple5 triple4) -> rule2))] @2: Anne is white.[(((triple1 ((triple1) -> rule8)) -> rule4))] Bob is quiet.[(((triple2 ((triple2 triple3) -> rule4)) -> rule7) OR ((triple2 ((triple2 ((triple2) -> rule8)) -> rule4)) -> rule7))] Erin is cold.[(((triple6 ((triple5 triple4) -> rule2)) -> rule1))] @3: Anne is quiet.[(((triple1 ((triple1 ((triple1) -> rule8)) -> rule4)) -> rule7))] Bob is kind.[(((triple2 ((triple2 ((triple2 triple3) -> rule4)) -> rule7)) -> rule3) OR ((triple2 ((triple2 ((triple2 ((triple2) -> rule8)) -> rule4)) -> rule7)) -> rule3))] Erin is white.[(((((triple6 ((triple5 triple4) -> rule2)) -> rule1) triple6) -> rule4))] @4: Anne is kind.[(((triple1 ((triple1 ((triple1 ((triple1) -> rule8)) -> rule4)) -> rule7)) -> rule3))] Bob is nice.[(((((triple2 triple3) -> rule4) ((triple2 ((triple2 ((triple2 triple3) -> rule4)) -> rule7)) -> rule3)) -> rule5) OR ((((triple2 ((triple2) -> rule8)) -> rule4) ((triple2 ((triple2 ((triple2 triple3) -> rule4)) -> rule7)) -> rule3)) -> rule5) OR ((((triple2 triple3) -> rule4) ((triple2 ((triple2 ((triple2 ((triple2) -> rule8)) -> rule4)) -> rule7)) -> rule3)) -> rule5) OR ((((triple2 ((triple2) -> rule8)) -> rule4) ((triple2 ((triple2 ((triple2 ((triple2) -> rule8)) -> rule4)) -> rule7)) -> rule3)) -> rule5))] @5: Anne is nice.[(((((triple1 ((triple1) -> rule8)) -> rule4) ((triple1 ((triple1 ((triple1 ((triple1) -> rule8)) -> rule4)) -> rule7)) -> rule3)) -> rule5))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
((triple2) -> (rule8 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
Erin is smart.
("Erin" "is" "smart" "+")
triple6
Fiona is rough.
("Fiona" "is" "rough" "+")
triple7
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple2 triple3) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((triple2 ((triple2) -> (rule8 % int2))) -> (rule4 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
((triple5 triple4) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((triple1 ((triple1) -> (rule8 % int2))) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2 ((triple2 triple3) -> (rule4 % int2))) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((triple2 ((triple2 ((triple2) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Erin is cold.
("Erin" "is" "cold" "+")
((triple6 ((triple5 triple4) -> (rule2 % int2))) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1 ((triple1 ((triple1) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
((triple2 ((triple2 ((triple2 triple3) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
((triple2 ((triple2 ((triple2 ((triple2) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Erin is white.
("Erin" "is" "white" "+")
((((triple6 ((triple5 triple4) -> (rule2 % int3))) -> (rule1 % int2)) triple6) -> (rule4 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
((triple1 ((triple1 ((triple1 ((triple1) -> (rule8 % int4))) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Bob is nice.
("Bob" "is" "nice" "+")
((((triple2 triple3) -> (rule4 % int4)) ((triple2 ((triple2 ((triple2 triple3) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
((((triple2 ((triple2) -> (rule8 % int5))) -> (rule4 % int4)) ((triple2 ((triple2 ((triple2 triple3) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5
((((triple2 triple3) -> (rule4 % int5)) ((triple2 ((triple2 ((triple2 ((triple2) -> (rule8 % int4))) -> (rule4 % int5))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
int5
((((triple2 ((triple2) -> (rule8 % int5))) -> (rule4 % int4)) ((triple2 ((triple2 ((triple2 ((triple2) -> (rule8 % int5))) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
int4
Bob is smart.
("Bob" "is" "smart" "+")
int5
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1 ((triple1) -> (rule8 % int5))) -> (rule4 % int4)) ((triple1 ((triple1 ((triple1 ((triple1) -> (rule8 % int5))) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
Anne is smart.
("Anne" "is" "smart" "+")
int5