Bob is red. Charlie is red. Charlie is rough. Charlie is white. Erin is rough. Gary is green. Gary is red. If Bob is green then Bob is white. All rough, green people are white. Green people are furry. Green, white people are nice. If Gary is furry and Gary is nice then Gary is rough. All white, furry people are red. All nice people are kind. If someone is kind and furry then they are white. If someone is red and furry then they are kind.
Bob is red.
("Bob" "is" "red" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is red.
("Gary" "is" "red" "+")
If Bob is green then Bob is white.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "white" "+"))
All rough, green people are white.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
Green people are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
Green, white people are nice.
((("someone" "is" "green" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
If Gary is furry and Gary is nice then Gary is rough.
((("Gary" "is" "furry" "+") ("Gary" "is" "nice" "+")) -> ("Gary" "is" "rough" "+"))
All white, furry people are red.
((("someone" "is" "white" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
All nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
If someone is kind and furry then they are white.
((("someone" "is" "kind" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
If someone is red and furry then they are kind.
((("someone" "is" "red" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "kind" "+"))
Gary is red.
True
1
proof
[(triple7)]
("Gary" "is" "red" "+")
triple7
Charlie is not white.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "white" "-")
triple4
Gary is furry.
True
2
proof
[(((triple6) -> rule3))]
("Gary" "is" "furry" "+")
((triple6) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not furry.
False
2
inv-proof
[(((triple6) -> rule3))]
("Gary" "is" "furry" "-")
((triple6) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
True
4
proof
[(((triple7 ((triple6) -> rule3)) -> rule9))]
("Gary" "is" "kind" "+")
((triple7 ((triple6) -> (rule3 % int2))) -> (rule9 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is not kind.
False
4
inv-proof
[(((triple7 ((triple6) -> rule3)) -> rule9))]
("Gary" "is" "kind" "-")
((triple7 ((triple6) -> (rule3 % int2))) -> (rule9 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is white.
True
7
proof
[(((((triple7 ((triple6) -> rule3)) -> rule9) ((triple6) -> rule3)) -> rule8))]
("Gary" "is" "white" "+")
((((triple7 ((triple6) -> (rule3 % int3))) -> (rule9 % int2)) ((triple6) -> (rule3 % int3))) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is not white.
False
7
inv-proof
[(((((triple7 ((triple6) -> rule3)) -> rule9) ((triple6) -> rule3)) -> rule8))]
("Gary" "is" "white" "-")
((((triple7 ((triple6) -> (rule3 % int3))) -> (rule9 % int2)) ((triple6) -> (rule3 % int3))) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is nice.
True
9
proof
[(((triple6 ((((triple7 ((triple6) -> rule3)) -> rule9) ((triple6) -> rule3)) -> rule8)) -> rule4))]
("Gary" "is" "nice" "+")
((triple6 ((((triple7 ((triple6) -> (rule3 % int4))) -> (rule9 % int3)) ((triple6) -> (rule3 % int4))) -> (rule8 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
int4
Gary is not nice.
False
9
inv-proof
[(((triple6 ((((triple7 ((triple6) -> rule3)) -> rule9) ((triple6) -> rule3)) -> rule8)) -> rule4))]
("Gary" "is" "nice" "-")
((triple6 ((((triple7 ((triple6) -> (rule3 % int4))) -> (rule9 % int3)) ((triple6) -> (rule3 % int4))) -> (rule8 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
int4
Gary is rough.
True
12
proof
[(((((triple6) -> rule3) ((triple6 ((((triple7 ((triple6) -> rule3)) -> rule9) ((triple6) -> rule3)) -> rule8)) -> rule4)) -> rule5))]
("Gary" "is" "rough" "+")
((((triple6) -> (rule3 % int5)) ((triple6 ((((triple7 ((triple6) -> (rule3 % int5))) -> (rule9 % int4)) ((triple6) -> (rule3 % int5))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
Gary is furry.
("Gary" "is" "furry" "+")
int5
Gary is not rough.
False
12
inv-proof
[(((((triple6) -> rule3) ((triple6 ((((triple7 ((triple6) -> rule3)) -> rule9) ((triple6) -> rule3)) -> rule8)) -> rule4)) -> rule5))]
("Gary" "is" "rough" "-")
((((triple6) -> (rule3 % int5)) ((triple6 ((((triple7 ((triple6) -> (rule3 % int5))) -> (rule9 % int4)) ((triple6) -> (rule3 % int5))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
Gary is furry.
("Gary" "is" "furry" "+")
int5
Bob is not white.
Unknown
inv-rconc
[@2: Bob is white.[CWA. Example of deepest failure = (rule8 <- rule3 <- FAIL)]]
("Bob" "is" "white" "-")
Bob is furry.
Unknown
rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "furry" "+")
Charlie is not kind.
Unknown
inv-rconc
[@2: Charlie is kind.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("Charlie" "is" "kind" "-")
Bob is kind.
Unknown
rconc
[@2: Bob is kind.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("Bob" "is" "kind" "+")
Erin is not white.
Unknown
inv-rconc
[@2: Erin is white.[CWA. Example of deepest failure = (rule8 <- rule3 <- FAIL)]]
("Erin" "is" "white" "-")
Bob is nice.
Unknown
rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "nice" "+")
Charlie is not green.
Unknown
inv-random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is red.[(triple1)] Charlie is red.[(triple2)] Charlie is rough.[(triple3)] Charlie is white.[(triple4)] Erin is rough.[(triple5)] Gary is green.[(triple6)] Gary is red.[(triple7)] @1: Gary is furry.[(((triple6) -> rule3))] @2: Gary is kind.[(((triple7 ((triple6) -> rule3)) -> rule9))] @3: Gary is white.[(((((triple7 ((triple6) -> rule3)) -> rule9) ((triple6) -> rule3)) -> rule8))] @4: Gary is nice.[(((triple6 ((((triple7 ((triple6) -> rule3)) -> rule9) ((triple6) -> rule3)) -> rule8)) -> rule4))] @5: Gary is rough.[(((((triple6) -> rule3) ((triple6 ((((triple7 ((triple6) -> rule3)) -> rule9) ((triple6) -> rule3)) -> rule8)) -> rule4)) -> rule5))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Charlie is white.
("Charlie" "is" "white" "+")
triple4
Erin is rough.
("Erin" "is" "rough" "+")
triple5
Gary is green.
("Gary" "is" "green" "+")
triple6
Gary is red.
("Gary" "is" "red" "+")
triple7
Gary is furry.
("Gary" "is" "furry" "+")
((triple6) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple7 ((triple6) -> (rule3 % int2))) -> (rule9 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((triple7 ((triple6) -> (rule3 % int3))) -> (rule9 % int2)) ((triple6) -> (rule3 % int3))) -> (rule8 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is furry.
("Gary" "is" "furry" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
((triple6 ((((triple7 ((triple6) -> (rule3 % int4))) -> (rule9 % int3)) ((triple6) -> (rule3 % int4))) -> (rule8 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
int4
Gary is rough.
("Gary" "is" "rough" "+")
((((triple6) -> (rule3 % int5)) ((triple6 ((((triple7 ((triple6) -> (rule3 % int5))) -> (rule9 % int4)) ((triple6) -> (rule3 % int5))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
Gary is furry.
("Gary" "is" "furry" "+")
int5