Bob is white. If someone is round and blue then they are white. If Bob is round and Bob is blue then Bob is quiet. If someone is white and round then they are not cold. If someone is white then they are round. If someone is blue and not round then they are big. If someone is white and not cold then they are quiet. All blue people are quiet. If someone is white and not big then they are not quiet.
Bob is white.
("Bob" "is" "white" "+")
If someone is round and blue then they are white.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
If Bob is round and Bob is blue then Bob is quiet.
((("Bob" "is" "round" "+") ("Bob" "is" "blue" "+")) -> ("Bob" "is" "quiet" "+"))
If someone is white and round then they are not cold.
((("someone" "is" "white" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "-"))
If someone is white then they are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
If someone is blue and not round then they are big.
((("someone" "is" "blue" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "big" "+"))
If someone is white and not cold then they are quiet.
((("someone" "is" "white" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "quiet" "+"))
All blue people are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If someone is white and not big then they are not quiet.
((("someone" "is" "white" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "quiet" "-"))
Bob is white.
True
1
proof
[(triple1)]
("Bob" "is" "white" "+")
triple1
Bob is not white.
False
1
inv-proof
[(triple1)]
("Bob" "is" "white" "-")
triple1
Bob is round.
True
2
proof
[(((triple1) -> rule4))]
("Bob" "is" "round" "+")
((triple1) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple1) -> rule4))]
("Bob" "is" "round" "-")
((triple1) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not cold.
True
4
proof
[(((triple1 ((triple1) -> rule4)) -> rule3))]
("Bob" "is" "cold" "-")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is cold.
False
4
inv-proof
[(((triple1 ((triple1) -> rule4)) -> rule3))]
("Bob" "is" "cold" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is quiet.
True
6
proof
[(((triple1 ((triple1 ((triple1) -> rule4)) -> rule3)) -> rule6))]
("Bob" "is" "quiet" "+")
((triple1 ((triple1 ((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not cold.
("Bob" "is" "cold" "-")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is not quiet.
False
6
inv-proof
[(((triple1 ((triple1 ((triple1) -> rule4)) -> rule3)) -> rule6))]
("Bob" "is" "quiet" "-")
((triple1 ((triple1 ((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not cold.
("Bob" "is" "cold" "-")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "big" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Bob is white.[(triple1)] @1: Bob is round.[(((triple1) -> rule4))] @2: Bob is not cold.[(((triple1 ((triple1) -> rule4)) -> rule3))] @3: Bob is quiet.[(((triple1 ((triple1 ((triple1) -> rule4)) -> rule3)) -> rule6))]
Bob is white.
("Bob" "is" "white" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not cold.
("Bob" "is" "cold" "-")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1 ((triple1 ((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is not cold.
("Bob" "is" "cold" "-")
int2
Bob is round.
("Bob" "is" "round" "+")
int3