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