Bob is kind. If something is furry then it is quiet. All kind things are cold. If Bob is cold then Bob is blue. If Bob is blue then Bob is furry. All quiet, nice things are furry. Nice, quiet things are young.
Bob is kind.
("Bob" "is" "kind" "+")
If something is furry then it is quiet.
((("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
All kind things are cold.
((("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If Bob is cold then Bob is blue.
((("Bob" "is" "cold" "+")) -> ("Bob" "is" "blue" "+"))
If Bob is blue then Bob is furry.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "furry" "+"))
All quiet, nice things are furry.
((("something" "is" "quiet" "+") ("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
Nice, quiet things are young.
((("something" "is" "nice" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
Bob is kind.
True
1
proof
[(triple1)]
("Bob" "is" "kind" "+")
triple1
Bob is not kind.
False
1
inv-proof
[(triple1)]
("Bob" "is" "kind" "-")
triple1
Bob is cold.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is not cold.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "cold" "-")
((triple1) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Bob" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not blue.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Bob" "is" "blue" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is furry.
True
4
proof
[(((((((triple1) -> rule2)) -> rule3)) -> rule4))]
("Bob" "is" "furry" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is not furry.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule3)) -> rule4))]
("Bob" "is" "furry" "-")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is not young.
Unknown
inv-rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "young" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is kind.[(triple1)] @1: Bob is cold.[(((triple1) -> rule2))] @2: Bob is blue.[(((((triple1) -> rule2)) -> rule3))] @3: Bob is furry.[(((((((triple1) -> rule2)) -> rule3)) -> rule4))] @4: Bob is quiet.[(((((((((triple1) -> rule2)) -> rule3)) -> rule4)) -> rule1))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
((((((((triple1) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
int4