Anne is furry. Bob is young. Rough, quiet things are furry. If Anne is furry and Anne is quiet then Anne is rough. If Bob is young then Bob is quiet. If something is young then it is rough. Nice, quiet things are cold. If Anne is cold then Anne is rough.
Anne is furry.
("Anne" "is" "furry" "+")
Bob is young.
("Bob" "is" "young" "+")
Rough, quiet things are furry.
((("something" "is" "rough" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
If Anne is furry and Anne is quiet then Anne is rough.
((("Anne" "is" "furry" "+") ("Anne" "is" "quiet" "+")) -> ("Anne" "is" "rough" "+"))
If Bob is young then Bob is quiet.
((("Bob" "is" "young" "+")) -> ("Bob" "is" "quiet" "+"))
If something is young then it is rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "+"))
Nice, quiet things are cold.
((("something" "is" "nice" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "cold" "+"))
If Anne is cold then Anne is rough.
((("Anne" "is" "cold" "+")) -> ("Anne" "is" "rough" "+"))
Bob is young.
True
1
proof
[(triple2)]
("Bob" "is" "young" "+")
triple2
Bob is not young.
False
1
inv-proof
[(triple2)]
("Bob" "is" "young" "-")
triple2
Bob is quiet.
True
2
proof
[(((triple2) -> rule3))]
("Bob" "is" "quiet" "+")
((triple2) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not quiet.
False
2
inv-proof
[(((triple2) -> rule3))]
("Bob" "is" "quiet" "-")
((triple2) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
True
5
proof
[(((((triple2) -> rule4) ((triple2) -> rule3)) -> rule1))]
("Bob" "is" "furry" "+")
((((triple2) -> (rule4 % int3)) ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is not furry.
False
5
inv-proof
[(((((triple2) -> rule4) ((triple2) -> rule3)) -> rule1))]
("Bob" "is" "furry" "-")
((((triple2) -> (rule4 % int3)) ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "cold" "-")
Anne is rough.
Unknown
rconc
[@2: Anne is rough.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Anne" "is" "rough" "+")
Anne is not cold.
Unknown
inv-rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "cold" "-")
Anne is nice.
Unknown
random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Anne is furry.[(triple1)] Bob is young.[(triple2)] @1: Bob is quiet.[(((triple2) -> rule3))] Bob is rough.[(((triple2) -> rule4))] @2: Bob is furry.[(((((triple2) -> rule4) ((triple2) -> rule3)) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple2) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((triple2) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((((triple2) -> (rule4 % int3)) ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3