Bob is kind. Charlie is not kind. Charlie is nice. Charlie is rough. Gary is kind. Harry is kind. Harry is white. All rough, quiet things are nice. If something is smart then it is nice. If Gary is kind then Gary is red. All quiet things are rough. Nice things are red. Red things are quiet. Quiet, nice things are white. If something is smart and not red then it is white. Smart things are not white.
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is not kind.
("Charlie" "is" "kind" "-")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is white.
("Harry" "is" "white" "+")
All rough, quiet things are nice.
((("something" "is" "rough" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
If something is smart then it is nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
If Gary is kind then Gary is red.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "red" "+"))
All quiet things are rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
Nice things are red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
Red things are quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
Quiet, nice things are white.
((("something" "is" "quiet" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
If something is smart and not red then it is white.
((("something" "is" "smart" "+") ("something" "is" "red" "~")) -> ("something" "is" "white" "+"))
Smart things are not white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "-"))
Charlie is rough.
True
1
proof
[(triple4 OR ((((((triple3) -> rule5)) -> rule6)) -> rule4))]
("Charlie" "is" "rough" "+")
triple4
((((((triple3) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Harry is not kind.
False
1
inv-proof
[(triple6)]
("Harry" "is" "kind" "-")
triple6
Gary is red.
True
2
proof
[(((triple5) -> rule3))]
("Gary" "is" "red" "+")
((triple5) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Charlie is not red.
False
2
inv-proof
[(((triple3) -> rule5))]
("Charlie" "is" "red" "-")
((triple3) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Gary is quiet.
True
3
proof
[(((((triple5) -> rule3)) -> rule6))]
("Gary" "is" "quiet" "+")
((((triple5) -> (rule3 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is not quiet.
False
3
inv-proof
[(((((triple5) -> rule3)) -> rule6))]
("Gary" "is" "quiet" "-")
((((triple5) -> (rule3 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Charlie is white.
True
5
proof
[(((((((triple3) -> rule5)) -> rule6) triple3) -> rule7))]
("Charlie" "is" "white" "+")
((((((triple3) -> (rule5 % int3))) -> (rule6 % int2)) triple3) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Gary is not rough.
False
4
inv-proof
[(((((((triple5) -> rule3)) -> rule6)) -> rule4))]
("Gary" "is" "rough" "-")
((((((triple5) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is nice.
True
8
proof
[(((((((((triple5) -> rule3)) -> rule6)) -> rule4) ((((triple5) -> rule3)) -> rule6)) -> rule1))]
("Gary" "is" "nice" "+")
((((((((triple5) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule4 % int2)) ((((triple5) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Gary is not nice.
False
8
inv-proof
[(((((((((triple5) -> rule3)) -> rule6)) -> rule4) ((((triple5) -> rule3)) -> rule6)) -> rule1))]
("Gary" "is" "nice" "-")
((((((((triple5) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule4 % int2)) ((((triple5) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Gary is white.
True
12
proof
[(((((((triple5) -> rule3)) -> rule6) ((((((((triple5) -> rule3)) -> rule6)) -> rule4) ((((triple5) -> rule3)) -> rule6)) -> rule1)) -> rule7))]
("Gary" "is" "white" "+")
((((((triple5) -> (rule3 % int5))) -> (rule6 % int4)) ((((((((triple5) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule4 % int3)) ((((triple5) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule1 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
int5
Gary is not white.
False
12
inv-proof
[(((((((triple5) -> rule3)) -> rule6) ((((((((triple5) -> rule3)) -> rule6)) -> rule4) ((((triple5) -> rule3)) -> rule6)) -> rule1)) -> rule7))]
("Gary" "is" "white" "-")
((((((triple5) -> (rule3 % int5))) -> (rule6 % int4)) ((((((((triple5) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule4 % int3)) ((((triple5) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule1 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
int5
Bob is not rough.
Unknown
inv-rconc
[@4: Bob is rough.[CWA. Example of deepest failure = (rule4 <- rule6 <- rule5 <- rule1 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is quiet.
Unknown
rconc
[@3: Bob is quiet.[CWA. Example of deepest failure = (rule6 <- rule5 <- rule1 <- FAIL)]]
("Bob" "is" "quiet" "+")
Harry is not red.
Unknown
inv-rconc
[@3: Harry is red.[CWA. Example of deepest failure = (rule5 <- rule1 <- rule6 <- FAIL)]]
("Harry" "is" "red" "-")
Bob is white.
Unknown
rconc
[@4: Bob is white.[CWA. Example of deepest failure = (rule7 <- rule6 <- rule5 <- rule1 <- FAIL)]]
("Bob" "is" "white" "+")
Harry is not nice.
Unknown
inv-rconc
[@4: Harry is nice.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule5 <- rule2 <- FAIL)]]
("Harry" "is" "nice" "-")
Harry is rough.
Unknown
rconc
[@4: Harry is rough.[CWA. Example of deepest failure = (rule4 <- rule6 <- rule5 <- rule1 <- FAIL)]]
("Harry" "is" "rough" "+")
Bob is not smart.
Unknown
inv-random
[@0: Bob is smart.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "smart" "-")
Gary is smart.
Unknown
random
[@0: Gary is smart.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "smart" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Bob is kind.[(triple1)] Charlie is nice.[(triple3)] Charlie is not kind.[(triple2)] Charlie is rough.[(triple4 OR ((((((triple3) -> rule5)) -> rule6)) -> rule4))] Gary is kind.[(triple5)] Harry is kind.[(triple6)] Harry is white.[(triple7)] @1: Charlie is red.[(((triple3) -> rule5))] Gary is red.[(((triple5) -> rule3))] @2: Charlie is quiet.[(((((triple3) -> rule5)) -> rule6))] Gary is quiet.[(((((triple5) -> rule3)) -> rule6))] @3: Charlie is white.[(((((((triple3) -> rule5)) -> rule6) triple3) -> rule7))] Gary is rough.[(((((((triple5) -> rule3)) -> rule6)) -> rule4))] @4: Gary is nice.[(((((((((triple5) -> rule3)) -> rule6)) -> rule4) ((((triple5) -> rule3)) -> rule6)) -> rule1))] @5: Gary is white.[(((((((triple5) -> rule3)) -> rule6) ((((((((triple5) -> rule3)) -> rule6)) -> rule4) ((((triple5) -> rule3)) -> rule6)) -> rule1)) -> rule7))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Charlie is not kind.
("Charlie" "is" "kind" "-")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
((((((triple3) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
triple5
Harry is kind.
("Harry" "is" "kind" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Charlie is red.
("Charlie" "is" "red" "+")
((triple3) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
((triple5) -> (rule3 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((triple5) -> (rule3 % int2))) -> (rule6 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
((((((triple3) -> (rule5 % int3))) -> (rule6 % int2)) triple3) -> (rule7 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
((((((triple5) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
((((((((triple5) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule4 % int2)) ((((triple5) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
int3
Gary is red.
("Gary" "is" "red" "+")
int4
Gary is white.
("Gary" "is" "white" "+")
((((((triple5) -> (rule3 % int5))) -> (rule6 % int4)) ((((((((triple5) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule4 % int3)) ((((triple5) -> (rule3 % int5))) -> (rule6 % int4))) -> (rule1 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is quiet.
("Gary" "is" "quiet" "+")
int4
Gary is red.
("Gary" "is" "red" "+")
int5