Anne is white. Bob is cold. Erin is white. Gary is cold. If Bob is cold then Bob is white. White people are smart. Quiet people are kind. Quiet, white people are kind. If Bob is smart then Bob is not big. If someone is big and not quiet then they are red.
Anne is white.
("Anne" "is" "white" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is cold.
("Gary" "is" "cold" "+")
If Bob is cold then Bob is white.
((("Bob" "is" "cold" "+")) -> ("Bob" "is" "white" "+"))
White people are smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
Quiet people are kind.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
Quiet, white people are kind.
((("someone" "is" "quiet" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
If Bob is smart then Bob is not big.
((("Bob" "is" "smart" "+")) -> ("Bob" "is" "big" "-"))
If someone is big and not quiet then they are red.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "red" "+"))
Anne is white.
True
1
proof
[(triple1)]
("Anne" "is" "white" "+")
triple1
Anne is not white.
False
1
inv-proof
[(triple1)]
("Anne" "is" "white" "-")
triple1
Erin is smart.
True
2
proof
[(((triple3) -> rule2))]
("Erin" "is" "smart" "+")
((triple3) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not smart.
False
2
inv-proof
[(((triple3) -> rule2))]
("Erin" "is" "smart" "-")
((triple3) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Bob is smart.
True
3
proof
[(((((triple2) -> rule1)) -> rule2))]
("Bob" "is" "smart" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not smart.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2))]
("Bob" "is" "smart" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not big.
True
4
proof
[(((((((triple2) -> rule1)) -> rule2)) -> rule5))]
("Bob" "is" "big" "-")
((((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is not big.
("Bob" "is" "big" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is big.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule2)) -> rule5))]
("Bob" "is" "big" "+")
((((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is not big.
("Bob" "is" "big" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "smart" "-")
Gary is kind.
Unknown
rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "kind" "+")
Anne is not red.
Unknown
inv-rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "red" "-")
Erin is red.
Unknown
rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "red" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Erin is not quiet.
Unknown
inv-random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
@0: Anne is white.[(triple1)] Bob is cold.[(triple2)] Erin is white.[(triple3)] Gary is cold.[(triple4)] @1: Anne is smart.[(((triple1) -> rule2))] Bob is white.[(((triple2) -> rule1))] Erin is smart.[(((triple3) -> rule2))] @2: Bob is smart.[(((((triple2) -> rule1)) -> rule2))] @3: Bob is not big.[(((((((triple2) -> rule1)) -> rule2)) -> rule5))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Erin is white.
("Erin" "is" "white" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple2) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple3) -> (rule2 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not big.
("Bob" "is" "big" "-")
((((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is not big.
("Bob" "is" "big" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3