Anne is blue. Bob is white. Charlie is big. Charlie is kind. Charlie is white. Harry is kind. Harry is nice. All green people are white. Blue people are nice. If Harry is rough and Harry is white then Harry is nice. If someone is nice then they are kind. If Anne is kind then Anne is green. All kind people are blue. If someone is nice and white then they are rough. If Charlie is rough then Charlie is green.
Anne is blue.
("Anne" "is" "blue" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
All green people are white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
Blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If Harry is rough and Harry is white then Harry is nice.
((("Harry" "is" "rough" "+") ("Harry" "is" "white" "+")) -> ("Harry" "is" "nice" "+"))
If someone is nice then they are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If Anne is kind then Anne is green.
((("Anne" "is" "kind" "+")) -> ("Anne" "is" "green" "+"))
All kind people are blue.
((("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
If someone is nice and white then they are rough.
((("someone" "is" "nice" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
If Charlie is rough then Charlie is green.
((("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "green" "+"))
Harry is nice.
True
1
proof
[(triple7 OR ((((triple6) -> rule6)) -> rule2))]
("Harry" "is" "nice" "+")
triple7
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Charlie is not white.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "white" "-")
triple5
Harry is blue.
True
2
proof
[(((triple6) -> rule6) OR ((((triple7) -> rule4)) -> rule6))]
("Harry" "is" "blue" "+")
((triple6) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Anne is not nice.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "nice" "-")
((triple1) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Charlie is nice.
True
3
proof
[(((((triple4) -> rule6)) -> rule2))]
("Charlie" "is" "nice" "+")
((((triple4) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is not nice.
False
3
inv-proof
[(((((triple4) -> rule6)) -> rule2))]
("Charlie" "is" "nice" "-")
((((triple4) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Anne is green.
True
4
proof
[(((((((triple1) -> rule2)) -> rule4)) -> rule5))]
("Anne" "is" "green" "+")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Charlie is not rough.
False
5
inv-proof
[(((((((triple4) -> rule6)) -> rule2) triple5) -> rule7))]
("Charlie" "is" "rough" "-")
((((((triple4) -> (rule6 % int3))) -> (rule2 % int2)) triple5) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is green.
True
6
proof
[(((((((((triple4) -> rule6)) -> rule2) triple5) -> rule7)) -> rule8))]
("Charlie" "is" "green" "+")
((((((((triple4) -> (rule6 % int4))) -> (rule2 % int3)) triple5) -> (rule7 % int2))) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Anne is not white.
False
5
inv-proof
[(((((((((triple1) -> rule2)) -> rule4)) -> rule5)) -> rule1))]
("Anne" "is" "white" "-")
((((((((triple1) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Anne is rough.
True
8
proof
[(((((triple1) -> rule2) ((((((((triple1) -> rule2)) -> rule4)) -> rule5)) -> rule1)) -> rule7))]
("Anne" "is" "rough" "+")
((((triple1) -> (rule2 % int5)) ((((((((triple1) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
int5
Anne is not rough.
False
8
inv-proof
[(((((triple1) -> rule2) ((((((((triple1) -> rule2)) -> rule4)) -> rule5)) -> rule1)) -> rule7))]
("Anne" "is" "rough" "-")
((((triple1) -> (rule2 % int5)) ((((((((triple1) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
int5
Bob is not nice.
Unknown
inv-rconc
[@3: Bob is nice.[CWA. Example of deepest failure = (rule2 <- rule6 <- rule4 <- FAIL)]]
("Bob" "is" "nice" "-")
Harry is rough.
Unknown
rconc
[@2: Harry is rough.[CWA. Example of deepest failure = (rule7 <- rule1 <- FAIL)]]
("Harry" "is" "rough" "+")
Bob is not blue.
Unknown
inv-rconc
[@3: Bob is blue.[CWA. Example of deepest failure = (rule6 <- rule4 <- rule2 <- FAIL)]]
("Bob" "is" "blue" "-")
Harry is white.
Unknown
rconc
[@1: Harry is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "white" "+")
Bob is not kind.
Unknown
inv-rconc
[@3: Bob is kind.[CWA. Example of deepest failure = (rule4 <- rule2 <- rule6 <- FAIL)]]
("Bob" "is" "kind" "-")
Bob is rough.
Unknown
rconc
[@4: Bob is rough.[CWA. Example of deepest failure = (rule7 <- rule2 <- rule6 <- rule4 <- FAIL)]]
("Bob" "is" "rough" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
Harry is not green.
Unknown
inv-random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is blue.[(triple1)] Bob is white.[(triple2)] Charlie is big.[(triple3)] Charlie is kind.[(triple4)] Charlie is white.[(triple5)] Harry is kind.[(triple6 OR ((triple7) -> rule4))] Harry is nice.[(triple7 OR ((((triple6) -> rule6)) -> rule2))] @1: Anne is nice.[(((triple1) -> rule2))] Charlie is blue.[(((triple4) -> rule6))] Harry is blue.[(((triple6) -> rule6) OR ((((triple7) -> rule4)) -> rule6))] @2: Anne is kind.[(((((triple1) -> rule2)) -> rule4))] Charlie is nice.[(((((triple4) -> rule6)) -> rule2))] @3: Anne is green.[(((((((triple1) -> rule2)) -> rule4)) -> rule5))] Charlie is rough.[(((((((triple4) -> rule6)) -> rule2) triple5) -> rule7))] @4: Anne is white.[(((((((((triple1) -> rule2)) -> rule4)) -> rule5)) -> rule1))] Charlie is green.[(((((((((triple4) -> rule6)) -> rule2) triple5) -> rule7)) -> rule8))] @5: Anne is rough.[(((((triple1) -> rule2) ((((((((triple1) -> rule2)) -> rule4)) -> rule5)) -> rule1)) -> rule7))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is white.
("Charlie" "is" "white" "+")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple6
((triple7) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple7
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple4) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple6) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((((triple7) -> (rule4 % int2))) -> (rule6 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple4) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
((((((triple4) -> (rule6 % int3))) -> (rule2 % int2)) triple5) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
((((((((triple1) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
int4
Charlie is green.
("Charlie" "is" "green" "+")
((((((((triple4) -> (rule6 % int4))) -> (rule2 % int3)) triple5) -> (rule7 % int2))) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
int4
Anne is rough.
("Anne" "is" "rough" "+")
((((triple1) -> (rule2 % int5)) ((((((((triple1) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
int4
Anne is nice.
("Anne" "is" "nice" "+")
int5