Bob is cold. Bob is smart. Erin is smart. If someone is rough and nice then they are cold. If Bob is smart then Bob is not big.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is smart.
("Erin" "is" "smart" "+")
If someone is rough and nice then they are cold.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If Bob is smart then Bob is not big.
((("Bob" "is" "smart" "+")) -> ("Bob" "is" "big" "-"))
Erin is smart.
True
1
proof
[(triple3)]
("Erin" "is" "smart" "+")
triple3
Erin is not smart.
False
1
inv-proof
[(triple3)]
("Erin" "is" "smart" "-")
triple3
Bob is not big.
True
2
proof
[(((triple2) -> rule2))]
("Bob" "is" "big" "-")
((triple2) -> (rule2 % int1))
Bob is not big.
("Bob" "is" "big" "-")
int1
Bob is big.
False
2
inv-proof
[(((triple2) -> rule2))]
("Bob" "is" "big" "+")
((triple2) -> (rule2 % int1))
Bob is not big.
("Bob" "is" "big" "-")
int1
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "cold" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
@0: Bob is cold.[(triple1)] Bob is smart.[(triple2)] Erin is smart.[(triple3)] @1: Bob is not big.[(((triple2) -> rule2))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Bob is not big.
("Bob" "is" "big" "-")
((triple2) -> (rule2 % int1))
Bob is not big.
("Bob" "is" "big" "-")
int1