Bob is not quiet. Bob is round. Bob is smart. Bob is white. Gary is not kind. Gary is nice. Gary is quiet. Gary is rough. Gary is round. Gary is white. Harry is kind. Harry is not nice. Harry is quiet. Harry is round. Harry is smart. Kind, white things are rough. If Bob is kind then Bob is round. If something is rough then it is nice. If something is rough then it is nice. Rough, white things are nice. If something is white then it is smart. If Gary is not white then Gary is quiet. If Bob is round and Bob is smart then Bob is kind.
Bob is not quiet.
("Bob" "is" "quiet" "-")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is white.
("Bob" "is" "white" "+")
Gary is not kind.
("Gary" "is" "kind" "-")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is not nice.
("Harry" "is" "nice" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Kind, white things are rough.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
If Bob is kind then Bob is round.
((("Bob" "is" "kind" "+")) -> ("Bob" "is" "round" "+"))
If something is rough then it is nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If something is rough then it is nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
Rough, white things are nice.
((("something" "is" "rough" "+") ("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
If something is white then it is smart.
((("something" "is" "white" "+")) -> ("something" "is" "smart" "+"))
If Gary is not white then Gary is quiet.
((("Gary" "is" "white" "~")) -> ("Gary" "is" "quiet" "+"))
If Bob is round and Bob is smart then Bob is kind.
((("Bob" "is" "round" "+") ("Bob" "is" "smart" "+")) -> ("Bob" "is" "kind" "+"))
Gary is round.
True
1
proof
[(triple9)]
("Gary" "is" "round" "+")
triple9
Gary is not rough.
False
1
inv-proof
[(triple8)]
("Gary" "is" "rough" "-")
triple8
Bob is kind.
True
3
proof
[(((triple2 triple3) -> rule8) OR ((triple2 ((triple4) -> rule6)) -> rule8))]
("Bob" "is" "kind" "+")
((triple2 triple3) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple2 ((triple4) -> (rule6 % int2))) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is not kind.
False
3
inv-proof
[(((triple2 triple3) -> rule8) OR ((triple2 ((triple4) -> rule6)) -> rule8))]
("Bob" "is" "kind" "-")
((triple2 triple3) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple2 ((triple4) -> (rule6 % int2))) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is rough.
True
5
proof
[(((((triple2 triple3) -> rule8) triple4) -> rule1) OR ((((triple2 ((triple4) -> rule6)) -> rule8) triple4) -> rule1))]
("Bob" "is" "rough" "+")
((((triple2 triple3) -> (rule8 % int2)) triple4) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple2 ((triple4) -> (rule6 % int3))) -> (rule8 % int2)) triple4) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is not rough.
False
5
inv-proof
[(((((triple2 triple3) -> rule8) triple4) -> rule1) OR ((((triple2 ((triple4) -> rule6)) -> rule8) triple4) -> rule1))]
("Bob" "is" "rough" "-")
((((triple2 triple3) -> (rule8 % int2)) triple4) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple2 ((triple4) -> (rule6 % int3))) -> (rule8 % int2)) triple4) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is nice.
True
6
proof
[(((((((triple2 triple3) -> rule8) triple4) -> rule1)) -> rule3) OR ((((((triple2 triple3) -> rule8) triple4) -> rule1)) -> rule4) OR ((((((triple2 triple3) -> rule8) triple4) -> rule1) triple4) -> rule5) OR ((((((triple2 ((triple4) -> rule6)) -> rule8) triple4) -> rule1)) -> rule3) OR ((((((triple2 ((triple4) -> rule6)) -> rule8) triple4) -> rule1)) -> rule4) OR ((((((triple2 ((triple4) -> rule6)) -> rule8) triple4) -> rule1) triple4) -> rule5))]
("Bob" "is" "nice" "+")
((((((triple2 triple3) -> (rule8 % int3)) triple4) -> (rule1 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((((triple2 triple3) -> (rule8 % int3)) triple4) -> (rule1 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((((triple2 triple3) -> (rule8 % int3)) triple4) -> (rule1 % int2)) triple4) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((((triple2 ((triple4) -> (rule6 % int4))) -> (rule8 % int3)) triple4) -> (rule1 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
((((((triple2 ((triple4) -> (rule6 % int4))) -> (rule8 % int3)) triple4) -> (rule1 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
((((((triple2 ((triple4) -> (rule6 % int4))) -> (rule8 % int3)) triple4) -> (rule1 % int2)) triple4) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Bob is not nice.
False
6
inv-proof
[(((((((triple2 triple3) -> rule8) triple4) -> rule1)) -> rule3) OR ((((((triple2 triple3) -> rule8) triple4) -> rule1)) -> rule4) OR ((((((triple2 triple3) -> rule8) triple4) -> rule1) triple4) -> rule5) OR ((((((triple2 ((triple4) -> rule6)) -> rule8) triple4) -> rule1)) -> rule3) OR ((((((triple2 ((triple4) -> rule6)) -> rule8) triple4) -> rule1)) -> rule4) OR ((((((triple2 ((triple4) -> rule6)) -> rule8) triple4) -> rule1) triple4) -> rule5))]
("Bob" "is" "nice" "-")
((((((triple2 triple3) -> (rule8 % int3)) triple4) -> (rule1 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((((triple2 triple3) -> (rule8 % int3)) triple4) -> (rule1 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((((triple2 triple3) -> (rule8 % int3)) triple4) -> (rule1 % int2)) triple4) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((((triple2 ((triple4) -> (rule6 % int4))) -> (rule8 % int3)) triple4) -> (rule1 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
((((((triple2 ((triple4) -> (rule6 % int4))) -> (rule8 % int3)) triple4) -> (rule1 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
((((((triple2 ((triple4) -> (rule6 % int4))) -> (rule8 % int3)) triple4) -> (rule1 % int2)) triple4) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "rough" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Bob is not quiet.[(triple1)] Bob is round.[(triple2)] Bob is smart.[(triple3 OR ((triple4) -> rule6))] Bob is white.[(triple4)] Gary is nice.[(triple6 OR ((triple8) -> rule3) OR ((triple8) -> rule4) OR ((triple8 triple10) -> rule5))] Gary is not kind.[(triple5)] Gary is quiet.[(triple7)] Gary is rough.[(triple8)] Gary is round.[(triple9)] Gary is white.[(triple10)] Harry is kind.[(triple11)] Harry is not nice.[(triple12)] Harry is quiet.[(triple13)] Harry is round.[(triple14)] Harry is smart.[(triple15)] @1: Bob is kind.[(((triple2 triple3) -> rule8) OR ((triple2 ((triple4) -> rule6)) -> rule8))] Gary is smart.[(((triple10) -> rule6))] @2: Bob is rough.[(((((triple2 triple3) -> rule8) triple4) -> rule1) OR ((((triple2 ((triple4) -> rule6)) -> rule8) triple4) -> rule1))] @3: Bob is nice.[(((((((triple2 triple3) -> rule8) triple4) -> rule1)) -> rule3) OR ((((((triple2 triple3) -> rule8) triple4) -> rule1)) -> rule4) OR ((((((triple2 triple3) -> rule8) triple4) -> rule1) triple4) -> rule5) OR ((((((triple2 ((triple4) -> rule6)) -> rule8) triple4) -> rule1)) -> rule3) OR ((((((triple2 ((triple4) -> rule6)) -> rule8) triple4) -> rule1)) -> rule4) OR ((((((triple2 ((triple4) -> rule6)) -> rule8) triple4) -> rule1) triple4) -> rule5))]
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
((triple4) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
triple4
Gary is nice.
("Gary" "is" "nice" "+")
triple6
((triple8) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((triple8) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((triple8 triple10) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not kind.
("Gary" "is" "kind" "-")
triple5
Gary is quiet.
("Gary" "is" "quiet" "+")
triple7
Gary is rough.
("Gary" "is" "rough" "+")
triple8
Gary is round.
("Gary" "is" "round" "+")
triple9
Gary is white.
("Gary" "is" "white" "+")
triple10
Harry is kind.
("Harry" "is" "kind" "+")
triple11
Harry is not nice.
("Harry" "is" "nice" "-")
triple12
Harry is quiet.
("Harry" "is" "quiet" "+")
triple13
Harry is round.
("Harry" "is" "round" "+")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple15
Bob is kind.
("Bob" "is" "kind" "+")
((triple2 triple3) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple2 ((triple4) -> (rule6 % int2))) -> (rule8 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
((triple10) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((((triple2 triple3) -> (rule8 % int2)) triple4) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple2 ((triple4) -> (rule6 % int3))) -> (rule8 % int2)) triple4) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
int3
Bob is nice.
("Bob" "is" "nice" "+")
((((((triple2 triple3) -> (rule8 % int3)) triple4) -> (rule1 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((((triple2 triple3) -> (rule8 % int3)) triple4) -> (rule1 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((((triple2 triple3) -> (rule8 % int3)) triple4) -> (rule1 % int2)) triple4) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
((((((triple2 ((triple4) -> (rule6 % int4))) -> (rule8 % int3)) triple4) -> (rule1 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
((((((triple2 ((triple4) -> (rule6 % int4))) -> (rule8 % int3)) triple4) -> (rule1 % int2))) -> (rule4 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4
((((((triple2 ((triple4) -> (rule6 % int4))) -> (rule8 % int3)) triple4) -> (rule1 % int2)) triple4) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
int4