Anne is blue. Anne is cold. Anne is nice. Anne is white. Bob is green. Bob is smart. Bob is not white. All green people are nice. Rough people are cold. If someone is nice then they are rough. Cold people are green. If someone is nice and not green then they are white. If someone is rough and not nice then they are white.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is not white.
("Bob" "is" "white" "-")
All green people are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Rough people are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If someone is nice then they are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
Cold people are green.
((("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If someone is nice and not green then they are white.
((("someone" "is" "nice" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "white" "+"))
If someone is rough and not nice then they are white.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "white" "+"))
Anne is nice.
True
1
proof
[(triple3 OR ((((triple2) -> rule4)) -> rule1))]
("Anne" "is" "nice" "+")
triple3
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not white.
False
1
inv-proof
[(triple4)]
("Anne" "is" "white" "-")
triple4
Bob is nice.
True
2
proof
[(((triple5) -> rule1))]
("Bob" "is" "nice" "+")
((triple5) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is not nice.
False
2
inv-proof
[(((triple5) -> rule1))]
("Bob" "is" "nice" "-")
((triple5) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
True
3
proof
[(((((triple5) -> rule1)) -> rule3))]
("Bob" "is" "rough" "+")
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not rough.
False
3
inv-proof
[(((((triple5) -> rule1)) -> rule3))]
("Bob" "is" "rough" "-")
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is cold.
True
4
proof
[(((((((triple5) -> rule1)) -> rule3)) -> rule2))]
("Bob" "is" "cold" "+")
((((((triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is not cold.
False
4
inv-proof
[(((((((triple5) -> rule1)) -> rule3)) -> rule2))]
("Bob" "is" "cold" "-")
((((((triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2 OR ((((triple3) -> rule3)) -> rule2))] Anne is nice.[(triple3 OR ((((triple2) -> rule4)) -> rule1))] Anne is white.[(triple4)] Bob is green.[(triple5)] Bob is not white.[(triple7)] Bob is smart.[(triple6)] @1: Anne is green.[(((triple2) -> rule4) OR ((((((triple3) -> rule3)) -> rule2)) -> rule4))] Anne is rough.[(((triple3) -> rule3) OR ((((((triple2) -> rule4)) -> rule1)) -> rule3))] Bob is nice.[(((triple5) -> rule1))] @2: Bob is rough.[(((((triple5) -> rule1)) -> rule3))] @3: Bob is cold.[(((((((triple5) -> rule1)) -> rule3)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
((((triple3) -> (rule3 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
((((triple2) -> (rule4 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
triple4
Bob is green.
("Bob" "is" "green" "+")
triple5
Bob is not white.
("Bob" "is" "white" "-")
triple7
Bob is smart.
("Bob" "is" "smart" "+")
triple6
Anne is green.
("Anne" "is" "green" "+")
((triple2) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((((triple3) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is rough.
("Anne" "is" "rough" "+")
((triple3) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((((triple2) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
((triple5) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((((triple5) -> (rule1 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
((((((triple5) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3