Bob is big. Charlie is blue. Gary is smart. If someone is white then they are kind. All smart people are nice. All big people are smart.
Bob is big.
("Bob" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If someone is white then they are kind.
((("someone" "is" "white" "+")) -> ("someone" "is" "kind" "+"))
All smart people are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
All big people are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Charlie is not blue.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "blue" "-")
triple2
Bob is smart.
True
2
proof
[(((triple1) -> rule3))]
("Bob" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not smart.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "smart" "-")
((triple1) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is nice.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Bob" "is" "nice" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not nice.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("Bob" "is" "nice" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "smart" "-")
Gary is kind.
Unknown
rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "kind" "+")
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Bob is big.[(triple1)] Charlie is blue.[(triple2)] Gary is smart.[(triple3)] @1: Bob is smart.[(((triple1) -> rule3))] Gary is nice.[(((triple3) -> rule2))] @2: Bob is nice.[(((((triple1) -> rule3)) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Gary is smart.
("Gary" "is" "smart" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple3) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2