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