Bob is white. Dave is rough. Gary is blue. White people are blue. Blue people are not nice. If Bob is blue and Bob is not nice then Bob is rough.
Bob is white.
("Bob" "is" "white" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Gary is blue.
("Gary" "is" "blue" "+")
White people are blue.
((("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
Blue people are not nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "-"))
If Bob is blue and Bob is not nice then Bob is rough.
((("Bob" "is" "blue" "+") ("Bob" "is" "nice" "~")) -> ("Bob" "is" "rough" "+"))
Dave is rough.
True
1
proof
[(triple2)]
("Dave" "is" "rough" "+")
triple2
Dave is not rough.
False
1
inv-proof
[(triple2)]
("Dave" "is" "rough" "-")
triple2
Gary is not nice.
True
2
proof
[(((triple3) -> rule2))]
("Gary" "is" "nice" "-")
((triple3) -> (rule2 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is nice.
False
2
inv-proof
[(((triple3) -> rule2))]
("Gary" "is" "nice" "+")
((triple3) -> (rule2 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Bob is not nice.
True
3
proof
[(((((triple1) -> rule1)) -> rule2))]
("Bob" "is" "nice" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is nice.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule2))]
("Bob" "is" "nice" "+")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
True
6
proof
[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule2)) -> rule3))]
("Bob" "is" "rough" "+")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not nice.
("Bob" "is" "nice" "-")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is not rough.
False
6
inv-proof
[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule2)) -> rule3))]
("Bob" "is" "rough" "-")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not nice.
("Bob" "is" "nice" "-")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "blue" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
Gary is not furry.
Unknown
inv-random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Bob is white.[(triple1)] Dave is rough.[(triple2)] Gary is blue.[(triple3)] @1: Bob is blue.[(((triple1) -> rule1))] Gary is not nice.[(((triple3) -> rule2))] @2: Bob is not nice.[(((((triple1) -> rule1)) -> rule2))] @3: Bob is rough.[(((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule2)) -> rule3))]
Bob is white.
("Bob" "is" "white" "+")
triple1
Dave is rough.
("Dave" "is" "rough" "+")
triple2
Gary is blue.
("Gary" "is" "blue" "+")
triple3
Bob is blue.
("Bob" "is" "blue" "+")
((triple1) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
((triple3) -> (rule2 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Bob is not nice.
("Bob" "is" "nice" "-")
((((triple1) -> (rule1 % int2))) -> (rule2 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not nice.
("Bob" "is" "nice" "-")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3