Bob is blue. If Bob is red then Bob is blue. If someone is blue then they are furry. Furry people are red. If someone is furry and not quiet then they are red. Red people are green. All green people are cold. If Bob is not red then Bob is round. If someone is green and not cold then they are round.
Bob is blue.
("Bob" "is" "blue" "+")
If Bob is red then Bob is blue.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "blue" "+"))
If someone is blue then they are furry.
((("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
Furry people are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
If someone is furry and not quiet then they are red.
((("someone" "is" "furry" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "red" "+"))
Red people are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
All green people are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If Bob is not red then Bob is round.
((("Bob" "is" "red" "~")) -> ("Bob" "is" "round" "+"))
If someone is green and not cold then they are round.
((("someone" "is" "green" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "round" "+"))
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 furry.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is not furry.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "furry" "-")
((triple1) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Bob" "is" "red" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is not red.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Bob" "is" "red" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is green.
True
4
proof
[(((((((triple1) -> rule2)) -> rule3)) -> rule5))]
("Bob" "is" "green" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is not green.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule3)) -> rule5))]
("Bob" "is" "green" "-")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is not round.
Unknown
inv-rconc
[@1: Bob is round.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "round" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is blue.[(triple1)] @1: Bob is furry.[(((triple1) -> rule2))] @2: Bob is red.[(((((triple1) -> rule2)) -> rule3))] @3: Bob is green.[(((((((triple1) -> rule2)) -> rule3)) -> rule5))] @4: Bob is cold.[(((((((((triple1) -> rule2)) -> rule3)) -> rule5)) -> rule6))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
int3
Bob is cold.
("Bob" "is" "cold" "+")
((((((((triple1) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
int4