Bob is big. Bob is blue. Bob is not green. Bob is nice. Bob is smart. Bob is not white. Charlie is big. Charlie is blue. Charlie is green. Charlie is nice. Charlie is smart. Charlie is white. Gary is blue. Gary is green. Gary is nice. Gary is smart. All green, blue people are young. If someone is big and not white then they are blue. If someone is young then they are big.
Bob is big.
("Bob" "is" "big" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is not green.
("Bob" "is" "green" "-")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is not white.
("Bob" "is" "white" "-")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is smart.
("Gary" "is" "smart" "+")
All green, blue people are young.
((("someone" "is" "green" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
If someone is big and not white then they are blue.
((("someone" "is" "big" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "blue" "+"))
If someone is young then they are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
Charlie is smart.
True
1
proof
[(triple11)]
("Charlie" "is" "smart" "+")
triple11
Bob is white.
False
1
inv-proof
[(triple6)]
("Bob" "is" "white" "+")
triple6
Gary is young.
True
3
proof
[(((triple14 triple13) -> rule1))]
("Gary" "is" "young" "+")
((triple14 triple13) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is not young.
False
3
inv-proof
[(((triple14 triple13) -> rule1))]
("Gary" "is" "young" "-")
((triple14 triple13) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is big.
True
4
proof
[(((((triple14 triple13) -> rule1)) -> rule3))]
("Gary" "is" "big" "+")
((((triple14 triple13) -> (rule1 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is not big.
False
4
inv-proof
[(((((triple14 triple13) -> rule1)) -> rule3))]
("Gary" "is" "big" "-")
((((triple14 triple13) -> (rule1 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Bob is not young.
Unknown
inv-rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "young" "-")
Gary is white.
Unknown
random
[@0: Gary is white.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "white" "+")
@0: Bob is big.[(triple1)] Bob is blue.[(triple2 OR ((triple1 triple6) -> rule2))] Bob is nice.[(triple4)] Bob is not green.[(triple3)] Bob is not white.[(triple6)] Bob is smart.[(triple5)] Charlie is big.[(triple7 OR ((((triple9 triple8) -> rule1)) -> rule3))] Charlie is blue.[(triple8)] Charlie is green.[(triple9)] Charlie is nice.[(triple10)] Charlie is smart.[(triple11)] Charlie is white.[(triple12)] Gary is blue.[(triple13)] Gary is green.[(triple14)] Gary is nice.[(triple15)] Gary is smart.[(triple16)] @1: Charlie is young.[(((triple9 triple8) -> rule1))] Gary is young.[(((triple14 triple13) -> rule1))] @2: Gary is big.[(((((triple14 triple13) -> rule1)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is blue.
("Bob" "is" "blue" "+")
triple2
((triple1 triple6) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple4
Bob is not green.
("Bob" "is" "green" "-")
triple3
Bob is not white.
("Bob" "is" "white" "-")
triple6
Bob is smart.
("Bob" "is" "smart" "+")
triple5
Charlie is big.
("Charlie" "is" "big" "+")
triple7
((((triple9 triple8) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple8
Charlie is green.
("Charlie" "is" "green" "+")
triple9
Charlie is nice.
("Charlie" "is" "nice" "+")
triple10
Charlie is smart.
("Charlie" "is" "smart" "+")
triple11
Charlie is white.
("Charlie" "is" "white" "+")
triple12
Gary is blue.
("Gary" "is" "blue" "+")
triple13
Gary is green.
("Gary" "is" "green" "+")
triple14
Gary is nice.
("Gary" "is" "nice" "+")
triple15
Gary is smart.
("Gary" "is" "smart" "+")
triple16
Charlie is young.
("Charlie" "is" "young" "+")
((triple9 triple8) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((triple14 triple13) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
((((triple14 triple13) -> (rule1 % int2))) -> (rule3 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2