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