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