Bob is big. Bob is smart. Bob is white. Bob is young. Gary is big. Gary is nice. Gary is not quiet. Nice, smart things are white. If something is smart and green then it is quiet. If something is big then it is smart.
Bob is big.
("Bob" "is" "big" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is not quiet.
("Gary" "is" "quiet" "-")
Nice, smart things are white.
((("something" "is" "nice" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If something is smart and green then it is quiet.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "quiet" "+"))
If something is big then it is smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
Gary is nice.
True
1
proof
[(triple6)]
("Gary" "is" "nice" "+")
triple6
Gary is not big.
False
1
inv-proof
[(triple5)]
("Gary" "is" "big" "-")
triple5
Gary is smart.
True
2
proof
[(((triple5) -> rule3))]
("Gary" "is" "smart" "+")
((triple5) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not smart.
False
2
inv-proof
[(((triple5) -> rule3))]
("Gary" "is" "smart" "-")
((triple5) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
True
4
proof
[(((triple6 ((triple5) -> rule3)) -> rule1))]
("Gary" "is" "white" "+")
((triple6 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not white.
False
4
inv-proof
[(((triple6 ((triple5) -> rule3)) -> rule1))]
("Gary" "is" "white" "-")
((triple6 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "quiet" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Bob is big.[(triple1)] Bob is smart.[(triple2 OR ((triple1) -> rule3))] Bob is white.[(triple3)] Bob is young.[(triple4)] Gary is big.[(triple5)] Gary is nice.[(triple6)] Gary is not quiet.[(triple7)] @1: Gary is smart.[(((triple5) -> rule3))] @2: Gary is white.[(((triple6 ((triple5) -> rule3)) -> rule1))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is smart.
("Bob" "is" "smart" "+")
triple2
((triple1) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
Gary is big.
("Gary" "is" "big" "+")
triple5
Gary is nice.
("Gary" "is" "nice" "+")
triple6
Gary is not quiet.
("Gary" "is" "quiet" "-")
triple7
Gary is smart.
("Gary" "is" "smart" "+")
((triple5) -> (rule3 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple6 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2