Charlie is furry. Charlie is rough. Dave is not big. Dave is kind. Dave is not young. Gary is big. Gary is blue. Gary is furry. Gary is kind. Gary is white. If Gary is big then Gary is not rough. If something is furry and blue then it is kind. If Gary is rough then Gary is kind. All rough, young things are blue. If something is furry and rough then it is young. If Gary is big and Gary is not kind then Gary is white.
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is not big.
("Dave" "is" "big" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is not young.
("Dave" "is" "young" "-")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is white.
("Gary" "is" "white" "+")
If Gary is big then Gary is not rough.
((("Gary" "is" "big" "+")) -> ("Gary" "is" "rough" "-"))
If something is furry and blue then it is kind.
((("something" "is" "furry" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If Gary is rough then Gary is kind.
((("Gary" "is" "rough" "+")) -> ("Gary" "is" "kind" "+"))
All rough, young things are blue.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If something is furry and rough then it is young.
((("something" "is" "furry" "+") ("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
If Gary is big and Gary is not kind then Gary is white.
((("Gary" "is" "big" "+") ("Gary" "is" "kind" "~")) -> ("Gary" "is" "white" "+"))
Gary is furry.
True
1
proof
[(triple8)]
("Gary" "is" "furry" "+")
triple8
Gary is not kind.
False
1
inv-proof
[(triple9 OR ((triple8 triple7) -> rule2))]
("Gary" "is" "kind" "-")
triple9
((triple8 triple7) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not rough.
True
2
proof
[(((triple6) -> rule1))]
("Gary" "is" "rough" "-")
((triple6) -> (rule1 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Charlie is not young.
False
3
inv-proof
[(((triple1 triple2) -> rule5))]
("Charlie" "is" "young" "-")
((triple1 triple2) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is blue.
True
5
proof
[(((triple2 ((triple1 triple2) -> rule5)) -> rule4))]
("Charlie" "is" "blue" "+")
((triple2 ((triple1 triple2) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is not blue.
False
5
inv-proof
[(((triple2 ((triple1 triple2) -> rule5)) -> rule4))]
("Charlie" "is" "blue" "-")
((triple2 ((triple1 triple2) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is kind.
True
7
proof
[(((triple1 ((triple2 ((triple1 triple2) -> rule5)) -> rule4)) -> rule2))]
("Charlie" "is" "kind" "+")
((triple1 ((triple2 ((triple1 triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Charlie is not kind.
False
7
inv-proof
[(((triple1 ((triple2 ((triple1 triple2) -> rule5)) -> rule4)) -> rule2))]
("Charlie" "is" "kind" "-")
((triple1 ((triple2 ((triple1 triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3
Dave is not blue.
Unknown
inv-rconc
[@1: Dave is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "blue" "-")
Gary is young.
Unknown
rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "young" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
@0: Charlie is furry.[(triple1)] Charlie is rough.[(triple2)] Dave is kind.[(triple4)] Dave is not big.[(triple3)] Dave is not young.[(triple5)] Gary is big.[(triple6)] Gary is blue.[(triple7)] Gary is furry.[(triple8)] Gary is kind.[(triple9 OR ((triple8 triple7) -> rule2))] Gary is white.[(triple10)] @1: Charlie is young.[(((triple1 triple2) -> rule5))] Gary is not rough.[(((triple6) -> rule1))] @2: Charlie is blue.[(((triple2 ((triple1 triple2) -> rule5)) -> rule4))] @3: Charlie is kind.[(((triple1 ((triple2 ((triple1 triple2) -> rule5)) -> rule4)) -> rule2))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple4
Dave is not big.
("Dave" "is" "big" "-")
triple3
Dave is not young.
("Dave" "is" "young" "-")
triple5
Gary is big.
("Gary" "is" "big" "+")
triple6
Gary is blue.
("Gary" "is" "blue" "+")
triple7
Gary is furry.
("Gary" "is" "furry" "+")
triple8
Gary is kind.
("Gary" "is" "kind" "+")
triple9
((triple8 triple7) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
triple10
Charlie is young.
("Charlie" "is" "young" "+")
((triple1 triple2) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Gary is not rough.
("Gary" "is" "rough" "-")
((triple6) -> (rule1 % int1))
Gary is not rough.
("Gary" "is" "rough" "-")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple2 ((triple1 triple2) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1 ((triple2 ((triple1 triple2) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
int3