Anne is nice. Anne is white. Bob is green. Bob is smart. Bob is white. Gary is blue. Gary is furry. Harry is nice. Harry is white. Harry is young. If something is white and smart then it is green. If Anne is smart then Anne is young. White, young things are smart. All nice things are white. If Harry is smart and Harry is green then Harry is nice. If something is nice then it is white.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is white and smart then it is green.
((("something" "is" "white" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If Anne is smart then Anne is young.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "young" "+"))
White, young things are smart.
((("something" "is" "white" "+") ("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
All nice things are white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If Harry is smart and Harry is green then Harry is nice.
((("Harry" "is" "smart" "+") ("Harry" "is" "green" "+")) -> ("Harry" "is" "nice" "+"))
If something is nice then it is white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
Gary is furry.
True
1
proof
[(triple7)]
("Gary" "is" "furry" "+")
triple7
Bob is not white.
False
1
inv-proof
[(triple5)]
("Bob" "is" "white" "-")
triple5
Anne is not smart.
Unknown
inv-rconc
[@2: Anne is smart.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Anne" "is" "smart" "-")
Gary is nice.
Unknown
random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "+")
@0: Anne is nice.[(triple1)] Anne is white.[(triple2 OR ((triple1) -> rule4) OR ((triple1) -> rule6))] Bob is green.[(triple3 OR ((triple5 triple4) -> rule1))] Bob is smart.[(triple4)] Bob is white.[(triple5)] Gary is blue.[(triple6)] Gary is furry.[(triple7)] Harry is nice.[(triple8 OR ((((triple9 triple10) -> rule3) ((triple9 ((triple9 triple10) -> rule3)) -> rule1)) -> rule5))] Harry is white.[(triple9 OR ((triple8) -> rule4) OR ((triple8) -> rule6))] Harry is young.[(triple10)] @1: Harry is smart.[(((triple9 triple10) -> rule3) OR ((((triple8) -> rule4) triple10) -> rule3) OR ((((triple8) -> rule6) triple10) -> rule3))] @2: Harry is green.[(((triple9 ((triple9 triple10) -> rule3)) -> rule1) OR ((((triple8) -> rule4) ((triple9 triple10) -> rule3)) -> rule1) OR ((((triple8) -> rule6) ((triple9 triple10) -> rule3)) -> rule1) OR ((triple9 ((((triple8) -> rule4) triple10) -> rule3)) -> rule1) OR ((triple9 ((((triple8) -> rule6) triple10) -> rule3)) -> rule1) OR ((((triple8) -> rule4) ((((triple8) -> rule4) triple10) -> rule3)) -> rule1) OR ((((triple8) -> rule4) ((((triple8) -> rule6) triple10) -> rule3)) -> rule1) OR ((((triple8) -> rule6) ((((triple8) -> rule4) triple10) -> rule3)) -> rule1) OR ((((triple8) -> rule6) ((((triple8) -> rule6) triple10) -> rule3)) -> rule1))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
((triple1) -> (rule4 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((triple1) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
triple3
((triple5 triple4) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Bob is white.
("Bob" "is" "white" "+")
triple5
Gary is blue.
("Gary" "is" "blue" "+")
triple6
Gary is furry.
("Gary" "is" "furry" "+")
triple7
Harry is nice.
("Harry" "is" "nice" "+")
triple8
((((triple9 triple10) -> (rule3 % int3)) ((triple9 ((triple9 triple10) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
triple9
((triple8) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((triple8) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple10
Harry is smart.
("Harry" "is" "smart" "+")
((triple9 triple10) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
((((triple8) -> (rule4 % int2)) triple10) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple8) -> (rule6 % int2)) triple10) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((triple9 ((triple9 triple10) -> (rule3 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
((((triple8) -> (rule4 % int3)) ((triple9 triple10) -> (rule3 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((triple8) -> (rule6 % int3)) ((triple9 triple10) -> (rule3 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((triple9 ((((triple8) -> (rule4 % int3)) triple10) -> (rule3 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((triple9 ((((triple8) -> (rule6 % int3)) triple10) -> (rule3 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((triple8) -> (rule4 % int3)) ((((triple8) -> (rule4 % int3)) triple10) -> (rule3 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((triple8) -> (rule4 % int3)) ((((triple8) -> (rule6 % int3)) triple10) -> (rule3 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((triple8) -> (rule6 % int3)) ((((triple8) -> (rule4 % int3)) triple10) -> (rule3 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3
((((triple8) -> (rule6 % int3)) ((((triple8) -> (rule6 % int3)) triple10) -> (rule3 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
int3