Anne is cold. Bob is big. Bob is nice. Erin is green. Erin is rough. Gary is big. Gary is kind. All green people are cold. All big people are green.
Anne is cold.
("Anne" "is" "cold" "+")
Bob is big.
("Bob" "is" "big" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is kind.
("Gary" "is" "kind" "+")
All green people are cold.
((("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
All big people are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
Bob is big.
True
1
proof
[(triple2)]
("Bob" "is" "big" "+")
triple2
Gary is not kind.
False
1
inv-proof
[(triple7)]
("Gary" "is" "kind" "-")
triple7
Gary is green.
True
2
proof
[(((triple6) -> rule2))]
("Gary" "is" "green" "+")
((triple6) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Erin is not cold.
False
2
inv-proof
[(((triple4) -> rule1))]
("Erin" "is" "cold" "-")
((triple4) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Bob is cold.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("Bob" "is" "cold" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not cold.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Bob" "is" "cold" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "green" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Erin is not kind.
Unknown
inv-random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Anne is cold.[(triple1)] Bob is big.[(triple2)] Bob is nice.[(triple3)] Erin is green.[(triple4)] Erin is rough.[(triple5)] Gary is big.[(triple6)] Gary is kind.[(triple7)] @1: Bob is green.[(((triple2) -> rule2))] Erin is cold.[(((triple4) -> rule1))] Gary is green.[(((triple6) -> rule2))] @2: Bob is cold.[(((((triple2) -> rule2)) -> rule1))] Gary is cold.[(((((triple6) -> rule2)) -> rule1))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Bob is big.
("Bob" "is" "big" "+")
triple2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Erin is green.
("Erin" "is" "green" "+")
triple4
Erin is rough.
("Erin" "is" "rough" "+")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is kind.
("Gary" "is" "kind" "+")
triple7
Bob is green.
("Bob" "is" "green" "+")
((triple2) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple4) -> (rule1 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple6) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((triple6) -> (rule2 % int2))) -> (rule1 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2