Bob is quiet. Bob is white. Charlie is quiet. Charlie is rough. Charlie is round. Erin is round. Erin is white. If something is white and nice then it is cold. If Charlie is round and Charlie is rough then Charlie is white. If Erin is quiet then Erin is white. All rough things are white. White, rough things are nice. All cold things are white.
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
If something is white and nice then it is cold.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If Charlie is round and Charlie is rough then Charlie is white.
((("Charlie" "is" "round" "+") ("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "white" "+"))
If Erin is quiet then Erin is white.
((("Erin" "is" "quiet" "+")) -> ("Erin" "is" "white" "+"))
All rough things are white.
((("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
White, rough things are nice.
((("something" "is" "white" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
All cold things are white.
((("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
Erin is white.
True
1
proof
[(triple7)]
("Erin" "is" "white" "+")
triple7
Bob is not white.
False
1
inv-proof
[(triple2)]
("Bob" "is" "white" "-")
triple2
Charlie is white.
True
2
proof
[(((triple4) -> rule4) OR ((triple5 triple4) -> rule2))]
("Charlie" "is" "white" "+")
((triple4) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple5 triple4) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple4) -> rule4) OR ((triple5 triple4) -> rule2))]
("Charlie" "is" "white" "-")
((triple4) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple5 triple4) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
True
4
proof
[(((((triple4) -> rule4) triple4) -> rule5) OR ((((triple5 triple4) -> rule2) triple4) -> rule5))]
("Charlie" "is" "nice" "+")
((((triple4) -> (rule4 % int2)) triple4) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((triple5 triple4) -> (rule2 % int2)) triple4) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not nice.
False
4
inv-proof
[(((((triple4) -> rule4) triple4) -> rule5) OR ((((triple5 triple4) -> rule2) triple4) -> rule5))]
("Charlie" "is" "nice" "-")
((((triple4) -> (rule4 % int2)) triple4) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((triple5 triple4) -> (rule2 % int2)) triple4) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is cold.
True
7
proof
[(((((triple4) -> rule4) ((((triple4) -> rule4) triple4) -> rule5)) -> rule1) OR ((((triple4) -> rule4) ((((triple5 triple4) -> rule2) triple4) -> rule5)) -> rule1) OR ((((triple5 triple4) -> rule2) ((((triple4) -> rule4) triple4) -> rule5)) -> rule1) OR ((((triple5 triple4) -> rule2) ((((triple5 triple4) -> rule2) triple4) -> rule5)) -> rule1))]
("Charlie" "is" "cold" "+")
((((triple4) -> (rule4 % int3)) ((((triple4) -> (rule4 % int3)) triple4) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((triple4) -> (rule4 % int3)) ((((triple5 triple4) -> (rule2 % int3)) triple4) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((triple5 triple4) -> (rule2 % int3)) ((((triple4) -> (rule4 % int3)) triple4) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((triple5 triple4) -> (rule2 % int3)) ((((triple5 triple4) -> (rule2 % int3)) triple4) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is not cold.
False
7
inv-proof
[(((((triple4) -> rule4) ((((triple4) -> rule4) triple4) -> rule5)) -> rule1) OR ((((triple4) -> rule4) ((((triple5 triple4) -> rule2) triple4) -> rule5)) -> rule1) OR ((((triple5 triple4) -> rule2) ((((triple4) -> rule4) triple4) -> rule5)) -> rule1) OR ((((triple5 triple4) -> rule2) ((((triple5 triple4) -> rule2) triple4) -> rule5)) -> rule1))]
("Charlie" "is" "cold" "-")
((((triple4) -> (rule4 % int3)) ((((triple4) -> (rule4 % int3)) triple4) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((triple4) -> (rule4 % int3)) ((((triple5 triple4) -> (rule2 % int3)) triple4) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((triple5 triple4) -> (rule2 % int3)) ((((triple4) -> (rule4 % int3)) triple4) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((triple5 triple4) -> (rule2 % int3)) ((((triple5 triple4) -> (rule2 % int3)) triple4) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Erin is not cold.
Unknown
inv-rconc
[@2: Erin is cold.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Erin" "is" "cold" "-")
Erin is nice.
Unknown
rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "nice" "+")
Bob is not nice.
Unknown
inv-rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "nice" "-")
Bob is cold.
Unknown
rconc
[@2: Bob is cold.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Bob" "is" "cold" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
Bob is not red.
Unknown
inv-random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Bob is quiet.[(triple1)] Bob is white.[(triple2)] Charlie is quiet.[(triple3)] Charlie is rough.[(triple4)] Charlie is round.[(triple5)] Erin is round.[(triple6)] Erin is white.[(triple7)] @1: Charlie is white.[(((triple4) -> rule4) OR ((triple5 triple4) -> rule2))] @2: Charlie is nice.[(((((triple4) -> rule4) triple4) -> rule5) OR ((((triple5 triple4) -> rule2) triple4) -> rule5))] @3: Charlie is cold.[(((((triple4) -> rule4) ((((triple4) -> rule4) triple4) -> rule5)) -> rule1) OR ((((triple4) -> rule4) ((((triple5 triple4) -> rule2) triple4) -> rule5)) -> rule1) OR ((((triple5 triple4) -> rule2) ((((triple4) -> rule4) triple4) -> rule5)) -> rule1) OR ((((triple5 triple4) -> rule2) ((((triple5 triple4) -> rule2) triple4) -> rule5)) -> rule1))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
Charlie is round.
("Charlie" "is" "round" "+")
triple5
Erin is round.
("Erin" "is" "round" "+")
triple6
Erin is white.
("Erin" "is" "white" "+")
triple7
Charlie is white.
("Charlie" "is" "white" "+")
((triple4) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((triple5 triple4) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple4) -> (rule4 % int2)) triple4) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((triple5 triple4) -> (rule2 % int2)) triple4) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple4) -> (rule4 % int3)) ((((triple4) -> (rule4 % int3)) triple4) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((triple4) -> (rule4 % int3)) ((((triple5 triple4) -> (rule2 % int3)) triple4) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((triple5 triple4) -> (rule2 % int3)) ((((triple4) -> (rule4 % int3)) triple4) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((triple5 triple4) -> (rule2 % int3)) ((((triple5 triple4) -> (rule2 % int3)) triple4) -> (rule5 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3