Bob is kind. Charlie is nice. Harry is kind. Big things are kind. Kind things are green. Green things are big. If something is young and green then it is big. If Harry is nice then Harry is big. Round, young things are not white. Green things are white. If something is white and not kind then it is not round.
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Big things are kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
Kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
Green things are big.
((("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If something is young and green then it is big.
((("something" "is" "young" "+") ("something" "is" "green" "+")) -> ("something" "is" "big" "+"))
If Harry is nice then Harry is big.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "big" "+"))
Round, young things are not white.
((("something" "is" "round" "+") ("something" "is" "young" "+")) -> ("something" "is" "white" "-"))
Green things are white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If something is white and not kind then it is not round.
((("something" "is" "white" "+") ("something" "is" "kind" "~")) -> ("something" "is" "round" "-"))
Charlie is nice.
True
1
proof
[(triple2)]
("Charlie" "is" "nice" "+")
triple2
Charlie is not nice.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "nice" "-")
triple2
Bob is green.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "green" "+")
((triple1) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple3) -> rule2))]
("Harry" "is" "green" "-")
((triple3) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Bob is big.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Bob" "is" "big" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Harry is not white.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule7))]
("Harry" "is" "white" "-")
((((triple3) -> (rule2 % int2))) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Charlie is not white.
Unknown
inv-rconc
[@4: Charlie is white.[CWA. Example of deepest failure = (rule7 <- rule2 <- rule1 <- rule3 <- FAIL)]]
("Charlie" "is" "white" "-")
Charlie is green.
Unknown
rconc
[@3: Charlie is green.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule3 <- FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not big.
Unknown
inv-rconc
[@4: Charlie is big.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule1 <- rule4 <- FAIL)]]
("Charlie" "is" "big" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Bob is nice.
Unknown
random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "+")
@0: Bob is kind.[(triple1)] Charlie is nice.[(triple2)] Harry is kind.[(triple3)] @1: Bob is green.[(((triple1) -> rule2))] Harry is green.[(((triple3) -> rule2))] @2: Bob is big.[(((((triple1) -> rule2)) -> rule3))] Bob is white.[(((((triple1) -> rule2)) -> rule7))] Harry is big.[(((((triple3) -> rule2)) -> rule3))] Harry is white.[(((((triple3) -> rule2)) -> rule7))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Harry is kind.
("Harry" "is" "kind" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple3) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
((((triple1) -> (rule2 % int2))) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((((triple3) -> (rule2 % int2))) -> (rule7 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2