Bob is big. Bob is nice. Bob is young. Dave is blue. Dave is green. Dave is smart. Gary is kind. Gary is young. Harry is nice. Harry is young. Nice people are young. Nice people are smart. If Gary is blue and Gary is smart then Gary is big. If someone is green and young then they are smart. All nice people are young. If Bob is big and Bob is blue then Bob is green. If Gary is green and Gary is kind then Gary is smart. Green people are blue.
Bob is big.
("Bob" "is" "big" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is young.
("Harry" "is" "young" "+")
Nice people are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
Nice people are smart.
((("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If Gary is blue and Gary is smart then Gary is big.
((("Gary" "is" "blue" "+") ("Gary" "is" "smart" "+")) -> ("Gary" "is" "big" "+"))
If someone is green and young then they are smart.
((("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
All nice people are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
If Bob is big and Bob is blue then Bob is green.
((("Bob" "is" "big" "+") ("Bob" "is" "blue" "+")) -> ("Bob" "is" "green" "+"))
If Gary is green and Gary is kind then Gary is smart.
((("Gary" "is" "green" "+") ("Gary" "is" "kind" "+")) -> ("Gary" "is" "smart" "+"))
Green people are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
Dave is smart.
True
1
proof
[(triple6)]
("Dave" "is" "smart" "+")
triple6
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Harry is smart.
True
2
proof
[(((triple9) -> rule2))]
("Harry" "is" "smart" "+")
((triple9) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Bob is not smart.
False
2
inv-proof
[(((triple2) -> rule2))]
("Bob" "is" "smart" "-")
((triple2) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "blue" "-")
Harry is blue.
Unknown
rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Harry" "is" "blue" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
@0: Bob is big.[(triple1)] Bob is nice.[(triple2)] Bob is young.[(triple3 OR ((triple2) -> rule1) OR ((triple2) -> rule5))] Dave is blue.[(triple4 OR ((triple5) -> rule8))] Dave is green.[(triple5)] Dave is smart.[(triple6)] Gary is kind.[(triple7)] Gary is young.[(triple8)] Harry is nice.[(triple9)] Harry is young.[(triple10 OR ((triple9) -> rule1) OR ((triple9) -> rule5))] @1: Bob is smart.[(((triple2) -> rule2))] Harry is smart.[(((triple9) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is young.
("Bob" "is" "young" "+")
triple3
((triple2) -> (rule1 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((triple2) -> (rule5 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
triple4
((triple5) -> (rule8 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
triple5
Dave is smart.
("Dave" "is" "smart" "+")
triple6
Gary is kind.
("Gary" "is" "kind" "+")
triple7
Gary is young.
("Gary" "is" "young" "+")
triple8
Harry is nice.
("Harry" "is" "nice" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
((triple9) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple9) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple2) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple9) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1