Bob is green. Harry is cold. Young, cold people are big. If someone is cold and white then they are big. If someone is green and not cold then they are white. If someone is white and not quiet then they are not green. Cold people are young. If someone is big and not kind then they are not young.
Bob is green.
("Bob" "is" "green" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Young, cold people are big.
((("someone" "is" "young" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
If someone is cold and white then they are big.
((("someone" "is" "cold" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If someone is green and not cold then they are white.
((("someone" "is" "green" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "white" "+"))
If someone is white and not quiet then they are not green.
((("someone" "is" "white" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "green" "-"))
Cold people are young.
((("someone" "is" "cold" "+")) -> ("someone" "is" "young" "+"))
If someone is big and not kind then they are not young.
((("someone" "is" "big" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "young" "-"))
Harry is cold.
True
1
proof
[(triple2)]
("Harry" "is" "cold" "+")
triple2
Harry is not cold.
False
1
inv-proof
[(triple2)]
("Harry" "is" "cold" "-")
triple2
Harry is young.
True
2
proof
[(((triple2) -> rule5))]
("Harry" "is" "young" "+")
((triple2) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is not young.
False
2
inv-proof
[(((triple2) -> rule5))]
("Harry" "is" "young" "-")
((triple2) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is big.
True
4
proof
[(((((triple2) -> rule5) triple2) -> rule1))]
("Harry" "is" "big" "+")
((((triple2) -> (rule5 % int2)) triple2) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is not big.
False
4
inv-proof
[(((((triple2) -> rule5) triple2) -> rule1))]
("Harry" "is" "big" "-")
((((triple2) -> (rule5 % int2)) triple2) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Bob is not white.
Unknown
inv-rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "white" "-")
Harry is white.
Unknown
rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "white" "+")
Bob is not young.
Unknown
inv-rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "young" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Bob is green.[(triple1)] Harry is cold.[(triple2)] @1: Harry is young.[(((triple2) -> rule5))] @2: Harry is big.[(((((triple2) -> rule5) triple2) -> rule1))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Harry is cold.
("Harry" "is" "cold" "+")
triple2
Harry is young.
("Harry" "is" "young" "+")
((triple2) -> (rule5 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((((triple2) -> (rule5 % int2)) triple2) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2