Bob is kind. Gary is kind. Gary is young. If something is kind then it is blue. If something is blue then it is kind. Kind things are blue. Kind, rough things are white. If Bob is blue and Bob is young then Bob is big. Young, blue things are rough. If something is kind and rough then it is white. If Gary is rough and Gary is white then Gary is big.
Bob is kind.
("Bob" "is" "kind" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is young.
("Gary" "is" "young" "+")
If something is kind then it is blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
If something is blue then it is kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
Kind things are blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
Kind, rough things are white.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
If Bob is blue and Bob is young then Bob is big.
((("Bob" "is" "blue" "+") ("Bob" "is" "young" "+")) -> ("Bob" "is" "big" "+"))
Young, blue things are rough.
((("something" "is" "young" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If something is kind and rough then it is white.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
If Gary is rough and Gary is white then Gary is big.
((("Gary" "is" "rough" "+") ("Gary" "is" "white" "+")) -> ("Gary" "is" "big" "+"))
Gary is young.
True
1
proof
[(triple3)]
("Gary" "is" "young" "+")
triple3
Gary is not kind.
False
1
inv-proof
[(triple2)]
("Gary" "is" "kind" "-")
triple2
Gary is blue.
True
2
proof
[(((triple2) -> rule1) OR ((triple2) -> rule3))]
("Gary" "is" "blue" "+")
((triple2) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple2) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Bob is not blue.
False
2
inv-proof
[(((triple1) -> rule1) OR ((triple1) -> rule3))]
("Bob" "is" "blue" "-")
((triple1) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple1) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Gary is rough.
True
4
proof
[(((triple3 ((triple2) -> rule1)) -> rule6) OR ((triple3 ((triple2) -> rule3)) -> rule6))]
("Gary" "is" "rough" "+")
((triple3 ((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((triple3 ((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is not rough.
False
4
inv-proof
[(((triple3 ((triple2) -> rule1)) -> rule6) OR ((triple3 ((triple2) -> rule3)) -> rule6))]
("Gary" "is" "rough" "-")
((triple3 ((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((triple3 ((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is white.
True
6
proof
[(((triple2 ((triple3 ((triple2) -> rule1)) -> rule6)) -> rule4) OR ((triple2 ((triple3 ((triple2) -> rule1)) -> rule6)) -> rule7) OR ((triple2 ((triple3 ((triple2) -> rule3)) -> rule6)) -> rule4) OR ((triple2 ((triple3 ((triple2) -> rule3)) -> rule6)) -> rule7))]
("Gary" "is" "white" "+")
((triple2 ((triple3 ((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
((triple2 ((triple3 ((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
((triple2 ((triple3 ((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
((triple2 ((triple3 ((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is not white.
False
6
inv-proof
[(((triple2 ((triple3 ((triple2) -> rule1)) -> rule6)) -> rule4) OR ((triple2 ((triple3 ((triple2) -> rule1)) -> rule6)) -> rule7) OR ((triple2 ((triple3 ((triple2) -> rule3)) -> rule6)) -> rule4) OR ((triple2 ((triple3 ((triple2) -> rule3)) -> rule6)) -> rule7))]
("Gary" "is" "white" "-")
((triple2 ((triple3 ((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
((triple2 ((triple3 ((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
((triple2 ((triple3 ((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
((triple2 ((triple3 ((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Bob is not white.
Unknown
inv-rconc
[@2: Bob is white.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Bob" "is" "white" "-")
Bob is big.
Unknown
rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "big" "+")
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
Bob is not young.
Unknown
inv-random
[@0: Bob is young.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "young" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Bob is kind.[(triple1)] Gary is kind.[(triple2)] Gary is young.[(triple3)] @1: Bob is blue.[(((triple1) -> rule1) OR ((triple1) -> rule3))] Gary is blue.[(((triple2) -> rule1) OR ((triple2) -> rule3))] @2: Gary is rough.[(((triple3 ((triple2) -> rule1)) -> rule6) OR ((triple3 ((triple2) -> rule3)) -> rule6))] @3: Gary is white.[(((triple2 ((triple3 ((triple2) -> rule1)) -> rule6)) -> rule4) OR ((triple2 ((triple3 ((triple2) -> rule1)) -> rule6)) -> rule7) OR ((triple2 ((triple3 ((triple2) -> rule3)) -> rule6)) -> rule4) OR ((triple2 ((triple3 ((triple2) -> rule3)) -> rule6)) -> rule7))] @4: Gary is big.[(((((triple3 ((triple2) -> rule1)) -> rule6) ((triple2 ((triple3 ((triple2) -> rule1)) -> rule6)) -> rule4)) -> rule8) OR ((((triple3 ((triple2) -> rule1)) -> rule6) ((triple2 ((triple3 ((triple2) -> rule1)) -> rule6)) -> rule7)) -> rule8) OR ((((triple3 ((triple2) -> rule1)) -> rule6) ((triple2 ((triple3 ((triple2) -> rule3)) -> rule6)) -> rule4)) -> rule8) OR ((((triple3 ((triple2) -> rule1)) -> rule6) ((triple2 ((triple3 ((triple2) -> rule3)) -> rule6)) -> rule7)) -> rule8) OR ((((triple3 ((triple2) -> rule3)) -> rule6) ((triple2 ((triple3 ((triple2) -> rule1)) -> rule6)) -> rule4)) -> rule8) OR ((((triple3 ((triple2) -> rule3)) -> rule6) ((triple2 ((triple3 ((triple2) -> rule1)) -> rule6)) -> rule7)) -> rule8) OR ((((triple3 ((triple2) -> rule3)) -> rule6) ((triple2 ((triple3 ((triple2) -> rule3)) -> rule6)) -> rule4)) -> rule8) OR ((((triple3 ((triple2) -> rule3)) -> rule6) ((triple2 ((triple3 ((triple2) -> rule3)) -> rule6)) -> rule7)) -> rule8))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Gary is kind.
("Gary" "is" "kind" "+")
triple2
Gary is young.
("Gary" "is" "young" "+")
triple3
Bob is blue.
("Bob" "is" "blue" "+")
((triple1) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((triple1) -> (rule3 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
((triple2) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple2) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple3 ((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
((triple3 ((triple2) -> (rule3 % int2))) -> (rule6 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((triple2 ((triple3 ((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
((triple2 ((triple3 ((triple2) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
((triple2 ((triple3 ((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
((triple2 ((triple3 ((triple2) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is big.
("Gary" "is" "big" "+")
((((triple3 ((triple2) -> (rule1 % int4))) -> (rule6 % int3)) ((triple2 ((triple3 ((triple2) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
((((triple3 ((triple2) -> (rule1 % int4))) -> (rule6 % int3)) ((triple2 ((triple3 ((triple2) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
((((triple3 ((triple2) -> (rule1 % int4))) -> (rule6 % int3)) ((triple2 ((triple3 ((triple2) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
((((triple3 ((triple2) -> (rule1 % int4))) -> (rule6 % int3)) ((triple2 ((triple3 ((triple2) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
((((triple3 ((triple2) -> (rule3 % int4))) -> (rule6 % int3)) ((triple2 ((triple3 ((triple2) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
((((triple3 ((triple2) -> (rule3 % int4))) -> (rule6 % int3)) ((triple2 ((triple3 ((triple2) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
((((triple3 ((triple2) -> (rule3 % int4))) -> (rule6 % int3)) ((triple2 ((triple3 ((triple2) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4
((((triple3 ((triple2) -> (rule3 % int4))) -> (rule6 % int3)) ((triple2 ((triple3 ((triple2) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4