Bob is white. Gary is cold. All white, blue things are green. If Bob is white then Bob is blue. If something is cold then it is nice. White, blue things are rough. If something is white and rough then it is cold. If something is young then it is blue. If Gary is white and Gary is young then Gary is cold. If something is green and young then it is blue.
Bob is white.
("Bob" "is" "white" "+")
Gary is cold.
("Gary" "is" "cold" "+")
All white, blue things are green.
((("something" "is" "white" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If Bob is white then Bob is blue.
((("Bob" "is" "white" "+")) -> ("Bob" "is" "blue" "+"))
If something is cold then it is nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
White, blue things are rough.
((("something" "is" "white" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If something is white and rough then it is cold.
((("something" "is" "white" "+") ("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If something is young then it is blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If Gary is white and Gary is young then Gary is cold.
((("Gary" "is" "white" "+") ("Gary" "is" "young" "+")) -> ("Gary" "is" "cold" "+"))
If something is green and young then it is blue.
((("something" "is" "green" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
Bob is white.
True
1
proof
[(triple1)]
("Bob" "is" "white" "+")
triple1
Gary is not cold.
False
1
inv-proof
[(triple2)]
("Gary" "is" "cold" "-")
triple2
Bob is blue.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Gary is not nice.
False
2
inv-proof
[(((triple2) -> rule3))]
("Gary" "is" "nice" "-")
((triple2) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Bob is green.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule1))]
("Bob" "is" "green" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is not rough.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule4))]
("Bob" "is" "rough" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is cold.
True
6
proof
[(((triple1 ((triple1 ((triple1) -> rule2)) -> rule4)) -> rule5))]
("Bob" "is" "cold" "+")
((triple1 ((triple1 ((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is not cold.
False
6
inv-proof
[(((triple1 ((triple1 ((triple1) -> rule2)) -> rule4)) -> rule5))]
("Bob" "is" "cold" "-")
((triple1 ((triple1 ((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "blue" "-")
Gary is rough.
Unknown
rconc
[@1: Gary is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "rough" "+")
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "green" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
Gary is not white.
Unknown
inv-random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "-")
Bob is young.
Unknown
random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "+")
@0: Bob is white.[(triple1)] Gary is cold.[(triple2)] @1: Bob is blue.[(((triple1) -> rule2))] Gary is nice.[(((triple2) -> rule3))] @2: Bob is green.[(((triple1 ((triple1) -> rule2)) -> rule1))] Bob is rough.[(((triple1 ((triple1) -> rule2)) -> rule4))] @3: Bob is cold.[(((triple1 ((triple1 ((triple1) -> rule2)) -> rule4)) -> rule5))] @4: Bob is nice.[(((((triple1 ((triple1 ((triple1) -> rule2)) -> rule4)) -> rule5)) -> rule3))]
Bob is white.
("Bob" "is" "white" "+")
triple1
Gary is cold.
("Gary" "is" "cold" "+")
triple2
Bob is blue.
("Bob" "is" "blue" "+")
((triple1) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
((triple1 ((triple1 ((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
((((triple1 ((triple1 ((triple1) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is blue.
("Bob" "is" "blue" "+")
int4