Bob is young. Erin is blue. Gary is rough. Harry is furry. If something is furry then it is blue. All white things are furry. Rough things are white.
Bob is young.
("Bob" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is furry.
("Harry" "is" "furry" "+")
If something is furry then it is blue.
((("something" "is" "furry" "+")) -> ("something" "is" "blue" "+"))
All white things are furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
Rough things are white.
((("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
Bob is young.
True
1
proof
[(triple1)]
("Bob" "is" "young" "+")
triple1
Gary is not rough.
False
1
inv-proof
[(triple3)]
("Gary" "is" "rough" "-")
triple3
Harry is blue.
True
2
proof
[(((triple4) -> rule1))]
("Harry" "is" "blue" "+")
((triple4) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Gary is not white.
False
2
inv-proof
[(((triple3) -> rule3))]
("Gary" "is" "white" "-")
((triple3) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is furry.
True
3
proof
[(((((triple3) -> rule3)) -> rule2))]
("Gary" "is" "furry" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not furry.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule2))]
("Gary" "is" "furry" "-")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Bob is not blue.
Unknown
inv-rconc
[@3: Bob is blue.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule3 <- FAIL)]]
("Bob" "is" "blue" "-")
Erin is furry.
Unknown
rconc
[@2: Erin is furry.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Erin" "is" "furry" "+")
Bob is not furry.
Unknown
inv-rconc
[@2: Bob is furry.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Bob" "is" "furry" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
@0: Bob is young.[(triple1)] Erin is blue.[(triple2)] Gary is rough.[(triple3)] Harry is furry.[(triple4)] @1: Gary is white.[(((triple3) -> rule3))] Harry is blue.[(((triple4) -> rule1))] @2: Gary is furry.[(((((triple3) -> rule3)) -> rule2))] @3: Gary is blue.[(((((((triple3) -> rule3)) -> rule2)) -> rule1))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Gary is rough.
("Gary" "is" "rough" "+")
triple3
Harry is furry.
("Harry" "is" "furry" "+")
triple4
Gary is white.
("Gary" "is" "white" "+")
((triple3) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple4) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3