Anne is blue. Bob is round. Dave is furry. Erin is blue. If something is round and white then it is rough. Round, cold things are white. All rough things are furry. All white, blue things are round. If Anne is rough then Anne is cold. If something is round then it is white.
Anne is blue.
("Anne" "is" "blue" "+")
Bob is round.
("Bob" "is" "round" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Erin is blue.
("Erin" "is" "blue" "+")
If something is round and white then it is rough.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
Round, cold things are white.
((("something" "is" "round" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
All rough things are furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
All white, blue things are round.
((("something" "is" "white" "+") ("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
If Anne is rough then Anne is cold.
((("Anne" "is" "rough" "+")) -> ("Anne" "is" "cold" "+"))
If something is round then it is white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
Bob is round.
True
1
proof
[(triple2)]
("Bob" "is" "round" "+")
triple2
Bob is not round.
False
1
inv-proof
[(triple2)]
("Bob" "is" "round" "-")
triple2
Bob is white.
True
2
proof
[(((triple2) -> rule6))]
("Bob" "is" "white" "+")
((triple2) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not white.
False
2
inv-proof
[(((triple2) -> rule6))]
("Bob" "is" "white" "-")
((triple2) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is rough.
True
4
proof
[(((triple2 ((triple2) -> rule6)) -> rule1))]
("Bob" "is" "rough" "+")
((triple2 ((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not rough.
False
4
inv-proof
[(((triple2 ((triple2) -> rule6)) -> rule1))]
("Bob" "is" "rough" "-")
((triple2 ((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is furry.
True
5
proof
[(((((triple2 ((triple2) -> rule6)) -> rule1)) -> rule3))]
("Bob" "is" "furry" "+")
((((triple2 ((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is not furry.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule6)) -> rule1)) -> rule3))]
("Bob" "is" "furry" "-")
((((triple2 ((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Erin is not rough.
Unknown
inv-rconc
[@3: Erin is rough.[CWA. Example of deepest failure = (rule1 <- rule4 <- rule2 <- FAIL)]]
("Erin" "is" "rough" "-")
Dave is rough.
Unknown
rconc
[@2: Dave is rough.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("Dave" "is" "rough" "+")
Erin is not white.
Unknown
inv-rconc
[@3: Erin is white.[CWA. Example of deepest failure = (rule6 <- rule4 <- rule2 <- FAIL)]]
("Erin" "is" "white" "-")
Dave is white.
Unknown
rconc
[@2: Dave is white.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Dave" "is" "white" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Anne is young.
Unknown
random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "+")
@0: Anne is blue.[(triple1)] Bob is round.[(triple2)] Dave is furry.[(triple3)] Erin is blue.[(triple4)] @1: Bob is white.[(((triple2) -> rule6))] @2: Bob is rough.[(((triple2 ((triple2) -> rule6)) -> rule1))] @3: Bob is furry.[(((((triple2 ((triple2) -> rule6)) -> rule1)) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
((triple2) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((triple2 ((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((triple2 ((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3