Bob is rough. Erin is smart. Erin is young. All rough people are white. Cold people are white. If someone is white then they are cold. If Bob is white and Bob is young then Bob is not cold. If someone is smart and young then they are rough. If someone is cold and big then they are smart.
Bob is rough.
("Bob" "is" "rough" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is young.
("Erin" "is" "young" "+")
All rough people are white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
Cold people are white.
((("someone" "is" "cold" "+")) -> ("someone" "is" "white" "+"))
If someone is white then they are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
If Bob is white and Bob is young then Bob is not cold.
((("Bob" "is" "white" "+") ("Bob" "is" "young" "+")) -> ("Bob" "is" "cold" "-"))
If someone is smart and young then they are rough.
((("someone" "is" "smart" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If someone is cold and big then they are smart.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Erin is smart.
True
1
proof
[(triple2)]
("Erin" "is" "smart" "+")
triple2
Erin is not smart.
False
1
inv-proof
[(triple2)]
("Erin" "is" "smart" "-")
triple2
Bob is white.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "white" "+")
((triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is not white.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "white" "-")
((triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Erin is white.
True
4
proof
[(((((triple2 triple3) -> rule5)) -> rule1))]
("Erin" "is" "white" "+")
((((triple2 triple3) -> (rule5 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Bob is not cold.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("Bob" "is" "cold" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Erin is cold.
True
5
proof
[(((((((triple2 triple3) -> rule5)) -> rule1)) -> rule3))]
("Erin" "is" "cold" "+")
((((((triple2 triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is not cold.
False
5
inv-proof
[(((((((triple2 triple3) -> rule5)) -> rule1)) -> rule3))]
("Erin" "is" "cold" "-")
((((((triple2 triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "smart" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is rough.[(triple1)] Erin is smart.[(triple2)] Erin is young.[(triple3)] @1: Bob is white.[(((triple1) -> rule1))] Erin is rough.[(((triple2 triple3) -> rule5))] @2: Bob is cold.[(((((triple1) -> rule1)) -> rule3))] Erin is white.[(((((triple2 triple3) -> rule5)) -> rule1))] @3: Erin is cold.[(((((((triple2 triple3) -> rule5)) -> rule1)) -> rule3))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Erin is smart.
("Erin" "is" "smart" "+")
triple2
Erin is young.
("Erin" "is" "young" "+")
triple3
Bob is white.
("Bob" "is" "white" "+")
((triple1) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
((triple2 triple3) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
((((triple2 triple3) -> (rule5 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
((((((triple2 triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3