Anne is not cold. Bob is quiet. Bob is rough. Bob is white. Dave is cold. Dave is quiet. Fiona is cold. Fiona is kind. Fiona is nice. Fiona is rough. All quiet, kind people are white. Quiet, blue people are kind. If someone is white and cold then they are kind. All quiet people are blue. If someone is white then they are rough. If someone is rough then they are nice. If someone is cold and not quiet then they are nice. If someone is blue and not rough then they are nice.
Anne is not cold.
("Anne" "is" "cold" "-")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
All quiet, kind people are white.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
Quiet, blue people are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If someone is white and cold then they are kind.
((("someone" "is" "white" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
All quiet people are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
If someone is white then they are rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
If someone is rough then they are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If someone is cold and not quiet then they are nice.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "nice" "+"))
If someone is blue and not rough then they are nice.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "nice" "+"))
Fiona is cold.
True
1
proof
[(triple7)]
("Fiona" "is" "cold" "+")
triple7
Bob is not white.
False
1
inv-proof
[(triple4 OR ((triple2 ((triple2 ((triple2) -> rule4)) -> rule2)) -> rule1))]
("Bob" "is" "white" "-")
triple4
((triple2 ((triple2 ((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Dave is blue.
True
2
proof
[(((triple6) -> rule4))]
("Dave" "is" "blue" "+")
((triple6) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Bob is not blue.
False
2
inv-proof
[(((triple2) -> rule4))]
("Bob" "is" "blue" "-")
((triple2) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Dave is kind.
True
4
proof
[(((triple6 ((triple6) -> rule4)) -> rule2))]
("Dave" "is" "kind" "+")
((triple6 ((triple6) -> (rule4 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not kind.
False
4
inv-proof
[(((triple6 ((triple6) -> rule4)) -> rule2))]
("Dave" "is" "kind" "-")
((triple6 ((triple6) -> (rule4 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is white.
True
6
proof
[(((triple6 ((triple6 ((triple6) -> rule4)) -> rule2)) -> rule1))]
("Dave" "is" "white" "+")
((triple6 ((triple6 ((triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is not white.
False
6
inv-proof
[(((triple6 ((triple6 ((triple6) -> rule4)) -> rule2)) -> rule1))]
("Dave" "is" "white" "-")
((triple6 ((triple6 ((triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is rough.
True
7
proof
[(((((triple6 ((triple6 ((triple6) -> rule4)) -> rule2)) -> rule1)) -> rule5))]
("Dave" "is" "rough" "+")
((((triple6 ((triple6 ((triple6) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is not rough.
False
7
inv-proof
[(((((triple6 ((triple6 ((triple6) -> rule4)) -> rule2)) -> rule1)) -> rule5))]
("Dave" "is" "rough" "-")
((((triple6 ((triple6 ((triple6) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is nice.
True
8
proof
[(((((((triple6 ((triple6 ((triple6) -> rule4)) -> rule2)) -> rule1)) -> rule5)) -> rule6))]
("Dave" "is" "nice" "+")
((((((triple6 ((triple6 ((triple6) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is blue.
("Dave" "is" "blue" "+")
int5
Dave is not nice.
False
8
inv-proof
[(((((((triple6 ((triple6 ((triple6) -> rule4)) -> rule2)) -> rule1)) -> rule5)) -> rule6))]
("Dave" "is" "nice" "-")
((((((triple6 ((triple6 ((triple6) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is blue.
("Dave" "is" "blue" "+")
int5
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "blue" "-")
Fiona is white.
Unknown
rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "white" "+")
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "white" "-")
Anne is rough.
Unknown
rconc
[@2: Anne is rough.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Anne" "is" "rough" "+")
Anne is not nice.
Unknown
inv-rconc
[@3: Anne is nice.[CWA. Example of deepest failure = (rule6 <- rule5 <- rule1 <- FAIL)]]
("Anne" "is" "nice" "-")
Anne is kind.
Unknown
rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "kind" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is not cold.[(triple1)] Bob is quiet.[(triple2)] Bob is rough.[(triple3 OR ((triple4) -> rule5) OR ((((triple2 ((triple2 ((triple2) -> rule4)) -> rule2)) -> rule1)) -> rule5))] Bob is white.[(triple4 OR ((triple2 ((triple2 ((triple2) -> rule4)) -> rule2)) -> rule1))] Dave is cold.[(triple5)] Dave is quiet.[(triple6)] Fiona is cold.[(triple7)] Fiona is kind.[(triple8)] Fiona is nice.[(triple9 OR ((triple10) -> rule6))] Fiona is rough.[(triple10)] @1: Bob is blue.[(((triple2) -> rule4))] Bob is nice.[(((triple3) -> rule6) OR ((((triple4) -> rule5)) -> rule6) OR ((((((triple2 ((triple2 ((triple2) -> rule4)) -> rule2)) -> rule1)) -> rule5)) -> rule6))] Dave is blue.[(((triple6) -> rule4))] @2: Bob is kind.[(((triple2 ((triple2) -> rule4)) -> rule2))] Dave is kind.[(((triple6 ((triple6) -> rule4)) -> rule2))] @3: Dave is white.[(((triple6 ((triple6 ((triple6) -> rule4)) -> rule2)) -> rule1))] @4: Dave is rough.[(((((triple6 ((triple6 ((triple6) -> rule4)) -> rule2)) -> rule1)) -> rule5))] @5: Dave is nice.[(((((((triple6 ((triple6 ((triple6) -> rule4)) -> rule2)) -> rule1)) -> rule5)) -> rule6))]
Anne is not cold.
("Anne" "is" "cold" "-")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is rough.
("Bob" "is" "rough" "+")
triple3
((triple4) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple2 ((triple2 ((triple2) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4
Bob is white.
("Bob" "is" "white" "+")
triple4
((triple2 ((triple2 ((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
triple5
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
Fiona is cold.
("Fiona" "is" "cold" "+")
triple7
Fiona is kind.
("Fiona" "is" "kind" "+")
triple8
Fiona is nice.
("Fiona" "is" "nice" "+")
triple9
((triple10) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple10
Bob is blue.
("Bob" "is" "blue" "+")
((triple2) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((triple3) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple4) -> (rule5 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((((triple2 ((triple2 ((triple2) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
int4
Bob is blue.
("Bob" "is" "blue" "+")
int5
Dave is blue.
("Dave" "is" "blue" "+")
((triple6) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple2 ((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((triple6 ((triple6) -> (rule4 % int2))) -> (rule2 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
((triple6 ((triple6 ((triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
((((triple6 ((triple6 ((triple6) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Dave is blue.
("Dave" "is" "blue" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
((((((triple6 ((triple6 ((triple6) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Dave is blue.
("Dave" "is" "blue" "+")
int5