Bob is cold. Bob is green. Bob is smart. Gary is cold. Gary is green. Gary is kind. Gary is smart. Gary is white. Harry is green. Harry is kind. Harry is red. Harry is young. Young, kind people are white. Kind, white people are young. All red, green people are kind. Young, smart people are kind. If someone is kind and green then they are red. All white, kind people are green.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
Young, kind people are white.
((("someone" "is" "young" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
Kind, white people are young.
((("someone" "is" "kind" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "young" "+"))
All red, green people are kind.
((("someone" "is" "red" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
Young, smart people are kind.
((("someone" "is" "young" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "kind" "+"))
If someone is kind and green then they are red.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
All white, kind people are green.
((("someone" "is" "white" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
Bob is green.
True
1
proof
[(triple2)]
("Bob" "is" "green" "+")
triple2
Gary is not smart.
False
1
inv-proof
[(triple7)]
("Gary" "is" "smart" "-")
triple7
Bob is not white.
Unknown
inv-rconc
[@2: Bob is white.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Bob" "is" "white" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Bob is cold.[(triple1)] Bob is green.[(triple2)] Bob is smart.[(triple3)] Gary is cold.[(triple4)] Gary is green.[(triple5 OR ((triple8 triple6) -> rule6))] Gary is kind.[(triple6)] Gary is smart.[(triple7)] Gary is white.[(triple8)] Harry is green.[(triple9 OR ((((triple12 triple10) -> rule1) triple10) -> rule6))] Harry is kind.[(triple10 OR ((triple11 triple9) -> rule3))] Harry is red.[(triple11 OR ((triple10 triple9) -> rule5) OR ((triple10 ((((triple12 triple10) -> rule1) triple10) -> rule6)) -> rule5))] Harry is young.[(triple12)] @1: Gary is red.[(((triple6 triple5) -> rule5) OR ((triple6 ((triple8 triple6) -> rule6)) -> rule5))] Gary is young.[(((triple6 triple8) -> rule2))] Harry is white.[(((triple12 triple10) -> rule1) OR ((triple12 ((triple11 triple9) -> rule3)) -> rule1))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Gary is cold.
("Gary" "is" "cold" "+")
triple4
Gary is green.
("Gary" "is" "green" "+")
triple5
((triple8 triple6) -> (rule6 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
triple6
Gary is smart.
("Gary" "is" "smart" "+")
triple7
Gary is white.
("Gary" "is" "white" "+")
triple8
Harry is green.
("Harry" "is" "green" "+")
triple9
((((triple12 triple10) -> (rule1 % int2)) triple10) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
triple10
((triple11 triple9) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple11
((triple10 triple9) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple10 ((((triple12 triple10) -> (rule1 % int3)) triple10) -> (rule6 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
triple12
Gary is red.
("Gary" "is" "red" "+")
((triple6 triple5) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
((triple6 ((triple8 triple6) -> (rule6 % int2))) -> (rule5 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
int2
Gary is young.
("Gary" "is" "young" "+")
((triple6 triple8) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple12 triple10) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple12 ((triple11 triple9) -> (rule3 % int2))) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2