Bob is blue. If something is nice then it is big. Quiet things are round. If something is big and quiet then it is furry. Blue things are round. Quiet, blue things are furry. If Bob is blue then Bob is quiet.
Bob is blue.
("Bob" "is" "blue" "+")
If something is nice then it is big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
Quiet things are round.
((("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
If something is big and quiet then it is furry.
((("something" "is" "big" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
Blue things are round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
Quiet, blue things are furry.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
If Bob is blue then Bob is quiet.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "quiet" "+"))
Bob is blue.
True
1
proof
[(triple1)]
("Bob" "is" "blue" "+")
triple1
Bob is not blue.
False
1
inv-proof
[(triple1)]
("Bob" "is" "blue" "-")
triple1
Bob is round.
True
2
proof
[(((triple1) -> rule4) OR ((((triple1) -> rule6)) -> rule2))]
("Bob" "is" "round" "+")
((triple1) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not round.
False
2
inv-proof
[(((triple1) -> rule4) OR ((((triple1) -> rule6)) -> rule2))]
("Bob" "is" "round" "-")
((triple1) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is furry.
True
4
proof
[(((((triple1) -> rule6) triple1) -> rule5))]
("Bob" "is" "furry" "+")
((((triple1) -> (rule6 % int2)) triple1) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not furry.
False
4
inv-proof
[(((((triple1) -> rule6) triple1) -> rule5))]
("Bob" "is" "furry" "-")
((((triple1) -> (rule6 % int2)) triple1) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "big" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is blue.[(triple1)] @1: Bob is quiet.[(((triple1) -> rule6))] Bob is round.[(((triple1) -> rule4) OR ((((triple1) -> rule6)) -> rule2))] @2: Bob is furry.[(((((triple1) -> rule6) triple1) -> rule5))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((triple1) -> (rule6 % int2)) triple1) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2