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