Charlie is red. Harry is young. If someone is white and big then they are not young. If Charlie is red then Charlie is quiet. White people are big. Red people are white. If someone is quiet then they are white. White people are red.
Charlie is red.
("Charlie" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
If someone is white and big then they are not young.
((("someone" "is" "white" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "-"))
If Charlie is red then Charlie is quiet.
((("Charlie" "is" "red" "+")) -> ("Charlie" "is" "quiet" "+"))
White people are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
Red people are white.
((("someone" "is" "red" "+")) -> ("someone" "is" "white" "+"))
If someone is quiet then they are white.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
White people are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
Harry is young.
True
1
proof
[(triple2)]
("Harry" "is" "young" "+")
triple2
Harry is not young.
False
1
inv-proof
[(triple2)]
("Harry" "is" "young" "-")
triple2
Charlie is white.
True
2
proof
[(((triple1) -> rule4) OR ((((triple1) -> rule2)) -> rule5))]
("Charlie" "is" "white" "+")
((triple1) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is not quiet.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "quiet" "-")
((triple1) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is big.
True
3
proof
[(((((triple1) -> rule4)) -> rule3) OR ((((((triple1) -> rule2)) -> rule5)) -> rule3))]
("Charlie" "is" "big" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is not big.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule3) OR ((((((triple1) -> rule2)) -> rule5)) -> rule3))]
("Charlie" "is" "big" "-")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is not young.
True
6
proof
[(((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule3)) -> rule1) OR ((((((triple1) -> rule2)) -> rule5) ((((triple1) -> rule4)) -> rule3)) -> rule1) OR ((((triple1) -> rule4) ((((((triple1) -> rule2)) -> rule5)) -> rule3)) -> rule1) OR ((((((triple1) -> rule2)) -> rule5) ((((((triple1) -> rule2)) -> rule5)) -> rule3)) -> rule1))]
("Charlie" "is" "young" "-")
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((((triple1) -> (rule2 % int4))) -> (rule5 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
((((triple1) -> (rule4 % int4)) ((((((triple1) -> (rule2 % int3))) -> (rule5 % int4))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
((((((triple1) -> (rule2 % int4))) -> (rule5 % int3)) ((((((triple1) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Charlie is young.
False
6
inv-proof
[(((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule3)) -> rule1) OR ((((((triple1) -> rule2)) -> rule5) ((((triple1) -> rule4)) -> rule3)) -> rule1) OR ((((triple1) -> rule4) ((((((triple1) -> rule2)) -> rule5)) -> rule3)) -> rule1) OR ((((((triple1) -> rule2)) -> rule5) ((((((triple1) -> rule2)) -> rule5)) -> rule3)) -> rule1))]
("Charlie" "is" "young" "+")
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((((triple1) -> (rule2 % int4))) -> (rule5 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
((((triple1) -> (rule4 % int4)) ((((((triple1) -> (rule2 % int3))) -> (rule5 % int4))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
((((((triple1) -> (rule2 % int4))) -> (rule5 % int3)) ((((((triple1) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
Harry is not red.
Unknown
inv-rconc
[@2: Harry is red.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Harry" "is" "red" "-")
Harry is big.
Unknown
rconc
[@4: Harry is big.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule6 <- rule5 <- FAIL)]]
("Harry" "is" "big" "+")
Harry is not white.
Unknown
inv-rconc
[@3: Harry is white.[CWA. Example of deepest failure = (rule4 <- rule6 <- rule5 <- FAIL)]]
("Harry" "is" "white" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Charlie is rough.
Unknown
random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "+")
@0: Charlie is red.[(triple1)] Harry is young.[(triple2)] @1: Charlie is quiet.[(((triple1) -> rule2))] Charlie is white.[(((triple1) -> rule4) OR ((((triple1) -> rule2)) -> rule5))] @2: Charlie is big.[(((((triple1) -> rule4)) -> rule3) OR ((((((triple1) -> rule2)) -> rule5)) -> rule3))] @3: Charlie is not young.[(((((triple1) -> rule4) ((((triple1) -> rule4)) -> rule3)) -> rule1) OR ((((((triple1) -> rule2)) -> rule5) ((((triple1) -> rule4)) -> rule3)) -> rule1) OR ((((triple1) -> rule4) ((((((triple1) -> rule2)) -> rule5)) -> rule3)) -> rule1) OR ((((((triple1) -> rule2)) -> rule5) ((((((triple1) -> rule2)) -> rule5)) -> rule3)) -> rule1))]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Harry is young.
("Harry" "is" "young" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple1) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple1) -> (rule4 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is not young.
("Charlie" "is" "young" "-")
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
((((((triple1) -> (rule2 % int4))) -> (rule5 % int3)) ((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4
((((triple1) -> (rule4 % int4)) ((((((triple1) -> (rule2 % int3))) -> (rule5 % int4))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
int4
((((((triple1) -> (rule2 % int4))) -> (rule5 % int3)) ((((((triple1) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is not young.
("Charlie" "is" "young" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int4