Charlie is red. Erin is big. Erin is furry. Erin is kind. Erin is nice. Erin is young. Fiona is kind. Fiona is red. Fiona is young. Gary is big. Rough people are red. If someone is furry and red then they are young. Kind people are rough. All kind people are nice. If Gary is red then Gary is furry. If someone is big then they are kind. If Charlie is rough then Charlie is furry. If someone is young and big then they are red.
Charlie is red.
("Charlie" "is" "red" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Rough people are red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If someone is furry and red then they are young.
((("someone" "is" "furry" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
Kind people are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
All kind people are nice.
((("someone" "is" "kind" "+")) -> ("someone" "is" "nice" "+"))
If Gary is red then Gary is furry.
((("Gary" "is" "red" "+")) -> ("Gary" "is" "furry" "+"))
If someone is big then they are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
If Charlie is rough then Charlie is furry.
((("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "furry" "+"))
If someone is young and big then they are red.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
Fiona is red.
True
1
proof
[(triple8 OR ((((triple7) -> rule3)) -> rule1))]
("Fiona" "is" "red" "+")
triple8
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Erin is not kind.
False
1
inv-proof
[(triple4 OR ((triple2) -> rule6))]
("Erin" "is" "kind" "-")
triple4
((triple2) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is rough.
True
2
proof
[(((triple4) -> rule3) OR ((((triple2) -> rule6)) -> rule3))]
("Erin" "is" "rough" "+")
((triple4) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is not red.
False
3
inv-proof
[(((triple6 triple2) -> rule8) OR ((((triple4) -> rule3)) -> rule1) OR ((((((triple2) -> rule6)) -> rule3)) -> rule1))]
("Erin" "is" "red" "-")
((triple6 triple2) -> (rule8 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Gary is nice.
True
3
proof
[(((((triple10) -> rule6)) -> rule4))]
("Gary" "is" "nice" "+")
((((triple10) -> (rule6 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is not nice.
False
3
inv-proof
[(((((triple10) -> rule6)) -> rule4))]
("Gary" "is" "nice" "-")
((((triple10) -> (rule6 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is red.
True
4
proof
[(((((((triple10) -> rule6)) -> rule3)) -> rule1))]
("Gary" "is" "red" "+")
((((((triple10) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is not red.
False
4
inv-proof
[(((((((triple10) -> rule6)) -> rule3)) -> rule1))]
("Gary" "is" "red" "-")
((((((triple10) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is furry.
True
5
proof
[(((((((((triple10) -> rule6)) -> rule3)) -> rule1)) -> rule5))]
("Gary" "is" "furry" "+")
((((((((triple10) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
Gary is not furry.
False
5
inv-proof
[(((((((((triple10) -> rule6)) -> rule3)) -> rule1)) -> rule5))]
("Gary" "is" "furry" "-")
((((((((triple10) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
Gary is young.
True
10
proof
[(((((((((((triple10) -> rule6)) -> rule3)) -> rule1)) -> rule5) ((((((triple10) -> rule6)) -> rule3)) -> rule1)) -> rule2))]
("Gary" "is" "young" "+")
((((((((((triple10) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule5 % int2)) ((((((triple10) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
Gary is kind.
("Gary" "is" "kind" "+")
int5
Gary is not young.
False
10
inv-proof
[(((((((((((triple10) -> rule6)) -> rule3)) -> rule1)) -> rule5) ((((((triple10) -> rule6)) -> rule3)) -> rule1)) -> rule2))]
("Gary" "is" "young" "-")
((((((((((triple10) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule5 % int2)) ((((((triple10) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
Gary is kind.
("Gary" "is" "kind" "+")
int5
Charlie is not furry.
Unknown
inv-rconc
[@3: Charlie is furry.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule6 <- FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is kind.
Unknown
rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "kind" "+")
Charlie is not young.
Unknown
inv-rconc
[@4: Charlie is young.[CWA. Example of deepest failure = (rule2 <- rule7 <- rule3 <- rule6 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is rough.
Unknown
rconc
[@2: Charlie is rough.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Charlie" "is" "rough" "+")
Charlie is not nice.
Unknown
inv-rconc
[@2: Charlie is nice.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Charlie" "is" "nice" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
@0: Charlie is red.[(triple1)] Erin is big.[(triple2)] Erin is furry.[(triple3)] Erin is kind.[(triple4 OR ((triple2) -> rule6))] Erin is nice.[(triple5 OR ((triple4) -> rule4) OR ((((triple2) -> rule6)) -> rule4))] Erin is young.[(triple6 OR ((triple3 ((((triple4) -> rule3)) -> rule1)) -> rule2) OR ((triple3 ((((((triple2) -> rule6)) -> rule3)) -> rule1)) -> rule2))] Fiona is kind.[(triple7)] Fiona is red.[(triple8 OR ((((triple7) -> rule3)) -> rule1))] Fiona is young.[(triple9)] Gary is big.[(triple10)] @1: Erin is red.[(((triple6 triple2) -> rule8) OR ((((triple4) -> rule3)) -> rule1) OR ((((((triple2) -> rule6)) -> rule3)) -> rule1))] Erin is rough.[(((triple4) -> rule3) OR ((((triple2) -> rule6)) -> rule3))] Fiona is nice.[(((triple7) -> rule4))] Fiona is rough.[(((triple7) -> rule3))] Gary is kind.[(((triple10) -> rule6))] @2: Gary is nice.[(((((triple10) -> rule6)) -> rule4))] Gary is rough.[(((((triple10) -> rule6)) -> rule3))] @3: Gary is red.[(((((((triple10) -> rule6)) -> rule3)) -> rule1))] @4: Gary is furry.[(((((((((triple10) -> rule6)) -> rule3)) -> rule1)) -> rule5))] @5: Gary is young.[(((((((((((triple10) -> rule6)) -> rule3)) -> rule1)) -> rule5) ((((((triple10) -> rule6)) -> rule3)) -> rule1)) -> rule2))]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Erin is big.
("Erin" "is" "big" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
triple3
Erin is kind.
("Erin" "is" "kind" "+")
triple4
((triple2) -> (rule6 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple5
((triple4) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule4 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
triple6
((triple3 ((((triple4) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
((triple3 ((((((triple2) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
int4
Fiona is kind.
("Fiona" "is" "kind" "+")
triple7
Fiona is red.
("Fiona" "is" "red" "+")
triple8
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is young.
("Fiona" "is" "young" "+")
triple9
Gary is big.
("Gary" "is" "big" "+")
triple10
Erin is red.
("Erin" "is" "red" "+")
((triple6 triple2) -> (rule8 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is kind.
("Erin" "is" "kind" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
((triple4) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
((triple7) -> (rule4 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple7) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple10) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((((triple10) -> (rule6 % int2))) -> (rule4 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
((((triple10) -> (rule6 % int2))) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
((((((triple10) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Gary is red.
("Gary" "is" "red" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
((((((((triple10) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is red.
("Gary" "is" "red" "+")
int2
Gary is rough.
("Gary" "is" "rough" "+")
int3
Gary is kind.
("Gary" "is" "kind" "+")
int4
Gary is young.
("Gary" "is" "young" "+")
((((((((((triple10) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule5 % int2)) ((((((triple10) -> (rule6 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule2 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
int3
Gary is rough.
("Gary" "is" "rough" "+")
int4
Gary is kind.
("Gary" "is" "kind" "+")
int5