Bob is round. Harry is nice. Harry is young. If someone is blue then they are round. If someone is blue and smart then they are rough. Young people are nice. All nice people are smart. Rough people are young. All blue, cold people are young.
Bob is round.
("Bob" "is" "round" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is blue then they are round.
((("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
If someone is blue and smart then they are rough.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
Young people are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
All nice people are smart.
((("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
Rough people are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
All blue, cold people are young.
((("someone" "is" "blue" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
Harry is young.
True
1
proof
[(triple3)]
("Harry" "is" "young" "+")
triple3
Bob is not round.
False
1
inv-proof
[(triple1)]
("Bob" "is" "round" "-")
triple1
Harry is smart.
True
2
proof
[(((triple2) -> rule4) OR ((((triple3) -> rule3)) -> rule4))]
("Harry" "is" "smart" "+")
((triple2) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not smart.
False
2
inv-proof
[(((triple2) -> rule4) OR ((((triple3) -> rule3)) -> rule4))]
("Harry" "is" "smart" "-")
((triple2) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Bob is not smart.
Unknown
inv-rconc
[@4: Bob is smart.[CWA. Example of deepest failure = (rule4 <- rule3 <- rule5 <- rule2 <- FAIL)]]
("Bob" "is" "smart" "-")
Bob is young.
Unknown
rconc
[@2: Bob is young.[CWA. Example of deepest failure = (rule5 <- rule2 <- FAIL)]]
("Bob" "is" "young" "+")
Harry is not blue.
Unknown
inv-random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is round.[(triple1)] Harry is nice.[(triple2 OR ((triple3) -> rule3))] Harry is young.[(triple3)] @1: Harry is smart.[(((triple2) -> rule4) OR ((((triple3) -> rule3)) -> rule4))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Harry is nice.
("Harry" "is" "nice" "+")
triple2
((triple3) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple3
Harry is smart.
("Harry" "is" "smart" "+")
((triple2) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2