Bob is kind. Bob is quiet. Bob is white. Gary is blue. Gary is cold. Gary is quiet. Gary is white. If someone is kind and blue then they are quiet. If someone is big and rough then they are kind. If someone is rough then they are big. Quiet people are kind. If someone is rough and quiet then they are white. If someone is blue and kind then they are rough.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is white.
("Bob" "is" "white" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is white.
("Gary" "is" "white" "+")
If someone is kind and blue then they are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If someone is big and rough then they are kind.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
If someone is rough then they are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
Quiet people are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
If someone is rough and quiet then they are white.
((("someone" "is" "rough" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If someone is blue and kind then they are rough.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
Gary is blue.
True
1
proof
[(triple4)]
("Gary" "is" "blue" "+")
triple4
Bob is not kind.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule4))]
("Bob" "is" "kind" "-")
triple1
((triple2) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Gary is kind.
True
2
proof
[(((triple6) -> rule4))]
("Gary" "is" "kind" "+")
((triple6) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not kind.
False
2
inv-proof
[(((triple6) -> rule4))]
("Gary" "is" "kind" "-")
((triple6) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is rough.
True
4
proof
[(((triple4 ((triple6) -> rule4)) -> rule6))]
("Gary" "is" "rough" "+")
((triple4 ((triple6) -> (rule4 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is not rough.
False
4
inv-proof
[(((triple4 ((triple6) -> rule4)) -> rule6))]
("Gary" "is" "rough" "-")
((triple4 ((triple6) -> (rule4 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is big.
True
5
proof
[(((((triple4 ((triple6) -> rule4)) -> rule6)) -> rule3))]
("Gary" "is" "big" "+")
((((triple4 ((triple6) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is not big.
False
5
inv-proof
[(((((triple4 ((triple6) -> rule4)) -> rule6)) -> rule3))]
("Gary" "is" "big" "-")
((((triple4 ((triple6) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Bob is not big.
Unknown
inv-rconc
[@2: Bob is big.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Bob" "is" "big" "-")
Bob is rough.
Unknown
rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "rough" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Bob is cold.
Unknown
random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "+")
@0: Bob is kind.[(triple1 OR ((triple2) -> rule4))] Bob is quiet.[(triple2)] Bob is white.[(triple3)] Gary is blue.[(triple4)] Gary is cold.[(triple5)] Gary is quiet.[(triple6)] Gary is white.[(triple7 OR ((((triple4 ((triple6) -> rule4)) -> rule6) triple6) -> rule5))] @1: Gary is kind.[(((triple6) -> rule4))] @2: Gary is rough.[(((triple4 ((triple6) -> rule4)) -> rule6))] @3: Gary is big.[(((((triple4 ((triple6) -> rule4)) -> rule6)) -> rule3))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
((triple2) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Bob is white.
("Bob" "is" "white" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
triple4
Gary is cold.
("Gary" "is" "cold" "+")
triple5
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
Gary is white.
("Gary" "is" "white" "+")
triple7
((((triple4 ((triple6) -> (rule4 % int3))) -> (rule6 % int2)) triple6) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
((triple6) -> (rule4 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple4 ((triple6) -> (rule4 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((((triple4 ((triple6) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3