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