Bob is quiet. Charlie is white. If someone is red and not green then they are not quiet. If someone is green and not nice then they are not quiet. If Charlie is nice then Charlie is quiet. All red, quiet people are big. If someone is cold then they are big. If Bob is not green then Bob is not big. If someone is big then they are white. If Bob is quiet then Bob is red.
Bob is quiet.
("Bob" "is" "quiet" "+")
Charlie is white.
("Charlie" "is" "white" "+")
If someone is red and not green then they are not quiet.
((("someone" "is" "red" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "quiet" "-"))
If someone is green and not nice then they are not quiet.
((("someone" "is" "green" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "quiet" "-"))
If Charlie is nice then Charlie is quiet.
((("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "quiet" "+"))
All red, quiet people are big.
((("someone" "is" "red" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
If someone is cold then they are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
If Bob is not green then Bob is not big.
((("Bob" "is" "green" "~")) -> ("Bob" "is" "big" "-"))
If someone is big then they are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
If Bob is quiet then Bob is red.
((("Bob" "is" "quiet" "+")) -> ("Bob" "is" "red" "+"))
Charlie is white.
True
1
proof
[(triple2)]
("Charlie" "is" "white" "+")
triple2
Charlie is not white.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "white" "-")
triple2
Bob is red.
True
2
proof
[(((triple1) -> rule8))]
("Bob" "is" "red" "+")
((triple1) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is not red.
False
2
inv-proof
[(((triple1) -> rule8))]
("Bob" "is" "red" "-")
((triple1) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
True
4
proof
[(((((triple1) -> rule8) triple1) -> rule4))]
("Bob" "is" "big" "+")
((((triple1) -> (rule8 % int2)) triple1) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is not big.
False
4
inv-proof
[(((((triple1) -> rule8) triple1) -> rule4))]
("Bob" "is" "big" "-")
((((triple1) -> (rule8 % int2)) triple1) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is white.
True
5
proof
[(((((((triple1) -> rule8) triple1) -> rule4)) -> rule7))]
("Bob" "is" "white" "+")
((((((triple1) -> (rule8 % int3)) triple1) -> (rule4 % int2))) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is not white.
False
5
inv-proof
[(((((((triple1) -> rule8) triple1) -> rule4)) -> rule7))]
("Bob" "is" "white" "-")
((((((triple1) -> (rule8 % int3)) triple1) -> (rule4 % int2))) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "big" "-")
Charlie is quiet.
Unknown
rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "quiet" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is quiet.[(triple1)] Charlie is white.[(triple2)] @1: Bob is red.[(((triple1) -> rule8))] @2: Bob is big.[(((((triple1) -> rule8) triple1) -> rule4))] @3: Bob is white.[(((((((triple1) -> rule8) triple1) -> rule4)) -> rule7))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Charlie is white.
("Charlie" "is" "white" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
((triple1) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple1) -> (rule8 % int2)) triple1) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((((((triple1) -> (rule8 % int3)) triple1) -> (rule4 % int2))) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3