Bob is kind. Bob is white. Charlie is blue. Charlie is not green. Charlie is rough. Charlie is not white. Dave is green. Dave is kind. Gary is not blue. Gary is green. Gary is not kind. Gary is rough. All kind, nice things are white. Green things are nice. If something is blue then it is nice. If something is kind then it is green. If Gary is smart and Gary is nice then Gary is rough. Nice things are rough. If something is smart and blue then it is rough. If something is rough and not white then it is smart.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is white.
("Bob" "is" "white" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is not green.
("Charlie" "is" "green" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is not white.
("Charlie" "is" "white" "-")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Gary is not blue.
("Gary" "is" "blue" "-")
Gary is green.
("Gary" "is" "green" "+")
Gary is not kind.
("Gary" "is" "kind" "-")
Gary is rough.
("Gary" "is" "rough" "+")
All kind, nice things are white.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
Green things are nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If something is blue then it is nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
If something is kind then it is green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If Gary is smart and Gary is nice then Gary is rough.
((("Gary" "is" "smart" "+") ("Gary" "is" "nice" "+")) -> ("Gary" "is" "rough" "+"))
Nice things are rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If something is smart and blue then it is rough.
((("something" "is" "smart" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If something is rough and not white then it is smart.
((("something" "is" "rough" "+") ("something" "is" "white" "~")) -> ("something" "is" "smart" "+"))
Gary is not blue.
True
1
proof
[(triple9)]
("Gary" "is" "blue" "-")
triple9
Charlie is green.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "green" "+")
triple4
Gary is nice.
True
2
proof
[(((triple10) -> rule2))]
("Gary" "is" "nice" "+")
((triple10) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple1) -> rule4))]
("Bob" "is" "green" "-")
((triple1) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Dave is rough.
True
3
proof
[(((((triple7) -> rule2)) -> rule6) OR ((((((triple8) -> rule4)) -> rule2)) -> rule6))]
("Dave" "is" "rough" "+")
((((triple7) -> (rule2 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((((triple8) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is not white.
False
4
inv-proof
[(((triple8 ((triple7) -> rule2)) -> rule1) OR ((triple8 ((((triple8) -> rule4)) -> rule2)) -> rule1))]
("Dave" "is" "white" "-")
((triple8 ((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((triple8 ((((triple8) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Bob is rough.
True
4
proof
[(((((((triple1) -> rule4)) -> rule2)) -> rule6))]
("Bob" "is" "rough" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is not rough.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule2)) -> rule6))]
("Bob" "is" "rough" "-")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Gary is not smart.
Unknown
inv-rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "smart" "-")
Dave is smart.
Unknown
rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "smart" "+")
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "smart" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "white" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
@0: Bob is kind.[(triple1)] Bob is white.[(triple2 OR ((triple1 ((((triple1) -> rule4)) -> rule2)) -> rule1))] Charlie is blue.[(triple3)] Charlie is not green.[(triple4)] Charlie is not white.[(triple6)] Charlie is rough.[(triple5 OR ((((triple3) -> rule3)) -> rule6))] Dave is green.[(triple7 OR ((triple8) -> rule4))] Dave is kind.[(triple8)] Gary is green.[(triple10)] Gary is not blue.[(triple9)] Gary is not kind.[(triple11)] Gary is rough.[(triple12 OR ((((triple10) -> rule2)) -> rule6))] @1: Bob is green.[(((triple1) -> rule4))] Charlie is nice.[(((triple3) -> rule3))] Charlie is smart.[(((triple5 triple6) -> rule8) OR ((((((triple3) -> rule3)) -> rule6) triple6) -> rule8))] Dave is nice.[(((triple7) -> rule2) OR ((((triple8) -> rule4)) -> rule2))] Gary is nice.[(((triple10) -> rule2))] @2: Bob is nice.[(((((triple1) -> rule4)) -> rule2))] Dave is rough.[(((((triple7) -> rule2)) -> rule6) OR ((((((triple8) -> rule4)) -> rule2)) -> rule6))] Dave is white.[(((triple8 ((triple7) -> rule2)) -> rule1) OR ((triple8 ((((triple8) -> rule4)) -> rule2)) -> rule1))] @3: Bob is rough.[(((((((triple1) -> rule4)) -> rule2)) -> rule6))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
((triple1 ((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Charlie is blue.
("Charlie" "is" "blue" "+")
triple3
Charlie is not green.
("Charlie" "is" "green" "-")
triple4
Charlie is not white.
("Charlie" "is" "white" "-")
triple6
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
((((triple3) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
triple7
((triple8) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
triple8
Gary is green.
("Gary" "is" "green" "+")
triple10
Gary is not blue.
("Gary" "is" "blue" "-")
triple9
Gary is not kind.
("Gary" "is" "kind" "-")
triple11
Gary is rough.
("Gary" "is" "rough" "+")
triple12
((((triple10) -> (rule2 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple3) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple5 triple6) -> (rule8 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((((((triple3) -> (rule3 % int3))) -> (rule6 % int2)) triple6) -> (rule8 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
((triple7) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple8) -> (rule4 % int2))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
((triple10) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((((triple1) -> (rule4 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
((((triple7) -> (rule2 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((((triple8) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Dave is white.
("Dave" "is" "white" "+")
((triple8 ((triple7) -> (rule2 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((triple8 ((((triple8) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
((((((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3