Bob is round. If something is quiet then it is blue. If something is green then it is quiet. If something is round then it is green. If Bob is white and Bob is green then Bob is round. If something is quiet then it is green. If Bob is blue then Bob is quiet.
Bob is round.
("Bob" "is" "round" "+")
If something is quiet then it is blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
If something is green then it is quiet.
((("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
If something is round then it is green.
((("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If Bob is white and Bob is green then Bob is round.
((("Bob" "is" "white" "+") ("Bob" "is" "green" "+")) -> ("Bob" "is" "round" "+"))
If something is quiet then it is green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
If Bob is blue then Bob is quiet.
((("Bob" "is" "blue" "+")) -> ("Bob" "is" "quiet" "+"))
Bob is round.
True
1
proof
[(triple1)]
("Bob" "is" "round" "+")
triple1
Bob is not round.
False
1
inv-proof
[(triple1)]
("Bob" "is" "round" "-")
triple1
Bob is green.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "green" "+")
((triple1) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "green" "-")
((triple1) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Bob" "is" "quiet" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not quiet.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("Bob" "is" "quiet" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is blue.
True
4
proof
[(((((((triple1) -> rule3)) -> rule2)) -> rule1))]
("Bob" "is" "blue" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is not blue.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule2)) -> rule1))]
("Bob" "is" "blue" "-")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Bob is round.[(triple1)] @1: Bob is green.[(((triple1) -> rule3))] @2: Bob is quiet.[(((((triple1) -> rule3)) -> rule2))] @3: Bob is blue.[(((((((triple1) -> rule3)) -> rule2)) -> rule1))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3