Anne is cold. Anne is green. Anne is white. Bob is kind. Bob is rough. Bob is white. Erin is big. Erin is cold. Erin is green. Gary is blue. Gary is rough. Gary is white. If someone is kind and rough then they are white. If Anne is cold and Anne is white then Anne is blue. All rough, cold people are big. If someone is kind and big then they are rough. Blue, kind people are cold. Rough people are blue.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is white.
("Bob" "is" "white" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is white.
("Gary" "is" "white" "+")
If someone is kind and rough then they are white.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
If Anne is cold and Anne is white then Anne is blue.
((("Anne" "is" "cold" "+") ("Anne" "is" "white" "+")) -> ("Anne" "is" "blue" "+"))
All rough, cold people are big.
((("someone" "is" "rough" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
If someone is kind and big then they are rough.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
Blue, kind people are cold.
((("someone" "is" "blue" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
Rough people are blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
Bob is white.
True
1
proof
[(triple6 OR ((triple4 triple5) -> rule1))]
("Bob" "is" "white" "+")
triple6
((triple4 triple5) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not kind.
False
1
inv-proof
[(triple4)]
("Bob" "is" "kind" "-")
triple4
Bob is blue.
True
2
proof
[(((triple5) -> rule6))]
("Bob" "is" "blue" "+")
((triple5) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not blue.
False
2
inv-proof
[(((triple5) -> rule6))]
("Bob" "is" "blue" "-")
((triple5) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
True
4
proof
[(((((triple5) -> rule6) triple4) -> rule5))]
("Bob" "is" "cold" "+")
((((triple5) -> (rule6 % int2)) triple4) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is not cold.
False
4
inv-proof
[(((((triple5) -> rule6) triple4) -> rule5))]
("Bob" "is" "cold" "-")
((((triple5) -> (rule6 % int2)) triple4) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Erin is not blue.
Unknown
inv-rconc
[@2: Erin is blue.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Erin" "is" "blue" "-")
Gary is cold.
Unknown
rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "cold" "+")
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "rough" "-")
Gary is kind.
Unknown
random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Anne is cold.[(triple1)] Anne is green.[(triple2)] Anne is white.[(triple3)] Bob is kind.[(triple4)] Bob is rough.[(triple5)] Bob is white.[(triple6 OR ((triple4 triple5) -> rule1))] Erin is big.[(triple7)] Erin is cold.[(triple8)] Erin is green.[(triple9)] Gary is blue.[(triple10 OR ((triple11) -> rule6))] Gary is rough.[(triple11)] Gary is white.[(triple12)] @1: Anne is blue.[(((triple1 triple3) -> rule2))] Bob is blue.[(((triple5) -> rule6))] @2: Bob is cold.[(((((triple5) -> rule6) triple4) -> rule5))] @3: Bob is big.[(((triple5 ((((triple5) -> rule6) triple4) -> rule5)) -> rule3))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Bob is kind.
("Bob" "is" "kind" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
triple5
Bob is white.
("Bob" "is" "white" "+")
triple6
((triple4 triple5) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
triple7
Erin is cold.
("Erin" "is" "cold" "+")
triple8
Erin is green.
("Erin" "is" "green" "+")
triple9
Gary is blue.
("Gary" "is" "blue" "+")
triple10
((triple11) -> (rule6 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
triple11
Gary is white.
("Gary" "is" "white" "+")
triple12
Anne is blue.
("Anne" "is" "blue" "+")
((triple1 triple3) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple5) -> (rule6 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((((triple5) -> (rule6 % int2)) triple4) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
((triple5 ((((triple5) -> (rule6 % int3)) triple4) -> (rule5 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3