Anne is cold. Bob is cold. Dave is young. Harry is kind. All white things are nice. If something is cold and kind then it is rough. All kind things are cold. Rough, cold things are white. If something is nice then it is furry. Furry things are nice. Furry, nice things are white. Young things are kind.
Anne is cold.
("Anne" "is" "cold" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is kind.
("Harry" "is" "kind" "+")
All white things are nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
If something is cold and kind then it is rough.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
All kind things are cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
Rough, cold things are white.
((("something" "is" "rough" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
If something is nice then it is furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
Furry things are nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
Furry, nice things are white.
((("something" "is" "furry" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
Young things are kind.
((("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
Harry is kind.
True
1
proof
[(triple4)]
("Harry" "is" "kind" "+")
triple4
Harry is not kind.
False
1
inv-proof
[(triple4)]
("Harry" "is" "kind" "-")
triple4
Dave is kind.
True
2
proof
[(((triple3) -> rule8))]
("Dave" "is" "kind" "+")
((triple3) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not kind.
False
2
inv-proof
[(((triple3) -> rule8))]
("Dave" "is" "kind" "-")
((triple3) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is cold.
True
3
proof
[(((((triple3) -> rule8)) -> rule3))]
("Dave" "is" "cold" "+")
((((triple3) -> (rule8 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is not cold.
False
3
inv-proof
[(((((triple3) -> rule8)) -> rule3))]
("Dave" "is" "cold" "-")
((((triple3) -> (rule8 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Harry is white.
True
7
proof
[(((((((triple4) -> rule3) triple4) -> rule2) ((triple4) -> rule3)) -> rule4))]
("Harry" "is" "white" "+")
((((((triple4) -> (rule3 % int3)) triple4) -> (rule2 % int2)) ((triple4) -> (rule3 % int3))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is not white.
False
7
inv-proof
[(((((((triple4) -> rule3) triple4) -> rule2) ((triple4) -> rule3)) -> rule4))]
("Harry" "is" "white" "-")
((((((triple4) -> (rule3 % int3)) triple4) -> (rule2 % int2)) ((triple4) -> (rule3 % int3))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Anne" "is" "kind" "-")
Anne is nice.
Unknown
rconc
[@6: Anne is nice.[CWA. Example of deepest failure = (rule6 <- rule5 <- rule1 <- rule4 <- rule2 <- rule8 <- FAIL)]]
("Anne" "is" "nice" "+")
Bob is not white.
Unknown
inv-rconc
[@6: Bob is white.[CWA. Example of deepest failure = (rule7 <- rule5 <- rule1 <- rule4 <- rule2 <- rule8 <- FAIL)]]
("Bob" "is" "white" "-")
Anne is white.
Unknown
rconc
[@6: Anne is white.[CWA. Example of deepest failure = (rule7 <- rule5 <- rule1 <- rule4 <- rule2 <- rule8 <- FAIL)]]
("Anne" "is" "white" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Harry is young.
Unknown
random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "+")
@0: Anne is cold.[(triple1)] Bob is cold.[(triple2)] Dave is young.[(triple3)] Harry is kind.[(triple4)] @1: Dave is kind.[(((triple3) -> rule8))] Harry is cold.[(((triple4) -> rule3))] @2: Dave is cold.[(((((triple3) -> rule8)) -> rule3))] Harry is rough.[(((((triple4) -> rule3) triple4) -> rule2))] @3: Dave is rough.[(((((((triple3) -> rule8)) -> rule3) ((triple3) -> rule8)) -> rule2))] Harry is white.[(((((((triple4) -> rule3) triple4) -> rule2) ((triple4) -> rule3)) -> rule4))] @4: Dave is white.[(((((((((triple3) -> rule8)) -> rule3) ((triple3) -> rule8)) -> rule2) ((((triple3) -> rule8)) -> rule3)) -> rule4))] Harry is nice.[(((((((((triple4) -> rule3) triple4) -> rule2) ((triple4) -> rule3)) -> rule4)) -> rule1))] @5: Dave is nice.[(((((((((((triple3) -> rule8)) -> rule3) ((triple3) -> rule8)) -> rule2) ((((triple3) -> rule8)) -> rule3)) -> rule4)) -> rule1))] Harry is furry.[(((((((((((triple4) -> rule3) triple4) -> rule2) ((triple4) -> rule3)) -> rule4)) -> rule1)) -> rule5))] @6: Dave is furry.[(((((((((((((triple3) -> rule8)) -> rule3) ((triple3) -> rule8)) -> rule2) ((((triple3) -> rule8)) -> rule3)) -> rule4)) -> rule1)) -> rule5))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
((triple3) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple4) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
((((triple3) -> (rule8 % int2))) -> (rule3 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((((triple4) -> (rule3 % int2)) triple4) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((((triple3) -> (rule8 % int3))) -> (rule3 % int2)) ((triple3) -> (rule8 % int3))) -> (rule2 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is cold.
("Dave" "is" "cold" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
((((((triple4) -> (rule3 % int3)) triple4) -> (rule2 % int2)) ((triple4) -> (rule3 % int3))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
((((((((triple3) -> (rule8 % int4))) -> (rule3 % int3)) ((triple3) -> (rule8 % int4))) -> (rule2 % int2)) ((((triple3) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule4 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is cold.
("Dave" "is" "cold" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
int4
Harry is nice.
("Harry" "is" "nice" "+")
((((((((triple4) -> (rule3 % int4)) triple4) -> (rule2 % int3)) ((triple4) -> (rule3 % int4))) -> (rule4 % int2))) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
((((((((((triple3) -> (rule8 % int5))) -> (rule3 % int4)) ((triple3) -> (rule8 % int5))) -> (rule2 % int3)) ((((triple3) -> (rule8 % int5))) -> (rule3 % int4))) -> (rule4 % int2))) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is cold.
("Dave" "is" "cold" "+")
int4
Dave is kind.
("Dave" "is" "kind" "+")
int5
Harry is furry.
("Harry" "is" "furry" "+")
((((((((((triple4) -> (rule3 % int5)) triple4) -> (rule2 % int4)) ((triple4) -> (rule3 % int5))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
int4
Harry is cold.
("Harry" "is" "cold" "+")
int5
Dave is furry.
("Dave" "is" "furry" "+")
((((((((((((triple3) -> (rule8 % int6))) -> (rule3 % int5)) ((triple3) -> (rule8 % int6))) -> (rule2 % int4)) ((((triple3) -> (rule8 % int6))) -> (rule3 % int5))) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is cold.
("Dave" "is" "cold" "+")
int5
Dave is kind.
("Dave" "is" "kind" "+")
int6