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