Dave is green. Dave is white. Harry is white. All nice things are kind. All rough things are nice. If Harry is white then Harry is rough.
Dave is green.
("Dave" "is" "green" "+")
Dave is white.
("Dave" "is" "white" "+")
Harry is white.
("Harry" "is" "white" "+")
All nice things are kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
All rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If Harry is white then Harry is rough.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "rough" "+"))
Dave is white.
True
1
proof
[(triple2)]
("Dave" "is" "white" "+")
triple2
Dave is not white.
False
1
inv-proof
[(triple2)]
("Dave" "is" "white" "-")
triple2
Harry is rough.
True
2
proof
[(((triple3) -> rule3))]
("Harry" "is" "rough" "+")
((triple3) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is not rough.
False
2
inv-proof
[(((triple3) -> rule3))]
("Harry" "is" "rough" "-")
((triple3) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
True
3
proof
[(((((triple3) -> rule3)) -> rule2))]
("Harry" "is" "nice" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not nice.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule2))]
("Harry" "is" "nice" "-")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is kind.
True
4
proof
[(((((((triple3) -> rule3)) -> rule2)) -> rule1))]
("Harry" "is" "kind" "+")
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is not kind.
False
4
inv-proof
[(((((((triple3) -> rule3)) -> rule2)) -> rule1))]
("Harry" "is" "kind" "-")
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Dave is not nice.
Unknown
inv-rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "nice" "-")
Dave is kind.
Unknown
rconc
[@2: Dave is kind.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Dave" "is" "kind" "+")
Dave is not cold.
Unknown
inv-random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Dave is green.[(triple1)] Dave is white.[(triple2)] Harry is white.[(triple3)] @1: Harry is rough.[(((triple3) -> rule3))] @2: Harry is nice.[(((((triple3) -> rule3)) -> rule2))] @3: Harry is kind.[(((((((triple3) -> rule3)) -> rule2)) -> rule1))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Harry is white.
("Harry" "is" "white" "+")
triple3
Harry is rough.
("Harry" "is" "rough" "+")
((triple3) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3