Anne is rough. Bob is nice. Charlie is red. Dave is round. If someone is nice then they are kind. All rough people are nice. Round people are rough.
Anne is rough.
("Anne" "is" "rough" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
If someone is nice then they are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
All rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
Round people are rough.
((("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
Anne is rough.
True
1
proof
[(triple1)]
("Anne" "is" "rough" "+")
triple1
Bob is not nice.
False
1
inv-proof
[(triple2)]
("Bob" "is" "nice" "-")
triple2
Anne is nice.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Dave is not rough.
False
2
inv-proof
[(((triple4) -> rule3))]
("Dave" "is" "rough" "-")
((triple4) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
True
3
proof
[(((((triple4) -> rule3)) -> rule2))]
("Dave" "is" "nice" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is not nice.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule2))]
("Dave" "is" "nice" "-")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is kind.
True
4
proof
[(((((((triple4) -> rule3)) -> rule2)) -> rule1))]
("Dave" "is" "kind" "+")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is not kind.
False
4
inv-proof
[(((((((triple4) -> rule3)) -> rule2)) -> rule1))]
("Dave" "is" "kind" "-")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Charlie is not rough.
Unknown
inv-rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "rough" "-")
Bob is rough.
Unknown
rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "rough" "+")
Charlie is not nice.
Unknown
inv-rconc
[@2: Charlie is nice.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is kind.
Unknown
rconc
[@3: Charlie is kind.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule3 <- FAIL)]]
("Charlie" "is" "kind" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
@0: Anne is rough.[(triple1)] Bob is nice.[(triple2)] Charlie is red.[(triple3)] Dave is round.[(triple4)] @1: Anne is nice.[(((triple1) -> rule2))] Bob is kind.[(((triple2) -> rule1))] Dave is rough.[(((triple4) -> rule3))] @2: Anne is kind.[(((((triple1) -> rule2)) -> rule1))] Dave is nice.[(((((triple4) -> rule3)) -> rule2))] @3: Dave is kind.[(((((((triple4) -> rule3)) -> rule2)) -> rule1))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
triple4
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple2) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((triple4) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((((((triple4) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3