Bob is red. If something is blue and big then it is white. Red things are big. If something is big then it is blue.
Bob is red.
("Bob" "is" "red" "+")
If something is blue and big then it is white.
((("something" "is" "blue" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
Red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If something is big then it is blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
Bob is red.
True
1
proof
[(triple1)]
("Bob" "is" "red" "+")
triple1
Bob is not red.
False
1
inv-proof
[(triple1)]
("Bob" "is" "red" "-")
triple1
Bob is big.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "big" "+")
((triple1) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is not big.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "big" "-")
((triple1) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
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 big.
("Bob" "is" "big" "+")
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 big.
("Bob" "is" "big" "+")
int2
Bob is white.
True
6
proof
[(((((((triple1) -> rule2)) -> rule3) ((triple1) -> rule2)) -> rule1))]
("Bob" "is" "white" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2)) ((triple1) -> (rule2 % int3))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is not white.
False
6
inv-proof
[(((((((triple1) -> rule2)) -> rule3) ((triple1) -> rule2)) -> rule1))]
("Bob" "is" "white" "-")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2)) ((triple1) -> (rule2 % int3))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is red.[(triple1)] @1: Bob is big.[(((triple1) -> rule2))] @2: Bob is blue.[(((((triple1) -> rule2)) -> rule3))] @3: Bob is white.[(((((((triple1) -> rule2)) -> rule3) ((triple1) -> rule2)) -> rule1))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Bob is big.
("Bob" "is" "big" "+")
((triple1) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((((((triple1) -> (rule2 % int3))) -> (rule3 % int2)) ((triple1) -> (rule2 % int3))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3