Bob is nice. Bob is young. Erin is not nice. Gary is cold. Gary is nice. Gary is white. Gary is not young. If Bob is young then Bob is rough. If something is nice and young then it is big. If Gary is smart and Gary is not young then Gary is nice. All white, nice things are smart. Smart things are white. If Bob is big then Bob is smart. If Gary is not white then Gary is rough. All rough things are cold.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is not nice.
("Erin" "is" "nice" "-")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is white.
("Gary" "is" "white" "+")
Gary is not young.
("Gary" "is" "young" "-")
If Bob is young then Bob is rough.
((("Bob" "is" "young" "+")) -> ("Bob" "is" "rough" "+"))
If something is nice and young then it is big.
((("something" "is" "nice" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
If Gary is smart and Gary is not young then Gary is nice.
((("Gary" "is" "smart" "+") ("Gary" "is" "young" "~")) -> ("Gary" "is" "nice" "+"))
All white, nice things are smart.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
Smart things are white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If Bob is big then Bob is smart.
((("Bob" "is" "big" "+")) -> ("Bob" "is" "smart" "+"))
If Gary is not white then Gary is rough.
((("Gary" "is" "white" "~")) -> ("Gary" "is" "rough" "+"))
All rough things are cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
Bob is nice.
True
1
proof
[(triple1)]
("Bob" "is" "nice" "+")
triple1
Gary is not cold.
False
1
inv-proof
[(triple4)]
("Gary" "is" "cold" "-")
triple4
Bob is big.
True
3
proof
[(((triple1 triple2) -> rule2))]
("Bob" "is" "big" "+")
((triple1 triple2) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is not big.
False
3
inv-proof
[(((triple1 triple2) -> rule2))]
("Bob" "is" "big" "-")
((triple1 triple2) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is smart.
True
4
proof
[(((((triple1 triple2) -> rule2)) -> rule6))]
("Bob" "is" "smart" "+")
((((triple1 triple2) -> (rule2 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not smart.
False
4
inv-proof
[(((((triple1 triple2) -> rule2)) -> rule6))]
("Bob" "is" "smart" "-")
((((triple1 triple2) -> (rule2 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is white.
True
5
proof
[(((((((triple1 triple2) -> rule2)) -> rule6)) -> rule5))]
("Bob" "is" "white" "+")
((((((triple1 triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is not white.
False
5
inv-proof
[(((((((triple1 triple2) -> rule2)) -> rule6)) -> rule5))]
("Bob" "is" "white" "-")
((((((triple1 triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "cold" "-")
Erin is big.
Unknown
rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "big" "+")
Gary is not big.
Unknown
inv-rconc
[@1: Gary is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "big" "-")
Erin is smart.
Unknown
rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "smart" "+")
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
@0: Bob is nice.[(triple1)] Bob is young.[(triple2)] Erin is not nice.[(triple3)] Gary is cold.[(triple4)] Gary is nice.[(triple5)] Gary is not young.[(triple7)] Gary is white.[(triple6)] @1: Bob is big.[(((triple1 triple2) -> rule2))] Bob is rough.[(((triple2) -> rule1))] Gary is smart.[(((triple6 triple5) -> rule4))] @2: Bob is cold.[(((((triple2) -> rule1)) -> rule8))] Bob is smart.[(((((triple1 triple2) -> rule2)) -> rule6))] @3: Bob is white.[(((((((triple1 triple2) -> rule2)) -> rule6)) -> rule5))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Erin is not nice.
("Erin" "is" "nice" "-")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Gary is nice.
("Gary" "is" "nice" "+")
triple5
Gary is not young.
("Gary" "is" "young" "-")
triple7
Gary is white.
("Gary" "is" "white" "+")
triple6
Bob is big.
("Bob" "is" "big" "+")
((triple1 triple2) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((triple2) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple6 triple5) -> (rule4 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((((triple2) -> (rule1 % int2))) -> (rule8 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((((triple1 triple2) -> (rule2 % int2))) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((((((triple1 triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3