Bob is blue. Bob is furry. Bob is not young. Harry is blue. Harry is not cold. Harry is not furry. Harry is green. Green people are blue. Blue people are not cold. If Bob is smart and Bob is quiet then Bob is green.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is not young.
("Bob" "is" "young" "-")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is not furry.
("Harry" "is" "furry" "-")
Harry is green.
("Harry" "is" "green" "+")
Green people are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
Blue people are not cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "-"))
If Bob is smart and Bob is quiet then Bob is green.
((("Bob" "is" "smart" "+") ("Bob" "is" "quiet" "+")) -> ("Bob" "is" "green" "+"))
Harry is blue.
True
1
proof
[(triple4 OR ((triple7) -> rule1))]
("Harry" "is" "blue" "+")
triple4
((triple7) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Bob is not blue.
False
1
inv-proof
[(triple1)]
("Bob" "is" "blue" "-")
triple1
Bob is not cold.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "cold" "-")
((triple1) -> (rule2 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Bob is cold.
False
2
inv-proof
[(((triple1) -> rule2))]
("Bob" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "green" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Bob is smart.
Unknown
random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "+")
@0: Bob is blue.[(triple1)] Bob is furry.[(triple2)] Bob is not young.[(triple3)] Harry is blue.[(triple4 OR ((triple7) -> rule1))] Harry is green.[(triple7)] Harry is not cold.[(triple5 OR ((triple4) -> rule2) OR ((((triple7) -> rule1)) -> rule2))] Harry is not furry.[(triple6)] @1: Bob is not cold.[(((triple1) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is not young.
("Bob" "is" "young" "-")
triple3
Harry is blue.
("Harry" "is" "blue" "+")
triple4
((triple7) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple7
Harry is not cold.
("Harry" "is" "cold" "-")
triple5
((triple4) -> (rule2 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not furry.
("Harry" "is" "furry" "-")
triple6
Bob is not cold.
("Bob" "is" "cold" "-")
((triple1) -> (rule2 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1