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