Bob is young. Gary is big. Harry is young. If Bob is young then Bob is smart. All big things are smart. If something is young and smart then it is blue.
Bob is young.
("Bob" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Harry is young.
("Harry" "is" "young" "+")
If Bob is young then Bob is smart.
((("Bob" "is" "young" "+")) -> ("Bob" "is" "smart" "+"))
All big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
If something is young and smart then it is blue.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "blue" "+"))
Harry is young.
True
1
proof
[(triple3)]
("Harry" "is" "young" "+")
triple3
Harry is not young.
False
1
inv-proof
[(triple3)]
("Harry" "is" "young" "-")
triple3
Bob is smart.
True
2
proof
[(((triple1) -> rule1))]
("Bob" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is not smart.
False
2
inv-proof
[(((triple1) -> rule1))]
("Bob" "is" "smart" "-")
((triple1) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule3))]
("Bob" "is" "blue" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not blue.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule3))]
("Bob" "is" "blue" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "blue" "-")
Harry is smart.
Unknown
rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "smart" "+")
Harry is not blue.
Unknown
inv-rconc
[@2: Harry is blue.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Harry" "is" "blue" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Bob is young.[(triple1)] Gary is big.[(triple2)] Harry is young.[(triple3)] @1: Bob is smart.[(((triple1) -> rule1))] Gary is smart.[(((triple2) -> rule2))] @2: Bob is blue.[(((triple1 ((triple1) -> rule1)) -> rule3))]
Bob is young.
("Bob" "is" "young" "+")
triple1
Gary is big.
("Gary" "is" "big" "+")
triple2
Harry is young.
("Harry" "is" "young" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple2) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2