Bob is nice. Charlie is green. Charlie is young. Gary is kind. Harry is kind. Harry is nice. Harry is white. Green, smart things are white. White things are green. Kind things are white.
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is white.
("Harry" "is" "white" "+")
Green, smart things are white.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
White things are green.
((("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
Kind things are white.
((("something" "is" "kind" "+")) -> ("something" "is" "white" "+"))
Harry is kind.
True
1
proof
[(triple5)]
("Harry" "is" "kind" "+")
triple5
Harry is not nice.
False
1
inv-proof
[(triple6)]
("Harry" "is" "nice" "-")
triple6
Harry is green.
True
2
proof
[(((triple7) -> rule2) OR ((((triple5) -> rule3)) -> rule2))]
("Harry" "is" "green" "+")
((triple7) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not green.
False
2
inv-proof
[(((triple7) -> rule2) OR ((((triple5) -> rule3)) -> rule2))]
("Harry" "is" "green" "-")
((triple7) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Gary is green.
True
3
proof
[(((((triple4) -> rule3)) -> rule2))]
("Gary" "is" "green" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not green.
False
3
inv-proof
[(((((triple4) -> rule3)) -> rule2))]
("Gary" "is" "green" "-")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "white" "-")
Bob is white.
Unknown
rconc
[@1: Bob is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "white" "+")
Bob is not green.
Unknown
inv-rconc
[@2: Bob is green.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Bob" "is" "green" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Bob is nice.[(triple1)] Charlie is green.[(triple2)] Charlie is young.[(triple3)] Gary is kind.[(triple4)] Harry is kind.[(triple5)] Harry is nice.[(triple6)] Harry is white.[(triple7 OR ((triple5) -> rule3))] @1: Gary is white.[(((triple4) -> rule3))] Harry is green.[(((triple7) -> rule2) OR ((((triple5) -> rule3)) -> rule2))] @2: Gary is green.[(((((triple4) -> rule3)) -> rule2))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
triple4
Harry is kind.
("Harry" "is" "kind" "+")
triple5
Harry is nice.
("Harry" "is" "nice" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
((triple5) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple4) -> (rule3 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple7) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Gary is green.
("Gary" "is" "green" "+")
((((triple4) -> (rule3 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2